E---3.5.1.THM-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : E---3.5.1
% Problem  : SWW900+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n018.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 : Thu Sep 24 03:11:23 PM UTC 2026

% Result   : Theorem 103.94s 25.64s
% Output   : CNFRefutation 103.94s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   11
%            Number of leaves      :   13
% Syntax   : Number of formulae    :   61 (  30 unt;   0 def)
%            Number of atoms       :  257 ( 185 equ)
%            Maximal formula atoms :   48 (   4 avg)
%            Number of connectives :  253 (  57   ~;  41   |; 134   &)
%                                         (  16 <=>;   5  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   82 (   6 avg)
%            Maximal term depth    :    9 (   2 avg)
%            Number of predicates  :    3 (   1 usr;   1 prp; 0-2 aty)
%            Number of functors    :   36 (  36 usr;  12 con; 0-3 aty)
%            Number of variables   :  249 (   7 sgn 192   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof('thm.bool.EQ_CLAUSES',axiom,
    ! [X8] :
      ( ( s__02(cbool__00,X8) = s__02(cbool__00,cF__00)
      <=> ~ p__01(s__02(cbool__00,X8)) )
      & ( s__02(cbool__00,cF__00) = s__02(cbool__00,X8)
      <=> ~ p__01(s__02(cbool__00,X8)) )
      & ( s__02(cbool__00,X8) = s__02(cbool__00,cT__00)
      <=> p__01(s__02(cbool__00,X8)) )
      & ( s__02(cbool__00,cT__00) = s__02(cbool__00,X8)
      <=> p__01(s__02(cbool__00,X8)) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.bool.EQ_CLAUSES') ).

fof(conjecture,conjecture,
    ! [X7,X20,X29,X18,X19,X21] :
      ( p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X7),X29),s__02(c_27type_2elist_2elist_27__01(X7),X18))),s__02(c_27type_2elist_2elist_27__01(X20),X19))))
     => ( p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),X18),s__02(c_27type_2elist_2elist_27__01(X20),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X29))),s__02(c_27type_2elist_2elist_27__01(X20),X19))))))
        & p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),X29),s__02(c_27type_2elist_2elist_27__01(X20),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X29))),s__02(c_27type_2elist_2elist_27__01(X20),X19)))))) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).

fof('thm.rich_list.LIST_REL_APPEND_IMP',axiom,
    ! [X7,X20,X24,X25,X26,X27,X28] :
      ( ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X25))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X20),X26)))
        & p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X24),s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X7),X25),s__02(c_27type_2elist_2elist_27__01(X7),X27))),s__02(c_27type_2elist_2elist_27__01(X20),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X20),X26),s__02(c_27type_2elist_2elist_27__01(X20),X28)))))) )
     => ( p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X24),s__02(c_27type_2elist_2elist_27__01(X7),X27),s__02(c_27type_2elist_2elist_27__01(X20),X28))))
        & p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X24),s__02(c_27type_2elist_2elist_27__01(X7),X25),s__02(c_27type_2elist_2elist_27__01(X20),X26)))) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.rich_list.LIST_REL_APPEND_IMP') ).

fof('thm.list.TAKE_DROP',axiom,
    ! [X7,X15,X23] : s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2elist_2elist_27__01(X7),X23))),s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2elist_2elist_27__01(X7),X23))))) = s__02(c_27type_2elist_2elist_27__01(X7),X23),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.list.TAKE_DROP') ).

fof('HL_TRUTH',axiom,
    p__01(s__02(cbool__00,cT__00)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','HL_TRUTH') ).

fof('thm.list.LIST_REL_LENGTH',axiom,
    ! [X7,X20,X21,X9,X22] :
      ( p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),X9),s__02(c_27type_2elist_2elist_27__01(X20),X22))))
     => s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X9))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X20),X22))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.list.LIST_REL_LENGTH') ).

