CSE_E---1.7.THM-CRf.s

%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : ITP020+1 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 04:32:41 PM UTC 2026

% Result   : Theorem 0.71s 1.62s
% Output   : CNFRefutation 0.71s
% Verified : 
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_47)

% Comments : 
%------------------------------------------------------------------------------
fof(thm_2Esat_2Edc__eq,axiom,
    ! [X34,X35,X36] :
      ( ( p(s(tyop_2Emin_2Ebool,X36))
      <=> s(tyop_2Emin_2Ebool,X35) = s(tyop_2Emin_2Ebool,X34) )
    <=> ( ( p(s(tyop_2Emin_2Ebool,X36))
          | p(s(tyop_2Emin_2Ebool,X35))
          | p(s(tyop_2Emin_2Ebool,X34)) )
        & ( p(s(tyop_2Emin_2Ebool,X36))
          | ~ p(s(tyop_2Emin_2Ebool,X34))
          | ~ p(s(tyop_2Emin_2Ebool,X35)) )
        & ( p(s(tyop_2Emin_2Ebool,X35))
          | ~ p(s(tyop_2Emin_2Ebool,X34))
          | ~ p(s(tyop_2Emin_2Ebool,X36)) )
        & ( p(s(tyop_2Emin_2Ebool,X34))
          | ~ p(s(tyop_2Emin_2Ebool,X35))
          | ~ p(s(tyop_2Emin_2Ebool,X36)) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Esat_2Edc__eq) ).

fof(thm_2Eutil__prob_2ENUM__2D__BIJ__INV,conjecture,
    ? [X3] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X3),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).

fof(thm_2Ebool_2ENOT__EXISTS__THM,axiom,
    ! [X1,X18] :
      ( ~ ? [X12] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X12))))
    <=> ! [X5] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X5)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__EXISTS__THM) ).

fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom,
    ! [X13] :
      ( ~ p(s(tyop_2Emin_2Ebool,X13))
    <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X13)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_7E_2E1) ).

fof(reserved_2Elogic_2E_7E,axiom,
    ! [X6] :
      ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X6))))
    <=> ~ p(s(tyop_2Emin_2Ebool,X6)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_7E) ).

fof(thm_2Ebool_2EIMP__CLAUSES,axiom,
    ! [X8] :
      ( ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
         => p(s(tyop_2Emin_2Ebool,X8)) )
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
      & ( ( p(s(tyop_2Emin_2Ebool,X8))
         => p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
         => p(s(tyop_2Emin_2Ebool,X8)) )
      <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ( p(s(tyop_2Emin_2Ebool,X8))
         => p(s(tyop_2Emin_2Ebool,X8)) )
      <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ( p(s(tyop_2Emin_2Ebool,X8))
         => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
      <=> ~ p(s(tyop_2Emin_2Ebool,X8)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__CLAUSES) ).

fof(thm_2Ebool_2EIMP__F,axiom,
    ! [X8] :
      ( ( p(s(tyop_2Emin_2Ebool,X8))
       => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
     => ~ p(s(tyop_2Emin_2Ebool,X8)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__F) ).

fof(thm_2Ebool_2EEQ__CLAUSES,axiom,
    ! [X8] :
      ( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X8)
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
      & ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
      & ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X8)
      <=> ~ p(s(tyop_2Emin_2Ebool,X8)) )
      & ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
      <=> ~ p(s(tyop_2Emin_2Ebool,X8)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).

fof(thm_2Ebool_2ENOT__CLAUSES,axiom,
    ( ! [X8] :
        ( ~ ~ p(s(tyop_2Emin_2Ebool,X8))
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
    & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
    & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__CLAUSES) ).

fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,axiom,
    ! [X13,X14,X15] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X13),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X14),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X15))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X13))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X14))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X15))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29) ).

fof(thm_2Ebool_2ESKOLEM__THM,axiom,
    ! [X1,X2,X18] :
      ( ! [X12] :
        ? [X25] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool)),X18),s(X1,X12))),s(X2,X25))))
    <=> ? [X26] :
        ! [X27] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool)),X18),s(X1,X27))),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X26),s(X1,X27)))))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ESKOLEM__THM) ).

fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,axiom,
    ! [X13,X14,X15] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X13),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X14),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X15))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X13))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X14))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X15))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum) ).

fof(reserved_2Eho_2Es__thm,axiom,
    ! [X1,X2,X11,X3,X4,X5] : s(X11,app_2E2(s(tyop_2Emin_2Efun(X1,X11),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X2),tyop_2Emin_2Efun(X1,X11)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,X11)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X2),tyop_2Emin_2Efun(X1,X11))),combin_s_2E0),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,X11)),X3))),s(tyop_2Emin_2Efun(X1,X2),X4))),s(X1,X5))) = s(X11,app_2E2(s(tyop_2Emin_2Efun(X2,X11),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,X11)),X3),s(X1,X5))),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X4),s(X1,X5))))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Es__thm) ).

fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27b_20mono_2EA_27a,axiom,
    ! [X1,X2,X13,X14,X15] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X2,X1),X13),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X14),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X1),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(X2,X1),X13))),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X14))),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X15))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27b_20mono_2EA_27a) ).

fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27a_20mono_2EA_27b,axiom,
    ! [X1,X2,X13,X14,X15] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X2),X13),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X14),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X15))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(X1,X2),X13))),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X14))),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X15))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27a_20mono_2EA_27b) ).

fof(arityeq2_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,axiom,
    ! [X13,X14] : s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X13),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X14))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool))),c_2Epred__set_2ECROSS_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X13))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X14))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum) ).

fof(reserved_2Eho_2Eeq__ext,axiom,
    ! [X1,X2,X3,X4] :
      ( ! [X5] : s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(X1,X5))) = s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X4),s(X1,X5)))
     => s(tyop_2Emin_2Efun(X1,X2),X3) = s(tyop_2Emin_2Efun(X1,X2),X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Eeq__ext) ).

fof(thm_2Epred__set_2EBIJ__SYM,axiom,
    ! [X1,X2,X28,X29] :
      ( ? [X30] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X2),X30),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X28),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X29))))
    <=> ? [X31] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X2,X1),X31),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X29),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X28)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Epred__set_2EBIJ__SYM) ).

fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom,
    ! [X1,X13,X14] :
      ( s(X1,X13) = s(X1,X14)
    <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X1,X13))),s(X1,X14)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a) ).

fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom,
    ! [X13,X14] :
      ( ( p(s(tyop_2Emin_2Ebool,X13))
       => p(s(tyop_2Emin_2Ebool,X14)) )
    <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X13))),s(tyop_2Emin_2Ebool,X14)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2) ).

fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom,
    ! [X13,X14] :
      ( ( p(s(tyop_2Emin_2Ebool,X13))
        | p(s(tyop_2Emin_2Ebool,X14)) )
    <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X13))),s(tyop_2Emin_2Ebool,X14)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Ebool_2E_5C_2F_2E2) ).

fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom,
    ! [X13,X14] :
      ( ( p(s(tyop_2Emin_2Ebool,X13))
        & p(s(tyop_2Emin_2Ebool,X14)) )
    <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X13))),s(tyop_2Emin_2Ebool,X14)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Ebool_2E_2F_5C_2E2) ).

fof(thm_2Eutil__prob_2ENUM__2D__BIJ,axiom,
    ? [X3] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X3),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eutil__prob_2ENUM__2D__BIJ) ).

fof(thm_2Ebool_2ERIGHT__AND__FORALL__THM,axiom,
    ! [X1,X18,X19] :
      ( ( p(s(tyop_2Emin_2Ebool,X18))
        & ! [X5] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X5)))) )
    <=> ! [X20] :
          ( p(s(tyop_2Emin_2Ebool,X18))
          & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ERIGHT__AND__FORALL__THM) ).

fof(thm_2Ebool_2ELEFT__AND__FORALL__THM,axiom,
    ! [X1,X18,X19] :
      ( ( ! [X5] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X5))))
        & p(s(tyop_2Emin_2Ebool,X19)) )
    <=> ! [X20] :
          ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X20))))
          & p(s(tyop_2Emin_2Ebool,X19)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ELEFT__AND__FORALL__THM) ).

fof(thm_2Ebool_2ERIGHT__FORALL__OR__THM,axiom,
    ! [X1,X18,X19] :
      ( ! [X5] :
          ( p(s(tyop_2Emin_2Ebool,X18))
          | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X5)))) )
    <=> ( p(s(tyop_2Emin_2Ebool,X18))
        | ! [X20] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ERIGHT__FORALL__OR__THM) ).

fof(thm_2Ebool_2ELEFT__FORALL__OR__THM,axiom,
    ! [X1,X21,X22] :
      ( ! [X5] :
          ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X22),s(X1,X5))))
          | p(s(tyop_2Emin_2Ebool,X21)) )
    <=> ( ! [X20] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X22),s(X1,X20))))
        | p(s(tyop_2Emin_2Ebool,X21)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ELEFT__FORALL__OR__THM) ).

fof(thm_2Ebool_2ERIGHT__EXISTS__AND__THM,axiom,
    ! [X1,X18,X19] :
      ( ? [X5] :
          ( p(s(tyop_2Emin_2Ebool,X18))
          & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X5)))) )
    <=> ( p(s(tyop_2Emin_2Ebool,X18))
        & ? [X20] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ERIGHT__EXISTS__AND__THM) ).

fof(thm_2Ebool_2ELEFT__EXISTS__AND__THM,axiom,
    ! [X1,X18,X19] :
      ( ? [X5] :
          ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X5))))
          & p(s(tyop_2Emin_2Ebool,X19)) )
    <=> ( ? [X20] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X20))))
        & p(s(tyop_2Emin_2Ebool,X19)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ELEFT__EXISTS__AND__THM) ).

fof(thm_2Ebool_2ERIGHT__OR__EXISTS__THM,axiom,
    ! [X1,X18,X19] :
      ( ( p(s(tyop_2Emin_2Ebool,X18))
        | ? [X5] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X5)))) )
    <=> ? [X20] :
          ( p(s(tyop_2Emin_2Ebool,X18))
          | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X19),s(X1,X20)))) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ERIGHT__OR__EXISTS__THM) ).

fof(thm_2Ebool_2ELEFT__OR__EXISTS__THM,axiom,
    ! [X1,X18,X19] :
      ( ( ? [X5] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X5))))
        | p(s(tyop_2Emin_2Ebool,X19)) )
    <=> ? [X20] :
          ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X20))))
          | p(s(tyop_2Emin_2Ebool,X19)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ELEFT__OR__EXISTS__THM) ).

fof(reserved_2Eho_2Ek__thm,axiom,
    ! [X1,X2,X9,X10] : s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,X1)),combin_k_2E0),s(X1,X9))),s(X2,X10))) = s(X1,X9),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ek__thm) ).

fof(reserved_2Equant_2E_21,axiom,
    ! [X1,X3] :
      ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))
    <=> ! [X12] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X12)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Equant_2E_21) ).

fof(reserved_2Equant_2E_3F,axiom,
    ! [X1,X3] :
      ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))
    <=> ? [X12] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,X12)))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Equant_2E_3F) ).

fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom,
    ! [X1,X13] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a) ).

fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom,
    ! [X1,X13] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X13))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a) ).

fof(reserved_2Elogic_2E_3D_3D_3E,axiom,
    ! [X6,X7] :
      ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X6),s(tyop_2Emin_2Ebool,X7))))
    <=> ( p(s(tyop_2Emin_2Ebool,X6))
       => p(s(tyop_2Emin_2Ebool,X7)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_3D_3D_3E) ).

fof(reserved_2Elogic_2E_3D,axiom,
    ! [X1,X6,X7] :
      ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X1,X6),s(X1,X7))))
    <=> s(X1,X6) = s(X1,X7) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_3D) ).

fof(reserved_2Elogic_2E_5C_2F,axiom,
    ! [X6,X7] :
      ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X6),s(tyop_2Emin_2Ebool,X7))))
    <=> ( p(s(tyop_2Emin_2Ebool,X6))
        | p(s(tyop_2Emin_2Ebool,X7)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_5C_2F) ).

fof(reserved_2Elogic_2E_2F_5C,axiom,
    ! [X6,X7] :
      ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X6),s(tyop_2Emin_2Ebool,X7))))
    <=> ( p(s(tyop_2Emin_2Ebool,X6))
        & p(s(tyop_2Emin_2Ebool,X7)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_2F_5C) ).

fof(reserved_2Eho_2Ei__thm,axiom,
    ! [X1,X9] : s(X1,app_2E2(s(tyop_2Emin_2Efun(X1,X1),combin_i_2E0),s(X1,X9))) = s(X1,X9),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ei__thm) ).

fof(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
    ! [X16,X17] :
      ( ( p(s(tyop_2Emin_2Ebool,X16))
       => p(s(tyop_2Emin_2Ebool,X17)) )
     => ( ( p(s(tyop_2Emin_2Ebool,X17))
         => p(s(tyop_2Emin_2Ebool,X16)) )
       => s(tyop_2Emin_2Ebool,X16) = s(tyop_2Emin_2Ebool,X17) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__ANTISYM__AX) ).

fof(reserved_2Eho_2Eboolext,axiom,
    ! [X6,X7] :
      ( ( p(s(tyop_2Emin_2Ebool,X6))
      <=> p(s(tyop_2Emin_2Ebool,X7)) )
     => s(tyop_2Emin_2Ebool,X6) = s(tyop_2Emin_2Ebool,X7) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Eboolext) ).

fof(reserved_2Eho_2Ebool__cases__ax,axiom,
    ! [X8] :
      ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
      | s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ebool__cases__ax) ).

fof(reserved_2Eho_2Enotfalse,axiom,
    ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Enotfalse) ).

fof(thm_2Ebool_2ETRUTH,axiom,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH) ).

fof(reserved_2Eho_2Etruth,axiom,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Etruth) ).

fof(i_0_47,plain,
    ! [X34,X35,X36] :
      ( epred1_3(X36,X35,X34)
    <=> ( ( p(s(tyop_2Emin_2Ebool,X36))
          | p(s(tyop_2Emin_2Ebool,X35))
          | p(s(tyop_2Emin_2Ebool,X34)) )
        & ( p(s(tyop_2Emin_2Ebool,X36))
          | ~ p(s(tyop_2Emin_2Ebool,X34))
          | ~ p(s(tyop_2Emin_2Ebool,X35)) )
        & ( p(s(tyop_2Emin_2Ebool,X35))
          | ~ p(s(tyop_2Emin_2Ebool,X34))
          | ~ p(s(tyop_2Emin_2Ebool,X36)) ) ) ),
    introduced(definition) ).

fof(i_0_48,plain,
    ! [X34,X35,X36] :
      ( ( p(s(tyop_2Emin_2Ebool,X36))
      <=> s(tyop_2Emin_2Ebool,X35) = s(tyop_2Emin_2Ebool,X34) )
    <=> ( epred1_3(X36,X35,X34)
        & ( p(s(tyop_2Emin_2Ebool,X34))
          | ~ p(s(tyop_2Emin_2Ebool,X35))
          | ~ p(s(tyop_2Emin_2Ebool,X36)) ) ) ),
    inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[thm_2Esat_2Edc__eq]),c_0_47]) ).

fof(i_0_49,negated_conjecture,
    ~ ? [X3] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X3),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))),
    inference(assume_negation,[status(cth)],[thm_2Eutil__prob_2ENUM__2D__BIJ__INV]) ).

fof(i_0_50,plain,
    ! [X1,X18] :
      ( ~ ? [X12] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X12))))
    <=> ! [X5] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X18),s(X1,X5)))) ),
    inference(fof_simplification,[status(thm)],[thm_2Ebool_2ENOT__EXISTS__THM]) ).

fof(i_0_51,plain,
    ! [X13] :
      ( ~ p(s(tyop_2Emin_2Ebool,X13))
    <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X13)))) ),
    inference(fof_simplification,[status(thm)],[arityeq1_2Ec_2Ebool_2E_7E_2E1]) ).

fof(i_0_52,plain,
    ! [X6] :
      ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X6))))
    <=> ~ p(s(tyop_2Emin_2Ebool,X6)) ),
    inference(fof_simplification,[status(thm)],[reserved_2Elogic_2E_7E]) ).