fof('HL_BOOL_CASES',axiom,
    ! [X1] :
      ( s__02(cbool__00,X1) = s__02(cbool__00,cF__00)
      | s__02(cbool__00,X1) = s__02(cbool__00,cT__00) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','HL_BOOL_CASES') ).

fof('HL_FALSITY',axiom,
    ~ p__01(s__02(cbool__00,cF__00)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','HL_FALSITY') ).

fof('thm.numeral.numeral_distrib',axiom,
    ( p__01(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))
    & ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15,X16] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] :
        ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))))
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) )
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,cT__00)
    & ! [X15,X16] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(cbool__00,cT__00)
    & ! [X15,X16] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(cbool__00,cF__00)
    & ! [X15,X16] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))
    & ! [X15] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,cF__00)
    & ! [X15,X16] :
        ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16)))
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,X16) )
    & ! [X15] :
        ( s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00) )
    & ! [X15] :
        ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00) )
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))))
    & s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))))
    & s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X15)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X15)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,X15) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.numeral.numeral_distrib') ).

fof('thm.arithmetic.ADD_MONO_LESS_EQ',axiom,
    ! [X16,X15,X17] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X17))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X17))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.arithmetic.ADD_MONO_LESS_EQ') ).

fof('thm.arithmetic.ADD_CLAUSES',axiom,
    ! [X15,X16] :
      ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X16))),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X16)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X16))) = s__02(c_27type_2enum_2enum_27__00,X16) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.arithmetic.ADD_CLAUSES') ).

fof('thm.list.LENGTH_TAKE',axiom,
    ! [X7,X15,X23] :
      ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X23))))))
     => s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2elist_2elist_27__01(X7),X23))))) = s__02(c_27type_2enum_2enum_27__00,X15) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.list.LENGTH_TAKE') ).

fof('thm.list.LENGTH_APPEND',axiom,
    ! [X7,X18,X19] : s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X7),X18),s__02(c_27type_2elist_2elist_27__01(X7),X19))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X18))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X19))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.list.LENGTH_APPEND') ).

fof(c_0_13,plain,
    ! [X8] :
      ( ( s__02(cbool__00,X8) = s__02(cbool__00,cF__00)
      <=> ~ p__01(s__02(cbool__00,X8)) )
      & ( s__02(cbool__00,cF__00) = s__02(cbool__00,X8)
      <=> ~ p__01(s__02(cbool__00,X8)) )
      & ( s__02(cbool__00,X8) = s__02(cbool__00,cT__00)
      <=> p__01(s__02(cbool__00,X8)) )
      & ( s__02(cbool__00,cT__00) = s__02(cbool__00,X8)
      <=> p__01(s__02(cbool__00,X8)) ) ),
    inference(fof_simplification,[status(thm)],['thm.bool.EQ_CLAUSES']) ).

fof(c_0_14,negated_conjecture,
    ~ ! [X7,X20,X29,X18,X19,X21] :
        ( p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X7),X29),s__02(c_27type_2elist_2elist_27__01(X7),X18))),s__02(c_27type_2elist_2elist_27__01(X20),X19))))
       => ( p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),X18),s__02(c_27type_2elist_2elist_27__01(X20),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X29))),s__02(c_27type_2elist_2elist_27__01(X20),X19))))))
          & p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X7,cfun__02(X20,cbool__00)),X21),s__02(c_27type_2elist_2elist_27__01(X7),X29),s__02(c_27type_2elist_2elist_27__01(X20),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X7),X29))),s__02(c_27type_2elist_2elist_27__01(X20),X19)))))) ) ),
    inference(assume_negation,[status(cth)],[conjecture]) ).