fof(i_0_53,plain,
    ! [X404,X405,X406] :
      ( ( epred1_3(X406,X405,X404)
        | ~ p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) != s(tyop_2Emin_2Ebool,X404) )
      & ( p(s(tyop_2Emin_2Ebool,X404))
        | ~ p(s(tyop_2Emin_2Ebool,X405))
        | ~ p(s(tyop_2Emin_2Ebool,X406))
        | ~ p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) != s(tyop_2Emin_2Ebool,X404) )
      & ( epred1_3(X406,X405,X404)
        | p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) = s(tyop_2Emin_2Ebool,X404) )
      & ( p(s(tyop_2Emin_2Ebool,X404))
        | ~ p(s(tyop_2Emin_2Ebool,X405))
        | ~ p(s(tyop_2Emin_2Ebool,X406))
        | p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) = s(tyop_2Emin_2Ebool,X404) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) = s(tyop_2Emin_2Ebool,X404)
        | ~ p(s(tyop_2Emin_2Ebool,X404))
        | ~ epred1_3(X406,X405,X404) )
      & ( s(tyop_2Emin_2Ebool,X405) != s(tyop_2Emin_2Ebool,X404)
        | p(s(tyop_2Emin_2Ebool,X406))
        | ~ p(s(tyop_2Emin_2Ebool,X404))
        | ~ epred1_3(X406,X405,X404) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) = s(tyop_2Emin_2Ebool,X404)
        | p(s(tyop_2Emin_2Ebool,X405))
        | ~ epred1_3(X406,X405,X404) )
      & ( s(tyop_2Emin_2Ebool,X405) != s(tyop_2Emin_2Ebool,X404)
        | p(s(tyop_2Emin_2Ebool,X406))
        | p(s(tyop_2Emin_2Ebool,X405))
        | ~ epred1_3(X406,X405,X404) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X406))
        | s(tyop_2Emin_2Ebool,X405) = s(tyop_2Emin_2Ebool,X404)
        | p(s(tyop_2Emin_2Ebool,X406))
        | ~ epred1_3(X406,X405,X404) )
      & ( s(tyop_2Emin_2Ebool,X405) != s(tyop_2Emin_2Ebool,X404)
        | p(s(tyop_2Emin_2Ebool,X406))
        | p(s(tyop_2Emin_2Ebool,X406))
        | ~ epred1_3(X406,X405,X404) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])])]) ).

fof(i_0_54,plain,
    ! [X420,X421,X422] :
      ( ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | ~ epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X421))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X422))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X420))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X421))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X420))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) )
      & ( p(s(tyop_2Emin_2Ebool,X422))
        | p(s(tyop_2Emin_2Ebool,X421))
        | ~ p(s(tyop_2Emin_2Ebool,X420))
        | epred1_3(X422,X421,X420) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_47])])]) ).

fof(i_0_55,plain,
    ! [X8] :
      ( ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
         => p(s(tyop_2Emin_2Ebool,X8)) )
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
      & ( ( p(s(tyop_2Emin_2Ebool,X8))
         => p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
         => p(s(tyop_2Emin_2Ebool,X8)) )
      <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
      & ( ( p(s(tyop_2Emin_2Ebool,X8))
         => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
      <=> ~ p(s(tyop_2Emin_2Ebool,X8)) ) ),
    inference(fof_simplification,[status(thm)],[thm_2Ebool_2EIMP__CLAUSES]) ).

fof(i_0_56,plain,
    ! [X8] :
      ( ( p(s(tyop_2Emin_2Ebool,X8))
       => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
     => ~ p(s(tyop_2Emin_2Ebool,X8)) ),
    inference(fof_simplification,[status(thm)],[thm_2Ebool_2EIMP__F]) ).

fof(i_0_57,plain,
    ! [X8] :
      ( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X8)
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
      & ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
      <=> p(s(tyop_2Emin_2Ebool,X8)) )
      & ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X8)
      <=> ~ p(s(tyop_2Emin_2Ebool,X8)) )
      & ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
      <=> ~ p(s(tyop_2Emin_2Ebool,X8)) ) ),
    inference(fof_simplification,[status(thm)],[thm_2Ebool_2EEQ__CLAUSES]) ).

fof(i_0_58,plain,
    ( ! [X8] : $true
    & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
    & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ),
    inference(fof_simplification,[status(thm)],[thm_2Ebool_2ENOT__CLAUSES]) ).

fof(i_0_59,plain,
    ! [X265,X266,X267] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X265),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X266),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X267))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X265))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X266))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X267))),
    inference(variable_rename,[status(thm)],[arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29]) ).

fof(i_0_60,plain,
    ! [X372,X373,X374,X376,X378,X379,X380,X381,X382,X384] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X373,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X372,tyop_2Emin_2Efun(X373,tyop_2Emin_2Ebool)),X374),s(X372,esk22_3(X372,X373,X374)))),s(X373,X376))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X373,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X372,tyop_2Emin_2Efun(X373,tyop_2Emin_2Ebool)),X374),s(X372,X378))),s(X373,app_2E2(s(tyop_2Emin_2Efun(X372,X373),esk23_3(X372,X373,X374)),s(X372,X378)))))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X380,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X379,tyop_2Emin_2Efun(X380,tyop_2Emin_2Ebool)),X381),s(X379,esk24_4(X379,X380,X381,X382)))),s(X380,app_2E2(s(tyop_2Emin_2Efun(X379,X380),X382),s(X379,esk24_4(X379,X380,X381,X382)))))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X380,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X379,tyop_2Emin_2Efun(X380,tyop_2Emin_2Ebool)),X381),s(X379,X384))),s(X380,esk25_4(X379,X380,X381,X384))))) ) ),
    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_2Ebool_2ESKOLEM__THM])])])])]) ).

fof(i_0_61,plain,
    ! [X270,X271,X272] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X270),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X271),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X272))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X270))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X271))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X272))),
    inference(variable_rename,[status(thm)],[arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum]) ).

fof(i_0_62,plain,
    ! [X213,X214,X215,X216,X217,X218] : s(X215,app_2E2(s(tyop_2Emin_2Efun(X213,X215),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X213,X214),tyop_2Emin_2Efun(X213,X215)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X213,tyop_2Emin_2Efun(X214,X215)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X213,X214),tyop_2Emin_2Efun(X213,X215))),combin_s_2E0),s(tyop_2Emin_2Efun(X213,tyop_2Emin_2Efun(X214,X215)),X216))),s(tyop_2Emin_2Efun(X213,X214),X217))),s(X213,X218))) = s(X215,app_2E2(s(tyop_2Emin_2Efun(X214,X215),app_2E2(s(tyop_2Emin_2Efun(X213,tyop_2Emin_2Efun(X214,X215)),X216),s(X213,X218))),s(X214,app_2E2(s(tyop_2Emin_2Efun(X213,X214),X217),s(X213,X218))))),
    inference(variable_rename,[status(thm)],[reserved_2Eho_2Es__thm]) ).

fof(i_0_63,plain,
    ! [X260,X261,X262,X263,X264] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X261,X260),X262),s(tyop_2Emin_2Efun(X261,tyop_2Emin_2Ebool),X263),s(tyop_2Emin_2Efun(X260,tyop_2Emin_2Ebool),X264))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X260,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X261,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X260,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X261,X260),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X261,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X260,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(X261,X260),X262))),s(tyop_2Emin_2Efun(X261,tyop_2Emin_2Ebool),X263))),s(tyop_2Emin_2Efun(X260,tyop_2Emin_2Ebool),X264))),
    inference(variable_rename,[status(thm)],[arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27b_20mono_2EA_27a]) ).

fof(i_0_64,plain,
    ! [X255,X256,X257,X258,X259] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X255,X256),X257),s(tyop_2Emin_2Efun(X255,tyop_2Emin_2Ebool),X258),s(tyop_2Emin_2Efun(X256,tyop_2Emin_2Ebool),X259))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X256,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X255,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X256,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X255,X256),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X255,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X256,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(X255,X256),X257))),s(tyop_2Emin_2Efun(X255,tyop_2Emin_2Ebool),X258))),s(tyop_2Emin_2Efun(X256,tyop_2Emin_2Ebool),X259))),
    inference(variable_rename,[status(thm)],[arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27a_20mono_2EA_27b]) ).

fof(i_0_65,plain,
    ! [X268,X269] : s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X268),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X269))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool))),c_2Epred__set_2ECROSS_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X268))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X269))),
    inference(variable_rename,[status(thm)],[arityeq2_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum]) ).

fof(i_0_66,plain,
    ! [X199,X200,X201,X202] :
      ( s(X200,app_2E2(s(tyop_2Emin_2Efun(X199,X200),X201),s(X199,esk1_4(X199,X200,X201,X202)))) != s(X200,app_2E2(s(tyop_2Emin_2Efun(X199,X200),X202),s(X199,esk1_4(X199,X200,X201,X202))))
      | s(tyop_2Emin_2Efun(X199,X200),X201) = s(tyop_2Emin_2Efun(X199,X200),X202) ),
    inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Eho_2Eeq__ext])])]) ).