fof(c_0_15,plain,
    ! [X122,X123,X124,X125,X126,X127,X128] :
      ( ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X122),X125))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X123),X126)))
        | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X122,cfun__02(X123,cbool__00)),X124),s__02(c_27type_2elist_2elist_27__01(X122),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X122),X125),s__02(c_27type_2elist_2elist_27__01(X122),X127))),s__02(c_27type_2elist_2elist_27__01(X123),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X123),X126),s__02(c_27type_2elist_2elist_27__01(X123),X128))))))
        | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X122,cfun__02(X123,cbool__00)),X124),s__02(c_27type_2elist_2elist_27__01(X122),X127),s__02(c_27type_2elist_2elist_27__01(X123),X128)))) )
      & ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X122),X125))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X123),X126)))
        | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X122,cfun__02(X123,cbool__00)),X124),s__02(c_27type_2elist_2elist_27__01(X122),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X122),X125),s__02(c_27type_2elist_2elist_27__01(X122),X127))),s__02(c_27type_2elist_2elist_27__01(X123),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X123),X126),s__02(c_27type_2elist_2elist_27__01(X123),X128))))))
        | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X122,cfun__02(X123,cbool__00)),X124),s__02(c_27type_2elist_2elist_27__01(X122),X125),s__02(c_27type_2elist_2elist_27__01(X123),X126)))) ) ),
    inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['thm.rich_list.LIST_REL_APPEND_IMP'])])])]) ).

fof(c_0_16,plain,
    ! [X119,X120,X121] : s__02(c_27type_2elist_2elist_27__01(X119),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X119),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X120),s__02(c_27type_2elist_2elist_27__01(X119),X121))),s__02(c_27type_2elist_2elist_27__01(X119),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,X120),s__02(c_27type_2elist_2elist_27__01(X119),X121))))) = s__02(c_27type_2elist_2elist_27__01(X119),X121),
    inference(variable_rename,[status(thm)],['thm.list.TAKE_DROP']) ).

fof(c_0_17,plain,
    ! [X38] :
      ( ( s__02(cbool__00,X38) = s__02(cbool__00,cF__00)
        | p__01(s__02(cbool__00,X38)) )
      & ( ~ p__01(s__02(cbool__00,X38))
        | s__02(cbool__00,X38) != s__02(cbool__00,cF__00) )
      & ( s__02(cbool__00,cF__00) = s__02(cbool__00,X38)
        | p__01(s__02(cbool__00,X38)) )
      & ( ~ p__01(s__02(cbool__00,X38))
        | s__02(cbool__00,cF__00) != s__02(cbool__00,X38) )
      & ( s__02(cbool__00,X38) = s__02(cbool__00,cT__00)
        | ~ p__01(s__02(cbool__00,X38)) )
      & ( p__01(s__02(cbool__00,X38))
        | s__02(cbool__00,X38) != s__02(cbool__00,cT__00) )
      & ( s__02(cbool__00,cT__00) = s__02(cbool__00,X38)
        | ~ p__01(s__02(cbool__00,X38)) )
      & ( p__01(s__02(cbool__00,X38))
        | s__02(cbool__00,cT__00) != s__02(cbool__00,X38) ) ),
    inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])]) ).

fof(c_0_18,negated_conjecture,
    ( ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))))
      | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))))) )
    & p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))) ),
    inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])]) ).

cnf(c_0_19,plain,
    ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X6))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),X7)))
    | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),X6),s__02(c_27type_2elist_2elist_27__01(X1),X4))),s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X2),X7),s__02(c_27type_2elist_2elist_27__01(X2),X5))))))
    | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X2),X5)))) ),
    inference(split_conjunct,[status(thm)],[c_0_15]) ).

cnf(c_0_20,plain,
    s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2elist_2elist_27__01(X1),X3))),s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2elist_2elist_27__01(X1),X3))))) = s__02(c_27type_2elist_2elist_27__01(X1),X3),
    inference(split_conjunct,[status(thm)],[c_0_16]) ).

cnf(c_0_21,plain,
    ( ~ p__01(s__02(cbool__00,X1))
    | s__02(cbool__00,X1) = s__02(cbool__00,cT__00) ),
    inference(split_conjunct,[status(thm)],[c_0_17]) ).

cnf(c_0_22,negated_conjecture,
    p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))),
    inference(split_conjunct,[status(thm)],[c_0_18]) ).

cnf(c_0_23,plain,
    ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),X7),s__02(c_27type_2elist_2elist_27__01(X1),X4))),s__02(c_27type_2elist_2elist_27__01(X2),X6))))
    | s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X7))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X5),s__02(c_27type_2elist_2elist_27__01(X2),X6)))))
    | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,X5),s__02(c_27type_2elist_2elist_27__01(X2),X6)))))) ),
    inference(spm,[status(thm)],[c_0_19,c_0_20]) ).

cnf(c_0_24,negated_conjecture,
    s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))) = s__02(cbool__00,cT__00),
    inference(spm,[status(thm)],[c_0_21,c_0_22]) ).

cnf(c_0_25,plain,
    p__01(s__02(cbool__00,cT__00)),
    inference(split_conjunct,[status(thm)],['HL_TRUTH']) ).

fof(c_0_26,plain,
    ! [X111,X112,X113,X114,X115] :
      ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X111),X114))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X112),X115)))
      | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X111,cfun__02(X112,cbool__00)),X113),s__02(c_27type_2elist_2elist_27__01(X111),X114),s__02(c_27type_2elist_2elist_27__01(X112),X115)))) ),
    inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['thm.list.LIST_REL_LENGTH'])])]) ).

cnf(c_0_27,plain,
    ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X4))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),X5)))
    | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X1),X6))),s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X2),X5),s__02(c_27type_2elist_2elist_27__01(X2),X7))))))
    | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X2),X5)))) ),
    inference(split_conjunct,[status(thm)],[c_0_15]) ).

cnf(c_0_28,negated_conjecture,
    ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))))
    | ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))))) ),
    inference(split_conjunct,[status(thm)],[c_0_18]) ).

cnf(c_0_29,negated_conjecture,
    ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0)))
    | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))))) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_24]),c_0_25])]) ).

cnf(c_0_30,plain,
    ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X2),X5))))
    | s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X4))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),X5))) ),
    inference(split_conjunct,[status(thm)],[c_0_26]) ).

fof(c_0_31,plain,
    ! [X30] :
      ( s__02(cbool__00,X30) = s__02(cbool__00,cF__00)
      | s__02(cbool__00,X30) = s__02(cbool__00,cT__00) ),
    inference(variable_rename,[status(thm)],['HL_BOOL_CASES']) ).

fof(c_0_32,plain,
    ~ p__01(s__02(cbool__00,cF__00)),
    inference(fof_simplification,[status(thm)],['HL_FALSITY']) ).

fof(c_0_33,plain,
    ( p__01(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))
    & ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15,X16] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] :
        ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))))
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) )
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,cT__00)
    & ! [X15,X16] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(cbool__00,cT__00)
    & ! [X15,X16] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X16),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(cbool__00,cF__00)
    & ! [X15,X16] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))
    & ! [X15] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,X15)))
    & ! [X15] : s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,cF__00)
    & ! [X15,X16] :
        ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16)))
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,X16) )
    & ! [X15] :
        ( s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00) )
    & ! [X15] :
        ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      <=> s__02(c_27type_2enum_2enum_27__00,X15) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00) )
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))))
    & s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X15)))))
    & s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,X15))))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X15)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
    & ! [X15,X16] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X15))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X16))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,X16)))))))
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X15),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X15)
    & ! [X15] : s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X15))) = s__02(c_27type_2enum_2enum_27__00,X15) ),
    inference(fof_simplification,[status(thm)],['thm.numeral.numeral_distrib']) ).

cnf(c_0_34,plain,
    ( ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X1),X7))),s__02(c_27type_2elist_2elist_27__01(X2),X6))))
    | s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X4))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X5),s__02(c_27type_2elist_2elist_27__01(X2),X6)))))
    | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(X1,cfun__02(X2,cbool__00)),X3),s__02(c_27type_2elist_2elist_27__01(X1),X4),s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X5),s__02(c_27type_2elist_2elist_27__01(X2),X6)))))) ),
    inference(spm,[status(thm)],[c_0_27,c_0_20]) ).