fof(i_0_67,plain,
    ! [X386,X387,X388,X389,X390,X392,X393,X394,X395,X396] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X386,X387),X390),s(tyop_2Emin_2Efun(X386,tyop_2Emin_2Ebool),X388),s(tyop_2Emin_2Efun(X387,tyop_2Emin_2Ebool),X389))))
        | p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X387,X386),esk26_4(X386,X387,X388,X389)),s(tyop_2Emin_2Efun(X387,tyop_2Emin_2Ebool),X389),s(tyop_2Emin_2Efun(X386,tyop_2Emin_2Ebool),X388)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X393,X392),X396),s(tyop_2Emin_2Efun(X393,tyop_2Emin_2Ebool),X395),s(tyop_2Emin_2Efun(X392,tyop_2Emin_2Ebool),X394))))
        | p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X392,X393),esk27_4(X392,X393,X394,X395)),s(tyop_2Emin_2Efun(X392,tyop_2Emin_2Ebool),X394),s(tyop_2Emin_2Efun(X393,tyop_2Emin_2Ebool),X395)))) ) ),
    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_2Epred__set_2EBIJ__SYM])])])])]) ).

fof(i_0_68,negated_conjecture,
    ! [X419] : ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X419),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))),
    inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_49])]) ).

fof(i_0_69,plain,
    ! [X248,X249,X250] :
      ( ( s(X248,X249) != s(X248,X250)
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X248,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X248,tyop_2Emin_2Efun(X248,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X248,X249))),s(X248,X250)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X248,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X248,tyop_2Emin_2Efun(X248,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X248,X249))),s(X248,X250))))
        | s(X248,X249) = s(X248,X250) ) ),
    inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a])]) ).

fof(i_0_70,plain,
    ! [X246,X247] :
      ( ( p(s(tyop_2Emin_2Ebool,X246))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X246))),s(tyop_2Emin_2Ebool,X247)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X247))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X246))),s(tyop_2Emin_2Ebool,X247)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X246))),s(tyop_2Emin_2Ebool,X247))))
        | ~ p(s(tyop_2Emin_2Ebool,X246))
        | p(s(tyop_2Emin_2Ebool,X247)) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2])])]) ).

fof(i_0_71,plain,
    ! [X243,X244] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,X243))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X243))),s(tyop_2Emin_2Ebool,X244)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X244))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X243))),s(tyop_2Emin_2Ebool,X244)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X243))),s(tyop_2Emin_2Ebool,X244))))
        | p(s(tyop_2Emin_2Ebool,X243))
        | p(s(tyop_2Emin_2Ebool,X244)) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Ebool_2E_5C_2F_2E2])])]) ).

fof(i_0_72,plain,
    ! [X241,X242] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,X241))
        | ~ p(s(tyop_2Emin_2Ebool,X242))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X241))),s(tyop_2Emin_2Ebool,X242)))) )
      & ( p(s(tyop_2Emin_2Ebool,X241))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X241))),s(tyop_2Emin_2Ebool,X242)))) )
      & ( p(s(tyop_2Emin_2Ebool,X242))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X241))),s(tyop_2Emin_2Ebool,X242)))) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Ebool_2E_2F_5C_2E2])])]) ).

fof(i_0_73,plain,
    p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),esk28_0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))),
    inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[thm_2Eutil__prob_2ENUM__2D__BIJ])]) ).

fof(i_0_74,plain,
    ! [X300,X301,X302,X304,X305,X306,X307,X309] :
      ( ( p(s(tyop_2Emin_2Ebool,X301))
        | ~ p(s(tyop_2Emin_2Ebool,X301))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X300,tyop_2Emin_2Ebool),X302),s(X300,esk8_3(X300,X301,X302))))) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X300,tyop_2Emin_2Ebool),X302),s(X300,X304))))
        | ~ p(s(tyop_2Emin_2Ebool,X301))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X300,tyop_2Emin_2Ebool),X302),s(X300,esk8_3(X300,X301,X302))))) )
      & ( p(s(tyop_2Emin_2Ebool,X306))
        | ~ p(s(tyop_2Emin_2Ebool,X306))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X305,tyop_2Emin_2Ebool),X307),s(X305,esk9_3(X305,X306,X307))))) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X305,tyop_2Emin_2Ebool),X307),s(X305,X309))))
        | ~ p(s(tyop_2Emin_2Ebool,X306))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X305,tyop_2Emin_2Ebool),X307),s(X305,esk9_3(X305,X306,X307))))) ) ),
    inference(distribute,[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_2Ebool_2ERIGHT__AND__FORALL__THM])])])])])]) ).

fof(i_0_75,plain,
    ! [X290,X291,X292,X294,X295,X296,X297,X299] :
      ( ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X290,tyop_2Emin_2Ebool),X291),s(X290,X294))))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X290,tyop_2Emin_2Ebool),X291),s(X290,esk6_3(X290,X291,X292)))))
        | ~ p(s(tyop_2Emin_2Ebool,X292)) )
      & ( p(s(tyop_2Emin_2Ebool,X292))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X290,tyop_2Emin_2Ebool),X291),s(X290,esk6_3(X290,X291,X292)))))
        | ~ p(s(tyop_2Emin_2Ebool,X292)) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X295,tyop_2Emin_2Ebool),X296),s(X295,X299))))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X295,tyop_2Emin_2Ebool),X296),s(X295,esk7_3(X295,X296,X297)))))
        | ~ p(s(tyop_2Emin_2Ebool,X297)) )
      & ( p(s(tyop_2Emin_2Ebool,X297))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X295,tyop_2Emin_2Ebool),X296),s(X295,esk7_3(X295,X296,X297)))))
        | ~ p(s(tyop_2Emin_2Ebool,X297)) ) ),
    inference(distribute,[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_2Ebool_2ELEFT__AND__FORALL__THM])])])])])]) ).

fof(i_0_76,plain,
    ! [X360,X361,X362,X364,X365,X366,X367,X369] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,X361))
        | p(s(tyop_2Emin_2Ebool,X361))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X360,tyop_2Emin_2Ebool),X362),s(X360,X364)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X360,tyop_2Emin_2Ebool),X362),s(X360,esk20_3(X360,X361,X362)))))
        | p(s(tyop_2Emin_2Ebool,X361))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X360,tyop_2Emin_2Ebool),X362),s(X360,X364)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X366))
        | p(s(tyop_2Emin_2Ebool,X366))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X365,tyop_2Emin_2Ebool),X367),s(X365,X369)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X365,tyop_2Emin_2Ebool),X367),s(X365,esk21_3(X365,X366,X367)))))
        | p(s(tyop_2Emin_2Ebool,X366))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X365,tyop_2Emin_2Ebool),X367),s(X365,X369)))) ) ),
    inference(distribute,[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_2Ebool_2ERIGHT__FORALL__OR__THM])])])])])]) ).

fof(i_0_77,plain,
    ! [X350,X351,X352,X354,X355,X356,X357,X359] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X350,tyop_2Emin_2Ebool),X352),s(X350,esk18_3(X350,X351,X352)))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X350,tyop_2Emin_2Ebool),X352),s(X350,X354))))
        | p(s(tyop_2Emin_2Ebool,X351)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X351))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X350,tyop_2Emin_2Ebool),X352),s(X350,X354))))
        | p(s(tyop_2Emin_2Ebool,X351)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X355,tyop_2Emin_2Ebool),X357),s(X355,esk19_3(X355,X356,X357)))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X355,tyop_2Emin_2Ebool),X357),s(X355,X359))))
        | p(s(tyop_2Emin_2Ebool,X356)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X356))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X355,tyop_2Emin_2Ebool),X357),s(X355,X359))))
        | p(s(tyop_2Emin_2Ebool,X356)) ) ),
    inference(distribute,[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_2Ebool_2ELEFT__FORALL__OR__THM])])])])])]) ).

fof(i_0_78,plain,
    ! [X340,X341,X342,X343,X345,X346,X347,X348] :
      ( ( p(s(tyop_2Emin_2Ebool,X341))
        | ~ p(s(tyop_2Emin_2Ebool,X341))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X340,tyop_2Emin_2Ebool),X342),s(X340,X343)))) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X340,tyop_2Emin_2Ebool),X342),s(X340,esk16_3(X340,X341,X342)))))
        | ~ p(s(tyop_2Emin_2Ebool,X341))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X340,tyop_2Emin_2Ebool),X342),s(X340,X343)))) )
      & ( p(s(tyop_2Emin_2Ebool,X346))
        | ~ p(s(tyop_2Emin_2Ebool,X346))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X345,tyop_2Emin_2Ebool),X347),s(X345,X348)))) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X345,tyop_2Emin_2Ebool),X347),s(X345,esk17_3(X345,X346,X347)))))
        | ~ p(s(tyop_2Emin_2Ebool,X346))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X345,tyop_2Emin_2Ebool),X347),s(X345,X348)))) ) ),
    inference(distribute,[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_2Ebool_2ERIGHT__EXISTS__AND__THM])])])])])]) ).