cnf(c_0_35,negated_conjecture,
    ~ p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))))),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_30]) ).

cnf(c_0_36,plain,
    ( s__02(cbool__00,X1) = s__02(cbool__00,cF__00)
    | s__02(cbool__00,X1) = s__02(cbool__00,cT__00) ),
    inference(split_conjunct,[status(thm)],[c_0_31]) ).

fof(c_0_37,plain,
    ~ p__01(s__02(cbool__00,cF__00)),
    inference(fof_nnf,[status(thm)],[c_0_32]) ).

fof(c_0_38,plain,
    ! [X59,X60,X61] : s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X59),s__02(c_27type_2enum_2enum_27__00,X60))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X59),s__02(c_27type_2enum_2enum_27__00,X61))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X60),s__02(c_27type_2enum_2enum_27__00,X61))),
    inference(variable_rename,[status(thm)],['thm.arithmetic.ADD_MONO_LESS_EQ']) ).

fof(c_0_39,plain,
    ! [X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81,X82,X83,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100,X101,X102,X103,X104,X105] :
      ( p__01(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))
      & ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))
      & s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X105))))) = s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,X105)))
      & s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X104))))) = s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,X104)))
      & s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X102))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X103))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X103),s__02(c_27type_2enum_2enum_27__00,X102)))
      & ( p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X101))))
        | s__02(c_27type_2enum_2enum_27__00,X101) != s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) )
      & ( s__02(c_27type_2enum_2enum_27__00,X101) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
        | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X101)))) )
      & s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X100),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,cT__00)
      & s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X98))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X99))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X98),s__02(c_27type_2enum_2enum_27__00,X99)))
      & s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X97))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X97),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))
      & s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X96))) = s__02(cbool__00,cT__00)
      & s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X94))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X95))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X95),s__02(c_27type_2enum_2enum_27__00,X94)))
      & s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X93))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,X93)))
      & s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X92))) = s__02(cbool__00,cF__00)
      & s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X90))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X91))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X90),s__02(c_27type_2enum_2enum_27__00,X91)))
      & s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X89))))) = s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,X89)))
      & s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,X88),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(cbool__00,cF__00)
      & ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X86))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X87)))
        | s__02(c_27type_2enum_2enum_27__00,X86) != s__02(c_27type_2enum_2enum_27__00,X87) )
      & ( s__02(c_27type_2enum_2enum_27__00,X86) = s__02(c_27type_2enum_2enum_27__00,X87)
        | s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X86))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X87))) )
      & ( s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X85)))
        | s__02(c_27type_2enum_2enum_27__00,X85) != s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00) )
      & ( s__02(c_27type_2enum_2enum_27__00,X85) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)
        | s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) != s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X85))) )
      & ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X84))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
        | s__02(c_27type_2enum_2enum_27__00,X84) != s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00) )
      & ( s__02(c_27type_2enum_2enum_27__00,X84) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)
        | s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X84))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00) )
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X83))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,X83)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X82))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X82)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X80))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X81))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,X80),s__02(c_27type_2enum_2enum_27__00,X81)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,X79),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,X78))))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,X77))))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X75))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X76))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,X75),s__02(c_27type_2enum_2enum_27__00,X76)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,X74),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X74)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X73))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X71))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X72))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,X71),s__02(c_27type_2enum_2enum_27__00,X72)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,X70),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X69))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X67))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,X68))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X67),s__02(c_27type_2enum_2enum_27__00,X68)))))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X66),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X66)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X65))) = s__02(c_27type_2enum_2enum_27__00,X65) ),
    inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])]) ).