fof(i_0_79,plain,
    ! [X330,X331,X332,X333,X335,X336,X337,X338] :
      ( ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X330,tyop_2Emin_2Ebool),X331),s(X330,esk14_3(X330,X331,X332)))))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X330,tyop_2Emin_2Ebool),X331),s(X330,X333))))
        | ~ p(s(tyop_2Emin_2Ebool,X332)) )
      & ( p(s(tyop_2Emin_2Ebool,X332))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X330,tyop_2Emin_2Ebool),X331),s(X330,X333))))
        | ~ p(s(tyop_2Emin_2Ebool,X332)) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X335,tyop_2Emin_2Ebool),X336),s(X335,esk15_3(X335,X336,X337)))))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X335,tyop_2Emin_2Ebool),X336),s(X335,X338))))
        | ~ p(s(tyop_2Emin_2Ebool,X337)) )
      & ( p(s(tyop_2Emin_2Ebool,X337))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X335,tyop_2Emin_2Ebool),X336),s(X335,X338))))
        | ~ p(s(tyop_2Emin_2Ebool,X337)) ) ),
    inference(distribute,[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_2Ebool_2ELEFT__EXISTS__AND__THM])])])])])]) ).

fof(i_0_80,plain,
    ! [X320,X321,X322,X323,X325,X326,X327,X328] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,X321))
        | p(s(tyop_2Emin_2Ebool,X321))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X320,tyop_2Emin_2Ebool),X322),s(X320,esk12_3(X320,X321,X322))))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X320,tyop_2Emin_2Ebool),X322),s(X320,X323))))
        | p(s(tyop_2Emin_2Ebool,X321))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X320,tyop_2Emin_2Ebool),X322),s(X320,esk12_3(X320,X321,X322))))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X326))
        | p(s(tyop_2Emin_2Ebool,X326))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X325,tyop_2Emin_2Ebool),X327),s(X325,esk13_3(X325,X326,X327))))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X325,tyop_2Emin_2Ebool),X327),s(X325,X328))))
        | p(s(tyop_2Emin_2Ebool,X326))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X325,tyop_2Emin_2Ebool),X327),s(X325,esk13_3(X325,X326,X327))))) ) ),
    inference(distribute,[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_2Ebool_2ERIGHT__OR__EXISTS__THM])])])])])]) ).

fof(i_0_81,plain,
    ! [X310,X311,X312,X313,X315,X316,X317,X318] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X310,tyop_2Emin_2Ebool),X311),s(X310,X313))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X310,tyop_2Emin_2Ebool),X311),s(X310,esk10_3(X310,X311,X312)))))
        | p(s(tyop_2Emin_2Ebool,X312)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X312))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X310,tyop_2Emin_2Ebool),X311),s(X310,esk10_3(X310,X311,X312)))))
        | p(s(tyop_2Emin_2Ebool,X312)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X315,tyop_2Emin_2Ebool),X316),s(X315,X318))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X315,tyop_2Emin_2Ebool),X316),s(X315,esk11_3(X315,X316,X317)))))
        | p(s(tyop_2Emin_2Ebool,X317)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X317))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X315,tyop_2Emin_2Ebool),X316),s(X315,esk11_3(X315,X316,X317)))))
        | p(s(tyop_2Emin_2Ebool,X317)) ) ),
    inference(distribute,[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_2Ebool_2ELEFT__OR__EXISTS__THM])])])])])]) ).

fof(i_0_82,plain,
    ! [X209,X210,X211,X212] : s(X209,app_2E2(s(tyop_2Emin_2Efun(X210,X209),app_2E2(s(tyop_2Emin_2Efun(X209,tyop_2Emin_2Efun(X210,X209)),combin_k_2E0),s(X209,X211))),s(X210,X212))) = s(X209,X211),
    inference(variable_rename,[status(thm)],[reserved_2Eho_2Ek__thm]) ).

fof(i_0_83,plain,
    ! [X282,X283,X285,X286,X287,X289] :
      ( ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X282,tyop_2Emin_2Ebool),X283),s(X282,esk4_2(X282,X283)))))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X282,tyop_2Emin_2Ebool),X283),s(X282,X285)))) )
      & ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X286,tyop_2Emin_2Ebool),X287),s(X286,esk5_2(X286,X287)))))
        | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X286,tyop_2Emin_2Ebool),X287),s(X286,X289)))) ) ),
    inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_50])])])])]) ).

fof(i_0_84,plain,
    ! [X229,X230,X231,X232,X233] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X229,tyop_2Emin_2Ebool),X230))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X229,tyop_2Emin_2Ebool),X230),s(X229,X231)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X232,tyop_2Emin_2Ebool),X233),s(X232,esk2_2(X232,X233)))))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X232,tyop_2Emin_2Ebool),X233)))) ) ),
    inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Equant_2E_21])])])])]) ).

fof(i_0_85,plain,
    ! [X235,X236,X238,X239,X240] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X235,tyop_2Emin_2Ebool),X236))))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X235,tyop_2Emin_2Ebool),X236),s(X235,esk3_2(X235,X236))))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X238,tyop_2Emin_2Ebool),X239),s(X238,X240))))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X238,tyop_2Emin_2Ebool),X239)))) ) ),
    inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Equant_2E_3F])])])])]) ).

fof(i_0_86,plain,
    ! [X245] :
      ( ( p(s(tyop_2Emin_2Ebool,X245))
        | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X245)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X245))))
        | ~ p(s(tyop_2Emin_2Ebool,X245)) ) ),
    inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])]) ).

fof(i_0_87,plain,
    ! [X253,X254] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X253,tyop_2Emin_2Ebool),X254))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X253,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(X253,tyop_2Emin_2Ebool),X254))),
    inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a]) ).

fof(i_0_88,plain,
    ! [X251,X252] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X251,tyop_2Emin_2Ebool),X252))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X251,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(X251,tyop_2Emin_2Ebool),X252))),
    inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a]) ).

fof(i_0_89,plain,
    ! [X224,X225] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X224),s(tyop_2Emin_2Ebool,X225))))
        | ~ p(s(tyop_2Emin_2Ebool,X224))
        | p(s(tyop_2Emin_2Ebool,X225)) )
      & ( p(s(tyop_2Emin_2Ebool,X224))
        | p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X224),s(tyop_2Emin_2Ebool,X225)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X225))
        | p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X224),s(tyop_2Emin_2Ebool,X225)))) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_3D_3D_3E])])]) ).

fof(i_0_90,plain,
    ! [X226,X227,X228] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X226,X227),s(X226,X228))))
        | s(X226,X227) = s(X226,X228) )
      & ( s(X226,X227) != s(X226,X228)
        | p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X226,X227),s(X226,X228)))) ) ),
    inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_3D])]) ).

fof(i_0_91,plain,
    ! [X221,X222] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X221),s(tyop_2Emin_2Ebool,X222))))
        | p(s(tyop_2Emin_2Ebool,X221))
        | p(s(tyop_2Emin_2Ebool,X222)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X221))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X221),s(tyop_2Emin_2Ebool,X222)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X222))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X221),s(tyop_2Emin_2Ebool,X222)))) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_5C_2F])])]) ).

fof(i_0_92,plain,
    ! [X219,X220] :
      ( ( p(s(tyop_2Emin_2Ebool,X219))
        | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X219),s(tyop_2Emin_2Ebool,X220)))) )
      & ( p(s(tyop_2Emin_2Ebool,X220))
        | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X219),s(tyop_2Emin_2Ebool,X220)))) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X219))
        | ~ p(s(tyop_2Emin_2Ebool,X220))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X219),s(tyop_2Emin_2Ebool,X220)))) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_2F_5C])])]) ).

fof(i_0_93,plain,
    ! [X207,X208] : s(X207,app_2E2(s(tyop_2Emin_2Efun(X207,X207),combin_i_2E0),s(X207,X208))) = s(X207,X208),
    inference(variable_rename,[status(thm)],[reserved_2Eho_2Ei__thm]) ).