fof(c_0_40,plain,
    ! [X47,X48] :
      ( s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X48),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X47))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X48),s__02(c_27type_2enum_2enum_27__00,X47)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,X48))),s__02(c_27type_2enum_2enum_27__00,X47))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X48),s__02(c_27type_2enum_2enum_27__00,X47)))))
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X48),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X48)
      & s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X48))) = s__02(c_27type_2enum_2enum_27__00,X48) ),
    inference(variable_rename,[status(thm)],['thm.arithmetic.ADD_CLAUSES']) ).

cnf(c_0_41,negated_conjecture,
    ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0)))
    | p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))))) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_24]),c_0_25])]) ).

cnf(c_0_42,negated_conjecture,
    s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(esk2_0,cfun__02(esk3_0,cbool__00)),esk7_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))) = s__02(cbool__00,cF__00),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_25])]) ).

cnf(c_0_43,plain,
    ~ p__01(s__02(cbool__00,cF__00)),
    inference(split_conjunct,[status(thm)],[c_0_37]) ).

fof(c_0_44,plain,
    ! [X116,X117,X118] :
      ( s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X116),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X117),s__02(c_27type_2elist_2elist_27__01(X116),X118))))) = s__02(c_27type_2enum_2enum_27__00,X117)
      | ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X117),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X116),X118)))))) ),
    inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['thm.list.LENGTH_TAKE'])])]) ).

cnf(c_0_45,plain,
    s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X2))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X3))))) = s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X2),s__02(c_27type_2enum_2enum_27__00,X3))),
    inference(split_conjunct,[status(thm)],[c_0_38]) ).

cnf(c_0_46,plain,
    s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),
    inference(split_conjunct,[status(thm)],[c_0_39]) ).

cnf(c_0_47,plain,
    s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))) = s__02(c_27type_2enum_2enum_27__00,X1),
    inference(split_conjunct,[status(thm)],[c_0_40]) ).

cnf(c_0_48,plain,
    s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,X1))) = s__02(cbool__00,cT__00),
    inference(split_conjunct,[status(thm)],[c_0_39]) ).

fof(c_0_49,plain,
    ! [X108,X109,X110] : s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X108),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X108),X109),s__02(c_27type_2elist_2elist_27__01(X108),X110))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X108),X109))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X108),X110))))),
    inference(variable_rename,[status(thm)],['thm.list.LENGTH_APPEND']) ).

cnf(c_0_50,negated_conjecture,
    s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk3_0),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))) != s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_42]),c_0_43]) ).

cnf(c_0_51,plain,
    ( ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),X3))))))
    | s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X2),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2elist_2elist_27__01(X2),X3))))) = s__02(c_27type_2enum_2enum_27__00,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_44]) ).

cnf(c_0_52,plain,
    s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,X1),s__02(c_27type_2enum_2enum_27__00,X2))))) = s__02(cbool__00,cT__00),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47]),c_0_48]) ).

cnf(c_0_53,plain,
    s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),X2),s__02(c_27type_2elist_2elist_27__01(X1),X3))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X2))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X3))))),
    inference(split_conjunct,[status(thm)],[c_0_49]) ).

cnf(c_0_54,negated_conjecture,
    ~ p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0)))))),
    inference(spm,[status(thm)],[c_0_50,c_0_51]) ).

cnf(c_0_55,plain,
    ( ~ p__01(s__02(cbool__00,X1))
    | s__02(cbool__00,X1) != s__02(cbool__00,cF__00) ),
    inference(split_conjunct,[status(thm)],[c_0_17]) ).

cnf(c_0_56,plain,
    s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),X2))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(X1),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(X1),X2),s__02(c_27type_2elist_2elist_27__01(X1),X3))))))) = s__02(cbool__00,cT__00),
    inference(spm,[status(thm)],[c_0_52,c_0_53]) ).

cnf(c_0_57,negated_conjecture,
    s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0),s__02(c_27type_2elist_2elist_27__01(esk2_0),esk5_0))))) = s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_24]),c_0_25])]) ).