fof(i_0_94,plain,
    ! [X223] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X223))))
        | ~ p(s(tyop_2Emin_2Ebool,X223)) )
      & ( p(s(tyop_2Emin_2Ebool,X223))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X223)))) ) ),
    inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])]) ).

cnf(i_0_95,plain,
    ( p(s(tyop_2Emin_2Ebool,X3))
    | p(s(tyop_2Emin_2Ebool,X3))
    | s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
    | ~ epred1_3(X3,X1,X2) ),
    inference(split_conjunct,[status(thm)],[i_0_53]) ).

cnf(i_0_96,plain,
    ( epred1_3(X2,X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]) ).

cnf(i_0_97,plain,
    ( epred1_3(X2,X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]) ).

cnf(i_0_98,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | epred1_3(X2,X3,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]) ).

cnf(i_0_99,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X1))
    | epred1_3(X2,X3,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]) ).

cnf(i_0_100,plain,
    ( p(s(tyop_2Emin_2Ebool,X2))
    | epred1_3(X3,X1,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]) ).

cnf(i_0_101,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X1))
    | epred1_3(X3,X2,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]) ).

fof(i_0_102,plain,
    ! [X273,X274] :
      ( ( p(s(tyop_2Emin_2Ebool,X274))
        | s(tyop_2Emin_2Ebool,X273) = s(tyop_2Emin_2Ebool,X274)
        | p(s(tyop_2Emin_2Ebool,X273)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X273))
        | s(tyop_2Emin_2Ebool,X273) = s(tyop_2Emin_2Ebool,X274)
        | p(s(tyop_2Emin_2Ebool,X273)) )
      & ( p(s(tyop_2Emin_2Ebool,X274))
        | s(tyop_2Emin_2Ebool,X273) = s(tyop_2Emin_2Ebool,X274)
        | ~ p(s(tyop_2Emin_2Ebool,X274)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X273))
        | s(tyop_2Emin_2Ebool,X273) = s(tyop_2Emin_2Ebool,X274)
        | ~ p(s(tyop_2Emin_2Ebool,X274)) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Ebool_2EIMP__ANTISYM__AX])])]) ).

fof(i_0_103,plain,
    ! [X204,X205] :
      ( ( ~ p(s(tyop_2Emin_2Ebool,X204))
        | ~ p(s(tyop_2Emin_2Ebool,X205))
        | s(tyop_2Emin_2Ebool,X204) = s(tyop_2Emin_2Ebool,X205) )
      & ( p(s(tyop_2Emin_2Ebool,X204))
        | p(s(tyop_2Emin_2Ebool,X205))
        | s(tyop_2Emin_2Ebool,X204) = s(tyop_2Emin_2Ebool,X205) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Eho_2Eboolext])])]) ).

fof(i_0_104,plain,
    ! [X277] :
      ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
        | p(s(tyop_2Emin_2Ebool,X277)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X277))
        | p(s(tyop_2Emin_2Ebool,X277)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X277))
        | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
        | p(s(tyop_2Emin_2Ebool,X277)) )
      & ( p(s(tyop_2Emin_2Ebool,X277))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
        | ~ p(s(tyop_2Emin_2Ebool,X277))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X277))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
        | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
        | p(s(tyop_2Emin_2Ebool,X277)) )
      & p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
      & ( p(s(tyop_2Emin_2Ebool,X277))
        | ~ p(s(tyop_2Emin_2Ebool,X277)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
        | ~ p(s(tyop_2Emin_2Ebool,X277)) )
      & ( p(s(tyop_2Emin_2Ebool,X277))
        | ~ p(s(tyop_2Emin_2Ebool,X277))
        | p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_55])])]) ).

fof(i_0_105,plain,
    ! [X275] :
      ( ( p(s(tyop_2Emin_2Ebool,X275))
        | ~ p(s(tyop_2Emin_2Ebool,X275)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
        | ~ p(s(tyop_2Emin_2Ebool,X275)) ) ),
    inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_56])])]) ).

fof(i_0_106,plain,
    ! [X281] :
      ( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,X281)
        | p(s(tyop_2Emin_2Ebool,X281)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X281))
        | s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X281) )
      & ( s(tyop_2Emin_2Ebool,X281) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
        | p(s(tyop_2Emin_2Ebool,X281)) )
      & ( ~ p(s(tyop_2Emin_2Ebool,X281))
        | s(tyop_2Emin_2Ebool,X281) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
      & ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,X281)
        | ~ p(s(tyop_2Emin_2Ebool,X281)) )
      & ( p(s(tyop_2Emin_2Ebool,X281))
        | s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X281) )
      & ( s(tyop_2Emin_2Ebool,X281) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
        | ~ p(s(tyop_2Emin_2Ebool,X281)) )
      & ( p(s(tyop_2Emin_2Ebool,X281))
        | s(tyop_2Emin_2Ebool,X281) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ),
    inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_57])]) ).

fof(i_0_107,plain,
    ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
      | p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
    & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
      | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
    & ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
      | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
    & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
      | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ),
    inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[i_0_58])]) ).

fof(i_0_108,plain,
    ! [X206] :
      ( s(tyop_2Emin_2Ebool,X206) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
      | s(tyop_2Emin_2Ebool,X206) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
    inference(variable_rename,[status(thm)],[reserved_2Eho_2Ebool__cases__ax]) ).

fof(i_0_109,plain,
    ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
    inference(fof_simplification,[status(thm)],[reserved_2Eho_2Enotfalse]) ).

cnf(i_0_110,plain,
    s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X1),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X3))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X1))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X2))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X3))),
    inference(split_conjunct,[status(thm)],[i_0_59]),
    [final] ).

cnf(i_0_111,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X3),s(X2,X5))),s(X1,esk25_4(X2,X1,X3,X5)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X3),s(X2,esk24_4(X2,X1,X3,X4)))),s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),X4),s(X2,esk24_4(X2,X1,X3,X4))))))) ),
    inference(split_conjunct,[status(thm)],[i_0_60]),
    [final] ).

cnf(i_0_112,plain,
    s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X1),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X3))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X1))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X2))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X3))),
    inference(split_conjunct,[status(thm)],[i_0_61]),
    [final] ).

cnf(i_0_113,plain,
    s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X2,X1)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X3,X1)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,X3),tyop_2Emin_2Efun(X2,X1))),combin_s_2E0),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X3,X1)),X4))),s(tyop_2Emin_2Efun(X2,X3),X5))),s(X2,X6))) = s(X1,app_2E2(s(tyop_2Emin_2Efun(X3,X1),app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X3,X1)),X4),s(X2,X6))),s(X3,app_2E2(s(tyop_2Emin_2Efun(X2,X3),X5),s(X2,X6))))),
    inference(split_conjunct,[status(thm)],[i_0_62]),
    [final] ).

cnf(i_0_114,plain,
    s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(X1,X2),X3))),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4))),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5))),
    inference(split_conjunct,[status(thm)],[i_0_63]),
    [final] ).

cnf(i_0_115,plain,
    s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,X2),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(X1,X2),X3))),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4))),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5))),
    inference(split_conjunct,[status(thm)],[i_0_64]),
    [final] ).

cnf(i_0_116,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X3),s(X2,X5))),s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),esk23_3(X2,X1,X3)),s(X2,X5))))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X3),s(X2,esk22_3(X2,X1,X3)))),s(X1,X4)))) ),
    inference(split_conjunct,[status(thm)],[i_0_60]),
    [final] ).

cnf(i_0_117,plain,
    s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X1),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X2))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool))),c_2Epred__set_2ECROSS_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X1))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X2))),
    inference(split_conjunct,[status(thm)],[i_0_65]),
    [final] ).

cnf(i_0_118,plain,
    ( s(tyop_2Emin_2Efun(X2,X1),X3) = s(tyop_2Emin_2Efun(X2,X1),X4)
    | s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),X3),s(X2,esk1_4(X2,X1,X3,X4)))) != s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),X4),s(X2,esk1_4(X2,X1,X3,X4)))) ),
    inference(split_conjunct,[status(thm)],[i_0_66]),
    [final] ).

cnf(i_0_119,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X2,X1),esk27_4(X2,X1,X5,X4)),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4))))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5)))) ),
    inference(split_conjunct,[status(thm)],[i_0_67]),
    [final] ).

cnf(i_0_120,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X2,X1),esk26_4(X1,X2,X4,X5)),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4))))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X4),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X5)))) ),
    inference(split_conjunct,[status(thm)],[i_0_67]),
    [final] ).

cnf(i_0_121,negated_conjecture,
    ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X1),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))),
    inference(split_conjunct,[status(thm)],[i_0_68]),
    [final] ).