cnf(c_0_58,negated_conjecture,
    s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk2_0),esk4_0))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(esk3_0),esk6_0))))) = s__02(cbool__00,cF__00),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_36]),c_0_25])]) ).

cnf(c_0_59,plain,
    s__02(cbool__00,cT__00) != s__02(cbool__00,cF__00),
    inference(spm,[status(thm)],[c_0_55,c_0_25]) ).

cnf(c_0_60,negated_conjecture,
    $false,
    inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_58]),c_0_59]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWW900+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05  % Command  : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/10.39  % Computer : n018.cluster.edu
% 0.13/10.39  % Model    : x86_64 x86_64
% 0.13/10.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.39  % Memory   : 8046.5625MB
% 0.13/10.39  % OS       : Linux 6.8.0-71-generic
% 0.13/10.39  % CPULimit : 300
% 0.13/10.39  % WCLimit  : 300
% 0.13/10.39  % DateTime : Mon Sep 21 10:18:24 UTC 2026
% 0.13/10.40  % CPUTime  : 
% 0.13/10.40  Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/10.44  Running first-order theorem proving
% 0.16/10.44  Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 103.94/25.64  % Version: 3.5.1
% 103.94/25.64  % Preprocessing class: FSLSSMSSSSSNFFN.
% 103.94/25.64  % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 103.94/25.64  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 103.94/25.64  % Starting new_bool_3 with 300s (1) cores
% 103.94/25.64  % Starting new_bool_1 with 300s (1) cores
% 103.94/25.64  % Starting sh5l with 300s (1) cores
% 103.94/25.64  % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 1631372 completed with status 0
% 103.94/25.64  % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 103.94/25.64  % Preprocessing class: FSLSSMSSSSSNFFN.
% 103.94/25.64  % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 103.94/25.64  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 103.94/25.64  % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 103.94/25.64  % No SInE strategy applied
% 103.94/25.64  % Search class: FGHSM-FFLM31-DFFFFFNN
% 103.94/25.64  % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 103.94/25.64  % Starting SubtermCWHack with 136s (1) cores
% 103.94/25.64  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 103.94/25.64  % Starting new_bool_3 with 311s (1) cores
% 103.94/25.64  % Starting new_bool_1 with 308s (1) cores
% 103.94/25.64  % Starting sh5l with 304s (1) cores
% 103.94/25.64  % sh5l with pid 1631383 completed with status 0
% 103.94/25.64  % Result found by sh5l
% 103.94/25.64  % Preprocessing class: FSLSSMSSSSSNFFN.
% 103.94/25.64  % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 103.94/25.64  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 103.94/25.64  % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 103.94/25.64  % No SInE strategy applied
% 103.94/25.64  % Search class: FGHSM-FFLM31-DFFFFFNN
% 103.94/25.64  % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 103.94/25.64  % Starting SubtermCWHack with 136s (1) cores
% 103.94/25.64  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 103.94/25.64  % Starting new_bool_3 with 311s (1) cores
% 103.94/25.64  % Starting new_bool_1 with 308s (1) cores
% 103.94/25.64  % Starting sh5l with 304s (1) cores
% 103.94/25.64  % Preprocessing time       : 0.003 s
% 103.94/25.64  % Presaturation interreduction done
% 103.94/25.64  
% 103.94/25.64  % Proof found!
% 103.94/25.64  % SZS status Theorem
% 103.94/25.64  % SZS output start CNFRefutation
% See solution above
% 103.94/25.65  % Parsed axioms                        : 31
% 103.94/25.65  % Removed by relevancy pruning/SinE    : 0
% 103.94/25.65  % Initial clauses                      : 118
% 103.94/25.65  % Removed in clause preprocessing      : 23
% 103.94/25.65  % Initial clauses in saturation        : 95
% 103.94/25.65  % Processed clauses                    : 53884
% 103.94/25.65  % ...of these trivial                  : 588
% 103.94/25.65  % ...subsumed                          : 51742
% 103.94/25.65  % ...remaining for further processing  : 1554
% 103.94/25.65  % Other redundant clauses eliminated   : 0
% 103.94/25.65  % Clauses deleted for lack of memory   : 0
% 103.94/25.65  % Backward-subsumed                    : 233
% 103.94/25.65  % Backward-rewritten                   : 133
% 103.94/25.65  % Generated clauses                    : 480656
% 103.94/25.65  % ...of the previous two non-redundant : 381997
% 103.94/25.65  % ...aggressively subsumed             : 0
% 103.94/25.65  % Contextual simplify-reflections      : 5
% 103.94/25.65  % Paramodulations                      : 480411
% 103.94/25.65  % Factorizations                       : 116
% 103.94/25.65  % NegExts                              : 0
% 103.94/25.65  % Equation resolutions                 : 129
% 103.94/25.65  % Disequality decompositions           : 0
% 103.94/25.65  % Total rewrite steps                  : 522868
% 103.94/25.65  % ...of those cached                   : 464822
% 103.94/25.65  % Propositional unsat checks           : 0
% 103.94/25.65  %    Propositional check models        : 0
% 103.94/25.65  %    Propositional check unsatisfiable : 0
% 103.94/25.65  %    Propositional clauses             : 0
% 103.94/25.65  %    Propositional clauses after purity: 0
% 103.94/25.65  %    Propositional unsat core size     : 0
% 103.94/25.65  %    Propositional preprocessing time  : 0.000
% 103.94/25.65  %    Propositional encoding time       : 0.000
% 103.94/25.65  %    Propositional solver time         : 0.000
% 103.94/25.65  %    Success case prop preproc time    : 0.000
% 103.94/25.65  %    Success case prop encoding time   : 0.000
% 103.94/25.65  %    Success case prop solver time     : 0.000
% 103.94/25.65  % Current number of processed clauses  : 1114
% 103.94/25.65  %    Positive orientable unit clauses  : 222
% 103.94/25.65  %    Positive unorientable unit clauses: 23
% 103.94/25.65  %    Negative unit clauses             : 287
% 103.94/25.65  %    Non-unit-clauses                  : 582
% 103.94/25.65  % Current number of unprocessed clauses: 321711
% 103.94/25.65  % ...number of literals in the above   : 644474
% 103.94/25.65  % Current number of archived formulas  : 0
% 103.94/25.65  % Current number of archived clauses   : 440
% 103.94/25.65  % Clause-clause subsumption calls (NU) : 306407
% 103.94/25.65  % Rec. Clause-clause subsumption calls : 244946
% 103.94/25.65  % Non-unit clause-clause subsumptions  : 17779
% 103.94/25.65  % Unit Clause-clause subsumption calls : 19339
% 103.94/25.65  % Rewrite failures with RHS unbound    : 0
% 103.94/25.65  % BW rewrite match attempts            : 15115
% 103.94/25.65  % BW rewrite match successes           : 154
% 103.94/25.65  % Condensation attempts                : 53884
% 103.94/25.65  % Condensation successes               : 8424
% 103.94/25.65  % Termbank termtop insertions          : 17089528
% 103.94/25.65  % Search garbage collected termcells   : 771
% 103.94/25.65  
% 103.94/25.65  % -------------------------------------------------
% 103.94/25.65  % User time                : 14.338 s
% 103.94/25.65  % System time              : 0.396 s
% 103.94/25.65  % Total time               : 14.734 s
% 103.94/25.65  % Maximum resident set size: 3736 pages
% 103.94/25.65  
% 103.94/25.65  % -------------------------------------------------
% 103.94/25.65  % User time                : 72.227 s
% 103.94/25.65  % System time              : 2.186 s
% 103.94/25.65  % Total time               : 74.412 s
% 103.94/25.65  % Maximum resident set size: 4864 pages
% 103.94/25.65  % E exiting
%------------------------------------------------------------------------------