cnf(i_0_122,plain,
    ( s(X1,X2) = s(X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X1,X2))),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_69]),
    [final] ).

cnf(i_0_123,plain,
    ( p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X1))),s(tyop_2Emin_2Ebool,X2))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_70]),
    [final] ).

cnf(i_0_124,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X1))),s(tyop_2Emin_2Ebool,X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_71]),
    [final] ).

cnf(i_0_125,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X1))),s(tyop_2Emin_2Ebool,X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_72]),
    [final] ).

cnf(i_0_126,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X2))),s(tyop_2Emin_2Ebool,X1)))) ),
    inference(split_conjunct,[status(thm)],[i_0_72]),
    [final] ).

cnf(i_0_127,plain,
    p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),esk28_0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))),
    inference(split_conjunct,[status(thm)],[i_0_73]),
    [final] ).

cnf(i_0_128,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X1,X2))),s(X1,X3))))
    | s(X1,X2) != s(X1,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_69]),
    [final] ).

cnf(i_0_129,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X1))),s(tyop_2Emin_2Ebool,X2))))
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_72]),
    [final] ).

cnf(i_0_130,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X2))),s(tyop_2Emin_2Ebool,X1))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_70]),
    [final] ).

cnf(i_0_131,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X1))),s(tyop_2Emin_2Ebool,X2))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_71]),
    [final] ).

cnf(i_0_132,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X2))),s(tyop_2Emin_2Ebool,X1))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_71]),
    [final] ).

cnf(i_0_133,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X1))),s(tyop_2Emin_2Ebool,X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_70]),
    [final] ).

cnf(i_0_134,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
    | ~ p(s(tyop_2Emin_2Ebool,X4))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk9_3(X1,X4,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_74]),
    [final] ).

cnf(i_0_135,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
    | ~ p(s(tyop_2Emin_2Ebool,X4))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk8_3(X1,X4,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_74]),
    [final] ).

cnf(i_0_136,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk7_3(X1,X2,X4)))))
    | ~ p(s(tyop_2Emin_2Ebool,X4)) ),
    inference(split_conjunct,[status(thm)],[i_0_75]),
    [final] ).

cnf(i_0_137,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk6_3(X1,X2,X4)))))
    | ~ p(s(tyop_2Emin_2Ebool,X4)) ),
    inference(split_conjunct,[status(thm)],[i_0_75]),
    [final] ).

cnf(i_0_138,plain,
    ( p(s(tyop_2Emin_2Ebool,X3))
    | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk21_3(X1,X3,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_76]),
    [final] ).

cnf(i_0_139,plain,
    ( p(s(tyop_2Emin_2Ebool,X3))
    | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk20_3(X1,X3,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_76]),
    [final] ).

cnf(i_0_140,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4))))
    | p(s(tyop_2Emin_2Ebool,X3))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk19_3(X1,X3,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_77]),
    [final] ).

cnf(i_0_141,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4))))
    | p(s(tyop_2Emin_2Ebool,X3))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk18_3(X1,X3,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_77]),
    [final] ).

cnf(i_0_142,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk17_3(X1,X3,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,X3))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4)))) ),
    inference(split_conjunct,[status(thm)],[i_0_78]),
    [final] ).

cnf(i_0_143,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk16_3(X1,X3,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,X3))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4)))) ),
    inference(split_conjunct,[status(thm)],[i_0_78]),
    [final] ).

cnf(i_0_144,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk15_3(X1,X2,X3)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4))))
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_79]),
    [final] ).

cnf(i_0_145,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk14_3(X1,X2,X3)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X4))))
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_79]),
    [final] ).

cnf(i_0_146,plain,
    ( p(s(tyop_2Emin_2Ebool,X4))
    | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk13_3(X1,X4,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_80]),
    [final] ).

cnf(i_0_147,plain,
    ( p(s(tyop_2Emin_2Ebool,X4))
    | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk12_3(X1,X4,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_80]),
    [final] ).

cnf(i_0_148,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk11_3(X1,X2,X4)))))
    | p(s(tyop_2Emin_2Ebool,X4))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_81]),
    [final] ).

cnf(i_0_149,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk10_3(X1,X2,X4)))))
    | p(s(tyop_2Emin_2Ebool,X4))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_81]),
    [final] ).

cnf(i_0_150,plain,
    s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X2,X1)),combin_k_2E0),s(X1,X3))),s(X2,X4))) = s(X1,X3),
    inference(split_conjunct,[status(thm)],[i_0_82]),
    [final] ).

cnf(i_0_151,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk5_2(X1,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_83]),
    [final] ).

cnf(i_0_152,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk4_2(X1,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_83]),
    [final] ).

cnf(i_0_153,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk2_2(X1,X2))))) ),
    inference(split_conjunct,[status(thm)],[i_0_84]),
    [final] ).

cnf(i_0_154,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk3_2(X1,X2)))))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_85]),
    [final] ).

cnf(i_0_155,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))))
    | ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_85]),
    [final] ).

cnf(i_0_156,plain,
    ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_84]),
    [final] ).

cnf(i_0_157,plain,
    ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X1))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_86]),
    [final] ).

cnf(i_0_158,plain,
    s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))),
    inference(split_conjunct,[status(thm)],[i_0_87]),
    [final] ).

cnf(i_0_159,plain,
    s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))),
    inference(split_conjunct,[status(thm)],[i_0_88]),
    [final] ).

cnf(i_0_160,plain,
    ( p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X1),s(tyop_2Emin_2Ebool,X2))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_89]),
    [final] ).

cnf(i_0_161,plain,
    ( s(X1,X2) = s(X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X1,X2),s(X1,X3)))) ),
    inference(split_conjunct,[status(thm)],[i_0_90]),
    [final] ).

cnf(i_0_162,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X1),s(tyop_2Emin_2Ebool,X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_91]),
    [final] ).

cnf(i_0_163,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X1)))) ),
    inference(split_conjunct,[status(thm)],[i_0_86]),
    [final] ).

cnf(i_0_164,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X1),s(tyop_2Emin_2Ebool,X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_92]),
    [final] ).

cnf(i_0_165,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X2),s(tyop_2Emin_2Ebool,X1)))) ),
    inference(split_conjunct,[status(thm)],[i_0_92]),
    [final] ).

cnf(i_0_166,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X1),s(tyop_2Emin_2Ebool,X2))))
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_92]),
    [final] ).

cnf(i_0_167,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X1,X2),s(X1,X3))))
    | s(X1,X2) != s(X1,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_90]),
    [final] ).

cnf(i_0_168,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X2),s(tyop_2Emin_2Ebool,X1))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_89]),
    [final] ).

cnf(i_0_169,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X1),s(tyop_2Emin_2Ebool,X2))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_91]),
    [final] ).

cnf(i_0_170,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X2),s(tyop_2Emin_2Ebool,X1))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_91]),
    [final] ).

cnf(i_0_171,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X1),s(tyop_2Emin_2Ebool,X2)))) ),
    inference(split_conjunct,[status(thm)],[i_0_89]),
    [final] ).

cnf(i_0_172,plain,
    s(X1,app_2E2(s(tyop_2Emin_2Efun(X1,X1),combin_i_2E0),s(X1,X2))) = s(X1,X2),
    inference(split_conjunct,[status(thm)],[i_0_93]),
    [final] ).

cnf(i_0_173,plain,
    ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X1))))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_94]),
    [final] ).

cnf(i_0_174,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X3))
    | ~ epred1_3(X1,X3,X2) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_175,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X3))
    | ~ epred1_3(X3,X1,X2) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_176,plain,
    ( s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X3))
    | ~ epred1_3(X1,X2,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_53]),
    [final] ).

cnf(i_0_177,plain,
    ( p(s(tyop_2Emin_2Ebool,X3))
    | s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ epred1_3(X3,X1,X2) ),
    inference(split_conjunct,[status(thm)],[i_0_53]),
    [final] ).

cnf(i_0_178,plain,
    ( epred1_3(X2,X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_179,plain,
    ( s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X3)
    | p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ epred1_3(X1,X2,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_53]),
    [final] ).

cnf(i_0_180,plain,
    ( p(s(tyop_2Emin_2Ebool,X3))
    | p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
    | ~ epred1_3(X3,X1,X2) ),
    inference(split_conjunct,[status(thm)],[i_0_53]),
    [final] ).

cnf(i_0_181,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | epred1_3(X2,X3,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_182,plain,
    ( p(s(tyop_2Emin_2Ebool,X2))
    | epred1_3(X3,X1,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_183,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | p(s(tyop_2Emin_2Ebool,X3))
    | ~ epred1_3(X1,X2,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_184,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X1)))) ),
    inference(split_conjunct,[status(thm)],[i_0_94]),
    [final] ).

cnf(i_0_185,plain,
    ( p(s(tyop_2Emin_2Ebool,X3))
    | s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
    | ~ epred1_3(X3,X1,X2) ),
    inference(cn,[status(thm)],[i_0_95]),
    [final] ).

cnf(i_0_186,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | epred1_3(X1,X2,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_187,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | epred1_3(X1,X3,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_188,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | epred1_3(X3,X2,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X3)) ),
    inference(split_conjunct,[status(thm)],[i_0_54]),
    [final] ).

cnf(i_0_189,plain,
    ( epred1_3(X2,X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(cn,[status(thm)],[i_0_96]),
    [final] ).

cnf(i_0_190,plain,
    ( epred1_3(X2,X1,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(cn,[status(thm)],[i_0_97]),
    [final] ).

cnf(i_0_191,plain,
    ( epred1_3(X1,X2,X3)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,X2) != s(tyop_2Emin_2Ebool,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_53]),
    [final] ).

cnf(i_0_192,plain,
    ( epred1_3(X2,X3,X1)
    | p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(cn,[status(thm)],[i_0_98]),
    [final] ).

cnf(i_0_193,plain,
    ( epred1_3(X2,X3,X1)
    | p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(cn,[status(thm)],[i_0_99]),
    [final] ).

cnf(i_0_194,plain,
    ( epred1_3(X3,X1,X2)
    | p(s(tyop_2Emin_2Ebool,X2))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(cn,[status(thm)],[i_0_100]),
    [final] ).

cnf(i_0_195,plain,
    ( epred1_3(X3,X2,X1)
    | p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(cn,[status(thm)],[i_0_101]),
    [final] ).

cnf(i_0_196,plain,
    ( s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_102]),
    [final] ).

cnf(i_0_197,plain,
    ( s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_103]),
    [final] ).

cnf(i_0_198,plain,
    ( epred1_3(X1,X2,X3)
    | p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X3) ),
    inference(split_conjunct,[status(thm)],[i_0_53]),
    [final] ).

cnf(i_0_199,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_200,plain,
    ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_201,plain,
    ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_105]),
    [final] ).

cnf(i_0_202,plain,
    ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_203,plain,
    ( s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_204,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X1)
    | p(s(tyop_2Emin_2Ebool,X2)) ),
    inference(split_conjunct,[status(thm)],[i_0_102]),
    [final] ).

cnf(i_0_205,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,X2))
    | s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,X2) ),
    inference(split_conjunct,[status(thm)],[i_0_103]),
    [final] ).

cnf(i_0_206,plain,
    ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_107]),
    [final] ).

cnf(i_0_207,plain,
    ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    | ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_107]),
    [final] ).

cnf(i_0_208,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_209,plain,
    ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X1)
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_210,plain,
    ( s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_211,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,X1) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_212,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_213,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    | p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_214,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_215,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X1) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_216,plain,
    ( p(s(tyop_2Emin_2Ebool,X1))
    | s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
    inference(split_conjunct,[status(thm)],[i_0_106]),
    [final] ).

cnf(i_0_217,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
    | p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_107]),
    [final] ).

cnf(i_0_218,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_107]),
    [final] ).

cnf(i_0_219,plain,
    ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
    | p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_220,plain,
    ( s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
    | s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
    inference(split_conjunct,[status(thm)],[i_0_108]),
    [final] ).

cnf(i_0_221,plain,
    ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
    inference(split_conjunct,[status(thm)],[i_0_109]),
    [final] ).

cnf(i_0_222,plain,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    inference(split_conjunct,[status(thm)],[i_0_104]),
    [final] ).

cnf(i_0_223,plain,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    inference(split_conjunct,[status(thm)],[thm_2Ebool_2ETRUTH]),
    [final] ).

cnf(i_0_224,plain,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    inference(split_conjunct,[status(thm)],[reserved_2Eho_2Etruth]),
    [final] ).

cnf(i_0_225,axiom,
    X1 = X1 ).

cnf(i_0_226,axiom,
    ( X1 = X2
    | X2 != X1 ) ).

cnf(i_0_227,axiom,
    ( X1 = X2
    | X1 != X3
    | X3 != X2 ) ).

cnf(i_0_228,axiom,
    ( X1 != X2
    | s(X1,X3) = s(X2,X3) ) ).

cnf(i_0_229,axiom,
    ( X1 != X2
    | s(X3,X1) = s(X3,X2) ) ).

cnf(i_0_230,axiom,
    ( X1 != X2
    | ~ p(X1)
    | p(X2) ) ).

cnf(i_0_231,axiom,
    ( X1 != X2
    | ~ epred1_3(X1,X3,X4)
    | epred1_3(X2,X3,X4) ) ).

cnf(i_0_232,axiom,
    ( X1 != X2
    | ~ epred1_3(X3,X1,X4)
    | epred1_3(X3,X2,X4) ) ).

cnf(i_0_233,axiom,
    ( X1 != X2
    | ~ epred1_3(X3,X4,X1)
    | epred1_3(X3,X4,X2) ) ).

cnf(i_0_225_001,axiom,
    X1 = X1 ).

cnf(i_0_226_002,axiom,
    ( X1 = X2
    | X2 != X1 ) ).

cnf(i_0_227_003,axiom,
    ( X1 = X2
    | X1 != X3
    | X3 != X2 ) ).

cnf(i_0_228_004,axiom,
    ( X1 != X2
    | s(X1,X3) = s(X2,X3) ) ).

cnf(i_0_229_005,axiom,
    ( X1 != X2
    | s(X3,X1) = s(X3,X2) ) ).

cnf(i_0_230_006,axiom,
    ( X1 != X2
    | ~ p(X1)
    | p(X2) ) ).

cnf(i_0_231_007,axiom,
    ( X1 != X2
    | ~ epred1_3(X1,X3,X4)
    | epred1_3(X2,X3,X4) ) ).

cnf(i_0_232_008,axiom,
    ( X1 != X2
    | ~ epred1_3(X3,X1,X4)
    | epred1_3(X3,X2,X4) ) ).

cnf(i_0_233_009,axiom,
    ( X1 != X2
    | ~ epred1_3(X3,X4,X1)
    | epred1_3(X3,X4,X2) ) ).

cnf(i_0_234,plain,
    s(tyop_2Emin_2Efun(X1,X2),X3) = s(tyop_2Emin_2Efun(X1,X2),X3),
    inference(equality_inference,[],[118]) ).

cnf(i_0_235,plain,
    p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X1,X2))),s(X1,X2)))),
    inference(equality_inference,[],[128]) ).

cnf(i_0_236,plain,
    p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X1,X2),s(X1,X2)))),
    inference(equality_inference,[],[167]) ).

cnf(i_0_237,plain,
    ( ~ epred1_3(X1,X2,X2)
    | p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(equality_inference,[],[185]) ).

cnf(i_0_238,plain,
    ( epred1_3(X1,X2,X2)
    | ~ p(s(tyop_2Emin_2Ebool,X1)) ),
    inference(equality_inference,[],[191]) ).

cnf(i_0_239,plain,
    ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
    inference(equality_inference,[],[202]) ).

cnf(i_0_240,plain,
    ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
    inference(equality_inference,[],[203]) ).

cnf(i_0_241,plain,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    inference(equality_inference,[],[211]) ).

cnf(i_0_242,plain,
    p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
    inference(equality_inference,[],[212]) ).

cnf(i_0_243,plain,
    $false,
    inference(scs_inference,[],[i_0_121,i_0_127,i_0_119]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : ITP020+1 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33  % Computer : n026.cluster.edu
% 0.16/0.33  % Model    : x86_64 x86_64
% 0.16/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33  % Memory   : 8042.1875MB
% 0.16/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33  % CPULimit   : 300
% 0.16/0.33  % WCLimit    : 300
% 0.16/0.33  % DateTime   : Mon May  4 19:45:23 EDT 2026
% 0.16/0.33  % CPUTime    : 
% 0.16/0.34  % start to proof: theBenchmark
% 0.71/1.62  % Version  : CSE_E---1.7
% 0.71/1.62  % Problem  : theBenchmark.p
% 0.71/1.62  % SZS status Theorem for theBenchmark.p
% 0.71/1.62  % SZS output start CNFRefutation
% See solution above
% 0.71/1.64  % Total time : 1.272s
%------------------------------------------------------------------------------