%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ITP015+2 : 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 : n007.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:31:36 PM UTC 2026
% Result : Theorem 113.13s 90.92s
% Output : CNFRefutation 116.26s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_181)
% Comments :
%------------------------------------------------------------------------------
fof(conj_thm_2Ebool_2ECOND__CONG,axiom,
! [X9] :
( ne(X9)
=> ! [X18] :
( mem(X18,bool)
=> ! [X19] :
( mem(X19,bool)
=> ! [X20] :
( mem(X20,X9)
=> ! [X21] :
( mem(X21,X9)
=> ! [X22] :
( mem(X22,X9)
=> ! [X23] :
( mem(X23,X9)
=> ( ( ( p(X18)
<=> p(X19) )
& ( p(X19)
=> X20 = X21 )
& ( ~ p(X19)
=> X22 = X23 ) )
=> ap(ap(ap(c_2Ebool_2ECOND(X9),X18),X20),X22) = ap(ap(ap(c_2Ebool_2ECOND(X9),X19),X21),X23) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ebool_2ECOND__CONG) ).
fof(conj_thm_2Einteger_2EINT__LT__CALCULATE,axiom,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ! [X27] :
( mem(X27,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__of__num,X27)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X26),X27)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X27),X26)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__of__num,X27)))
<=> ( X26 != c_2Enum_2E0
| X27 != c_2Enum_2E0 ) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> ~ $true ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__LT__CALCULATE) ).
fof(conj_thm_2Eprim__rec_2ENOT__LESS__0,axiom,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ~ p(ap(ap(c_2Eprim__rec_2E_3C,X26),c_2Enum_2E0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eprim__rec_2ENOT__LESS__0) ).
fof(conj_thm_2Einteger__word_2Ei2w__0,conjecture,
! [X9] :
( ne(X9)
=> ap(c_2Einteger__word_2Ei2w(X9),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X9),c_2Enum_2E0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger__word_2Ei2w__0) ).
fof(ax_neg_p,axiom,
! [X5] :
( mem(X5,bool)
=> ( p(ap(c_2Ebool_2E_7E,X5))
<=> ~ p(X5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_neg_p) ).
fof(funcext,axiom,
! [X1,X2,X3] :
( mem(X3,arr(X1,X2))
=> ! [X7] :
( mem(X7,arr(X1,X2))
=> ( ! [X4] :
( mem(X4,X1)
=> ap(X3,X4) = ap(X7,X4) )
=> X3 = X7 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',funcext) ).
fof(ax_thm_2Einteger__word_2Ei2w__def,axiom,
! [X9] :
( ne(X9)
=> ! [X28] :
( mem(X28,ty_2Einteger_2Eint)
=> ap(c_2Einteger__word_2Ei2w(X9),X28) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X9)),ap(ap(c_2Einteger_2Eint__lt,X28),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X9),ap(c_2Ewords_2En2w(X9),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X28))))),ap(c_2Ewords_2En2w(X9),ap(c_2Einteger_2ENum,X28))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Einteger__word_2Ei2w__def) ).
fof(conj_thm_2Ewords_2En2w__11,axiom,
! [X9] :
( ne(X9)
=> ! [X29] :
( mem(X29,ty_2Enum_2Enum)
=> ! [X30] :
( mem(X30,ty_2Enum_2Enum)
=> ( ap(c_2Ewords_2En2w(X9),X29) = ap(c_2Ewords_2En2w(X9),X30)
<=> ap(ap(c_2Earithmetic_2EMOD,X29),ap(c_2Ewords_2Edimword(X9),c_2Ebool_2Ethe__value(X9))) = ap(ap(c_2Earithmetic_2EMOD,X30),ap(c_2Ewords_2Edimword(X9),c_2Ebool_2Ethe__value(X9))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ewords_2En2w__11) ).
fof(ax_all_p,axiom,
! [X1] :
( ne(X1)
=> ! [X5] :
( mem(X5,arr(X1,bool))
=> ( p(ap(c_2Ebool_2E_21(X1),X5))
<=> ! [X4] :
( mem(X4,X1)
=> p(ap(X5,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_all_p) ).
fof(ax_eq_p,axiom,
! [X1] :
( ne(X1)
=> ! [X4] :
( mem(X4,X1)
=> ! [X8] :
( mem(X8,X1)
=> ( p(ap(ap(c_2Emin_2E_3D(X1),X4),X8))
<=> X4 = X8 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_eq_p) ).
fof(mem_c_2Ebool_2ECOND,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ebool_2ECOND(X9),arr(bool,arr(X9,arr(X9,X9)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2ECOND) ).
fof(ax_imp_p,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( p(ap(ap(c_2Emin_2E_3D_3D_3E,X5),X6))
<=> ( p(X5)
=> p(X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_imp_p) ).
fof(ax_or_p,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( p(ap(ap(c_2Ebool_2E_5C_2F,X5),X6))
<=> ( p(X5)
| p(X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_or_p) ).
fof(ax_and_p,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( p(ap(ap(c_2Ebool_2E_2F_5C,X5),X6))
<=> ( p(X5)
& p(X6) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_and_p) ).
fof(conj_thm_2Ebool_2Ebool__case__thm,axiom,
! [X9] :
( ne(X9)
=> ( ! [X12] :
( mem(X12,X9)
=> ! [X13] :
( mem(X13,X9)
=> ap(ap(ap(c_2Ebool_2ECOND(X9),c_2Ebool_2ET),X12),X13) = X12 ) )
& ! [X24] :
( mem(X24,X9)
=> ! [X25] :
( mem(X25,X9)
=> ap(ap(ap(c_2Ebool_2ECOND(X9),c_2Ebool_2EF),X24),X25) = X25 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ebool_2Ebool__case__thm) ).
fof(mem_c_2Ewords_2Eword__2comp,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ewords_2Eword__2comp(X9),arr(ty_2Efcp_2Ecart(bool,X9),ty_2Efcp_2Ecart(bool,X9))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ewords_2Eword__2comp) ).
fof(ap_tp,axiom,
! [X1,X2,X3] :
( mem(X3,arr(X1,X2))
=> ! [X4] :
( mem(X4,X1)
=> mem(ap(X3,X4),X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(mem_c_2Emin_2E_3D,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Emin_2E_3D(X9),arr(X9,arr(X9,bool))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D) ).
fof(mem_c_2Ebool_2E_21,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ebool_2E_21(X9),arr(arr(X9,bool),bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_21) ).
fof(mem_c_2Ewords_2En2w,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ewords_2En2w(X9),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X9))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ewords_2En2w) ).
fof(mem_c_2Einteger__word_2Ei2w,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Einteger__word_2Ei2w(X9),arr(ty_2Einteger_2Eint,ty_2Efcp_2Ecart(bool,X9))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Einteger__word_2Ei2w) ).
fof(conj_thm_2Ewords_2EWORD__NEG__0,axiom,
! [X9] :
( ne(X9)
=> ap(c_2Ewords_2Eword__2comp(X9),ap(c_2Ewords_2En2w(X9),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X9),c_2Enum_2E0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ewords_2EWORD__NEG__0) ).
fof(kbeta,axiom,
! [X1,X8,X4] :
( mem(X4,X1)
=> ap(k(X1,X8),X4) = X8 ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',kbeta) ).
fof(mem_c_2Ewords_2Edimword,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ewords_2Edimword(X9),arr(ty_2Ebool_2Eitself(X9),ty_2Enum_2Enum)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ewords_2Edimword) ).
fof(boolext,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( ( p(X5)
<=> p(X6) )
=> X5 = X6 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
fof(conj_thm_2Einteger_2ENUM__OF__INT,axiom,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X26)) = X26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger_2ENUM__OF__INT) ).
fof(ne_ty_2Efcp_2Ecart,axiom,
! [X10] :
( ne(X10)
=> ! [X11] :
( ne(X11)
=> ne(ty_2Efcp_2Ecart(X10,X11)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Efcp_2Ecart) ).
fof(arr_ne,axiom,
! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ne(arr(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',arr_ne) ).
fof(ibeta,axiom,
! [X1,X4] :
( mem(X4,X1)
=> ap(i(X1),X4) = X4 ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ibeta) ).
fof(mem_c_2Ebool_2Ethe__value,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ebool_2Ethe__value(X9),ty_2Ebool_2Eitself(X9)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2Ethe__value) ).
fof(ne_ty_2Ebool_2Eitself,axiom,
! [X10] :
( ne(X10)
=> ne(ty_2Ebool_2Eitself(X10)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Ebool_2Eitself) ).
fof(ax_false_p,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_false_p) ).
fof(mem_c_2Earithmetic_2EMOD,axiom,
mem(c_2Earithmetic_2EMOD,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Earithmetic_2EMOD) ).
fof(mem_c_2Eprim__rec_2E_3C,axiom,
mem(c_2Eprim__rec_2E_3C,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Eprim__rec_2E_3C) ).
fof(mem_c_2Einteger_2Eint__lt,axiom,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__lt) ).
fof(mem_c_2Ebool_2E_2F_5C,axiom,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_2F_5C) ).
fof(mem_c_2Ebool_2E_5C_2F,axiom,
mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_5C_2F) ).
fof(mem_c_2Emin_2E_3D_3D_3E,axiom,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D_3D_3E) ).
fof(conj_thm_2Einteger_2EINT__NEG__0,axiom,
ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__NEG__0) ).
fof(mem_c_2Ebool_2E_7E,axiom,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2E_7E) ).
fof(mem_c_2Einteger_2Eint__of__num,axiom,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__of__num) ).
fof(mem_c_2Einteger_2ENum,axiom,
mem(c_2Einteger_2ENum,arr(ty_2Einteger_2Eint,ty_2Enum_2Enum)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Einteger_2ENum) ).
fof(mem_c_2Einteger_2Eint__neg,axiom,
mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__neg) ).
fof(mem_c_2Enum_2E0,axiom,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Enum_2E0) ).
fof(mem_c_2Ebool_2EF,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(mem_c_2Ebool_2ET,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
fof(ax_true_p,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_true_p) ).
fof(ne_ty_2Enum_2Enum,axiom,
ne(ty_2Enum_2Enum),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Enum_2Enum) ).
fof(ne_ty_2Einteger_2Eint,axiom,
ne(ty_2Einteger_2Eint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Einteger_2Eint) ).
fof(ind_ne,axiom,
ne(ind),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ind_ne) ).
fof(bool_ne,axiom,
ne(bool),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',bool_ne) ).
fof(i_0_51,plain,
! [X9] :
( ne(X9)
=> ! [X18] :
( mem(X18,bool)
=> ! [X19] :
( mem(X19,bool)
=> ! [X20] :
( mem(X20,X9)
=> ! [X21] :
( mem(X21,X9)
=> ! [X22] :
( mem(X22,X9)
=> ! [X23] :
( mem(X23,X9)
=> ( ( ( p(X18)
<=> p(X19) )
& ( p(X19)
=> X20 = X21 )
& ( ~ p(X19)
=> X22 = X23 ) )
=> ap(ap(ap(c_2Ebool_2ECOND(X9),X18),X20),X22) = ap(ap(ap(c_2Ebool_2ECOND(X9),X19),X21),X23) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Ebool_2ECOND__CONG]) ).
fof(i_0_52,plain,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ! [X27] :
( mem(X27,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__of__num,X27)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X26),X27)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X27),X26)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__of__num,X27)))
<=> ( X26 != c_2Enum_2E0
| X27 != c_2Enum_2E0 ) )
& ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27)))) ) ) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Einteger_2EINT__LT__CALCULATE]) ).
fof(i_0_53,plain,
! [X160,X161,X162,X163,X164,X165,X166] :
( ( ~ p(X162)
| p(X162)
| ~ p(X161)
| ~ p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( X165 != X166
| p(X162)
| ~ p(X161)
| ~ p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( ~ p(X162)
| X163 != X164
| ~ p(X161)
| ~ p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( X165 != X166
| X163 != X164
| ~ p(X161)
| ~ p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( ~ p(X162)
| p(X162)
| p(X161)
| p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( X165 != X166
| p(X162)
| p(X161)
| p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( ~ p(X162)
| X163 != X164
| p(X161)
| p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) )
& ( X165 != X166
| X163 != X164
| p(X161)
| p(X162)
| ap(ap(ap(c_2Ebool_2ECOND(X160),X161),X163),X165) = ap(ap(ap(c_2Ebool_2ECOND(X160),X162),X164),X166)
| ~ mem(X166,X160)
| ~ mem(X165,X160)
| ~ mem(X164,X160)
| ~ mem(X163,X160)
| ~ mem(X162,bool)
| ~ mem(X161,bool)
| ~ ne(X160) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])])]) ).
fof(i_0_54,plain,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ~ p(ap(ap(c_2Eprim__rec_2E_3C,X26),c_2Enum_2E0)) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Eprim__rec_2ENOT__LESS__0]) ).
fof(i_0_55,negated_conjecture,
~ ! [X9] :
( ne(X9)
=> ap(c_2Einteger__word_2Ei2w(X9),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X9),c_2Enum_2E0) ),
inference(assume_negation,[status(cth)],[conj_thm_2Einteger__word_2Ei2w__0]) ).
fof(i_0_56,plain,
! [X5] :
( mem(X5,bool)
=> ( p(ap(c_2Ebool_2E_7E,X5))
<=> ~ p(X5) ) ),
inference(fof_simplification,[status(thm)],[ax_neg_p]) ).
fof(i_0_57,plain,
! [X115,X116,X117,X118] :
( ( mem(esk1_4(X115,X116,X117,X118),X115)
| X117 = X118
| ~ mem(X118,arr(X115,X116))
| ~ mem(X117,arr(X115,X116)) )
& ( ap(X117,esk1_4(X115,X116,X117,X118)) != ap(X118,esk1_4(X115,X116,X117,X118))
| X117 = X118
| ~ mem(X118,arr(X115,X116))
| ~ mem(X117,arr(X115,X116)) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[funcext])])])])]) ).
fof(i_0_58,plain,
! [X175,X176] :
( ~ ne(X175)
| ~ mem(X176,ty_2Einteger_2Eint)
| ap(c_2Einteger__word_2Ei2w(X175),X176) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X175)),ap(ap(c_2Einteger_2Eint__lt,X176),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X175),ap(c_2Ewords_2En2w(X175),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X176))))),ap(c_2Ewords_2En2w(X175),ap(c_2Einteger_2ENum,X176))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_thm_2Einteger__word_2Ei2w__def])])]) ).
fof(i_0_59,plain,
! [X172,X173] :
( ( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X172)),ap(c_2Einteger_2Eint__of__num,X173)))
| p(ap(ap(c_2Eprim__rec_2E_3C,X172),X173))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( ~ p(ap(ap(c_2Eprim__rec_2E_3C,X172),X173))
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X172)),ap(c_2Einteger_2Eint__of__num,X173)))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X172))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X173))))
| p(ap(ap(c_2Eprim__rec_2E_3C,X173),X172))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( ~ p(ap(ap(c_2Eprim__rec_2E_3C,X173),X172))
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X172))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X173))))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X172))),ap(c_2Einteger_2Eint__of__num,X173)))
| X172 != c_2Enum_2E0
| X173 != c_2Enum_2E0
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( X172 = c_2Enum_2E0
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X172))),ap(c_2Einteger_2Eint__of__num,X173)))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( X173 = c_2Enum_2E0
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X172))),ap(c_2Einteger_2Eint__of__num,X173)))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) )
& ( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X172)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X173))))
| ~ mem(X173,ty_2Enum_2Enum)
| ~ mem(X172,ty_2Enum_2Enum) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])])])]) ).
cnf(i_0_60,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X5),X4),X2),X6) = ap(ap(ap(c_2Ebool_2ECOND(X5),X1),X3),X7)
| ~ p(X1)
| X2 != X3
| ~ p(X4)
| ~ p(X1)
| ~ mem(X7,X5)
| ~ mem(X6,X5)
| ~ mem(X3,X5)
| ~ mem(X2,X5)
| ~ mem(X1,bool)
| ~ mem(X4,bool)
| ~ ne(X5) ),
inference(split_conjunct,[status(thm)],[i_0_53]) ).
cnf(i_0_61,plain,
( p(X3)
| p(X4)
| p(X3)
| ap(ap(ap(c_2Ebool_2ECOND(X5),X4),X6),X1) = ap(ap(ap(c_2Ebool_2ECOND(X5),X3),X7),X2)
| X1 != X2
| ~ mem(X2,X5)
| ~ mem(X1,X5)
| ~ mem(X7,X5)
| ~ mem(X6,X5)
| ~ mem(X3,bool)
| ~ mem(X4,bool)
| ~ ne(X5) ),
inference(split_conjunct,[status(thm)],[i_0_53]) ).
fof(i_0_62,plain,
! [X178,X179,X180] :
( ( ap(c_2Ewords_2En2w(X178),X179) != ap(c_2Ewords_2En2w(X178),X180)
| ap(ap(c_2Earithmetic_2EMOD,X179),ap(c_2Ewords_2Edimword(X178),c_2Ebool_2Ethe__value(X178))) = ap(ap(c_2Earithmetic_2EMOD,X180),ap(c_2Ewords_2Edimword(X178),c_2Ebool_2Ethe__value(X178)))
| ~ mem(X180,ty_2Enum_2Enum)
| ~ mem(X179,ty_2Enum_2Enum)
| ~ ne(X178) )
& ( ap(ap(c_2Earithmetic_2EMOD,X179),ap(c_2Ewords_2Edimword(X178),c_2Ebool_2Ethe__value(X178))) != ap(ap(c_2Earithmetic_2EMOD,X180),ap(c_2Ewords_2Edimword(X178),c_2Ebool_2Ethe__value(X178)))
| ap(c_2Ewords_2En2w(X178),X179) = ap(c_2Ewords_2En2w(X178),X180)
| ~ mem(X180,ty_2Enum_2Enum)
| ~ mem(X179,ty_2Enum_2Enum)
| ~ ne(X178) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ewords_2En2w__11])])])]) ).
fof(i_0_63,plain,
! [X140,X141,X142] :
( ( ~ p(ap(c_2Ebool_2E_21(X140),X141))
| ~ mem(X142,X140)
| p(ap(X141,X142))
| ~ mem(X141,arr(X140,bool))
| ~ ne(X140) )
& ( mem(esk2_2(X140,X141),X140)
| p(ap(c_2Ebool_2E_21(X140),X141))
| ~ mem(X141,arr(X140,bool))
| ~ ne(X140) )
& ( ~ p(ap(X141,esk2_2(X140,X141)))
| p(ap(c_2Ebool_2E_21(X140),X141))
| ~ mem(X141,arr(X140,bool))
| ~ ne(X140) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_all_p])])])])]) ).
fof(i_0_64,plain,
! [X147,X148,X149] :
( ( ~ p(ap(ap(c_2Emin_2E_3D(X147),X148),X149))
| X148 = X149
| ~ mem(X149,X147)
| ~ mem(X148,X147)
| ~ ne(X147) )
& ( X148 != X149
| p(ap(ap(c_2Emin_2E_3D(X147),X148),X149))
| ~ mem(X149,X147)
| ~ mem(X148,X147)
| ~ ne(X147) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_eq_p])])])]) ).
fof(i_0_65,plain,
! [X131] :
( ~ ne(X131)
| mem(c_2Ebool_2ECOND(X131),arr(bool,arr(X131,arr(X131,X131)))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2ECOND])]) ).
fof(i_0_66,plain,
! [X125,X126] :
( ( ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,X125),X126))
| ~ p(X125)
| p(X126)
| ~ mem(X126,bool)
| ~ mem(X125,bool) )
& ( p(X125)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X125),X126))
| ~ mem(X126,bool)
| ~ mem(X125,bool) )
& ( ~ p(X126)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X125),X126))
| ~ mem(X126,bool)
| ~ mem(X125,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_imp_p])])])]) ).
fof(i_0_67,plain,
! [X127,X128] :
( ( ~ p(ap(ap(c_2Ebool_2E_5C_2F,X127),X128))
| p(X127)
| p(X128)
| ~ mem(X128,bool)
| ~ mem(X127,bool) )
& ( ~ p(X127)
| p(ap(ap(c_2Ebool_2E_5C_2F,X127),X128))
| ~ mem(X128,bool)
| ~ mem(X127,bool) )
& ( ~ p(X128)
| p(ap(ap(c_2Ebool_2E_5C_2F,X127),X128))
| ~ mem(X128,bool)
| ~ mem(X127,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_or_p])])])]) ).
fof(i_0_68,plain,
! [X129,X130] :
( ( p(X129)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X129),X130))
| ~ mem(X130,bool)
| ~ mem(X129,bool) )
& ( p(X130)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X129),X130))
| ~ mem(X130,bool)
| ~ mem(X129,bool) )
& ( ~ p(X129)
| ~ p(X130)
| p(ap(ap(c_2Ebool_2E_2F_5C,X129),X130))
| ~ mem(X130,bool)
| ~ mem(X129,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_and_p])])])]) ).
fof(i_0_69,plain,
! [X167,X168,X169,X170,X171] :
( ( ~ mem(X168,X167)
| ~ mem(X169,X167)
| ap(ap(ap(c_2Ebool_2ECOND(X167),c_2Ebool_2ET),X168),X169) = X168
| ~ ne(X167) )
& ( ~ mem(X170,X167)
| ~ mem(X171,X167)
| ap(ap(ap(c_2Ebool_2ECOND(X167),c_2Ebool_2EF),X170),X171) = X171
| ~ ne(X167) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ebool_2Ebool__case__thm])])])]) ).
fof(i_0_70,plain,
! [X145] :
( ~ ne(X145)
| mem(c_2Ewords_2Eword__2comp(X145),arr(ty_2Efcp_2Ecart(bool,X145),ty_2Efcp_2Ecart(bool,X145))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ewords_2Eword__2comp])]) ).
fof(i_0_71,plain,
! [X177] :
( ~ mem(X177,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X177),c_2Enum_2E0)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_54])]) ).
fof(i_0_72,plain,
! [X109,X110,X111,X112] :
( ~ mem(X111,arr(X109,X110))
| ~ mem(X112,X109)
| mem(ap(X111,X112),X110) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])]) ).
fof(i_0_73,plain,
! [X146] :
( ~ ne(X146)
| mem(c_2Emin_2E_3D(X146),arr(X146,arr(X146,bool))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Emin_2E_3D])]) ).
fof(i_0_74,plain,
! [X139] :
( ~ ne(X139)
| mem(c_2Ebool_2E_21(X139),arr(arr(X139,bool),bool)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_21])]) ).
fof(i_0_75,plain,
! [X144] :
( ~ ne(X144)
| mem(c_2Ewords_2En2w(X144),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X144))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ewords_2En2w])]) ).
fof(i_0_76,plain,
! [X134] :
( ~ ne(X134)
| mem(c_2Einteger__word_2Ei2w(X134),arr(ty_2Einteger_2Eint,ty_2Efcp_2Ecart(bool,X134))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Einteger__word_2Ei2w])]) ).
fof(i_0_77,negated_conjecture,
( ne(esk3_0)
& ap(c_2Einteger__word_2Ei2w(esk3_0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) != ap(c_2Ewords_2En2w(esk3_0),c_2Enum_2E0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_55])])]) ).
fof(i_0_78,plain,
! [X181] :
( ~ ne(X181)
| ap(c_2Ewords_2Eword__2comp(X181),ap(c_2Ewords_2En2w(X181),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X181),c_2Enum_2E0) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ewords_2EWORD__NEG__0])]) ).
fof(i_0_79,plain,
! [X135] :
( ( ~ p(ap(c_2Ebool_2E_7E,X135))
| ~ p(X135)
| ~ mem(X135,bool) )
& ( p(X135)
| p(ap(c_2Ebool_2E_7E,X135))
| ~ mem(X135,bool) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_56])])]) ).
fof(i_0_80,plain,
! [X120,X121,X122] :
( ~ mem(X122,X120)
| ap(k(X120,X121),X122) = X121 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kbeta])]) ).
fof(i_0_81,plain,
! [X138] :
( ~ ne(X138)
| mem(c_2Ewords_2Edimword(X138),arr(ty_2Ebool_2Eitself(X138),ty_2Enum_2Enum)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ewords_2Edimword])]) ).
fof(i_0_82,plain,
! [X113,X114] :
( ( ~ p(X113)
| ~ p(X114)
| X113 = X114
| ~ mem(X114,bool)
| ~ mem(X113,bool) )
& ( p(X113)
| p(X114)
| X113 = X114
| ~ mem(X114,bool)
| ~ mem(X113,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[boolext])])])]) ).
fof(i_0_83,plain,
! [X174] :
( ~ mem(X174,ty_2Enum_2Enum)
| ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X174)) = X174 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Einteger_2ENUM__OF__INT])]) ).
fof(i_0_84,plain,
! [X132,X133] :
( ~ ne(X132)
| ~ ne(X133)
| ne(ty_2Efcp_2Ecart(X132,X133)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ne_ty_2Efcp_2Ecart])])]) ).
fof(i_0_85,plain,
! [X107,X108] :
( ~ ne(X107)
| ~ ne(X108)
| ne(arr(X107,X108)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arr_ne])])]) ).
fof(i_0_86,plain,
! [X123,X124] :
( ~ mem(X124,X123)
| ap(i(X123),X124) = X124 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ibeta])]) ).
fof(i_0_87,plain,
! [X137] :
( ~ ne(X137)
| mem(c_2Ebool_2Ethe__value(X137),ty_2Ebool_2Eitself(X137)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2Ethe__value])]) ).
fof(i_0_88,plain,
! [X136] :
( ~ ne(X136)
| ne(ty_2Ebool_2Eitself(X136)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ne_ty_2Ebool_2Eitself])]) ).
fof(i_0_89,plain,
~ p(c_2Ebool_2EF),
inference(fof_simplification,[status(thm)],[ax_false_p]) ).
cnf(i_0_90,plain,
( X1 = X4
| ap(X1,esk1_4(X2,X3,X1,X4)) != ap(X4,esk1_4(X2,X3,X1,X4))
| ~ mem(X4,arr(X2,X3))
| ~ mem(X1,arr(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_91,plain,
( ap(c_2Einteger__word_2Ei2w(X1),X2) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),ap(ap(c_2Einteger_2Eint__lt,X2),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X2))))),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,X2)))
| ~ ne(X1)
| ~ mem(X2,ty_2Einteger_2Eint) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_92,plain,
( p(ap(ap(c_2Eprim__rec_2E_3C,X2),X1))
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X2))))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_93,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))),ap(c_2Einteger_2Eint__of__num,X2)))
| X1 != c_2Enum_2E0
| X2 != c_2Enum_2E0
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_94,plain,
( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X2))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X1),X2))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X2,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_95,plain,
( mem(esk1_4(X1,X2,X3,X4),X1)
| X3 = X4
| ~ mem(X4,arr(X1,X2))
| ~ mem(X3,arr(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_96,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X1)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X2))))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_97,plain,
( p(ap(ap(c_2Eprim__rec_2E_3C,X1),X2))
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X1)),ap(c_2Einteger_2Eint__of__num,X2)))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_98,plain,
( X1 = c_2Enum_2E0
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))),ap(c_2Einteger_2Eint__of__num,X2)))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_99,plain,
( X1 = c_2Enum_2E0
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X2))),ap(c_2Einteger_2Eint__of__num,X1)))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X2,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_100,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X7),X5),X3),X1) = ap(ap(ap(c_2Ebool_2ECOND(X7),X6),X4),X2)
| X1 != X2
| X3 != X4
| ~ p(X5)
| ~ p(X6)
| ~ mem(X2,X7)
| ~ mem(X1,X7)
| ~ mem(X4,X7)
| ~ mem(X3,X7)
| ~ mem(X6,bool)
| ~ mem(X5,bool)
| ~ ne(X7) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_101,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X5),X1),X3),X7) = ap(ap(ap(c_2Ebool_2ECOND(X5),X4),X2),X6)
| X2 != X3
| ~ ne(X5)
| ~ p(X4)
| ~ p(X1)
| ~ mem(X7,X5)
| ~ mem(X6,X5)
| ~ mem(X3,X5)
| ~ mem(X2,X5)
| ~ mem(X4,bool)
| ~ mem(X1,bool) ),
inference(cn,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_102,plain,
( p(X5)
| p(X6)
| ap(ap(ap(c_2Ebool_2ECOND(X7),X5),X3),X1) = ap(ap(ap(c_2Ebool_2ECOND(X7),X6),X4),X2)
| X1 != X2
| X3 != X4
| ~ mem(X2,X7)
| ~ mem(X1,X7)
| ~ mem(X4,X7)
| ~ mem(X3,X7)
| ~ mem(X6,bool)
| ~ mem(X5,bool)
| ~ ne(X7) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_103,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X5),X3),X7),X2) = ap(ap(ap(c_2Ebool_2ECOND(X5),X4),X6),X1)
| p(X4)
| p(X3)
| X1 != X2
| ~ ne(X5)
| ~ mem(X7,X5)
| ~ mem(X6,X5)
| ~ mem(X2,X5)
| ~ mem(X1,X5)
| ~ mem(X4,bool)
| ~ mem(X3,bool) ),
inference(cn,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_104,plain,
( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X1)),ap(c_2Einteger_2Eint__of__num,X2)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X1),X2))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_105,plain,
( ap(c_2Ewords_2En2w(X2),X1) = ap(c_2Ewords_2En2w(X2),X3)
| ap(ap(c_2Earithmetic_2EMOD,X1),ap(c_2Ewords_2Edimword(X2),c_2Ebool_2Ethe__value(X2))) != ap(ap(c_2Earithmetic_2EMOD,X3),ap(c_2Ewords_2Edimword(X2),c_2Ebool_2Ethe__value(X2)))
| ~ mem(X3,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_106,plain,
( ap(ap(c_2Earithmetic_2EMOD,X2),ap(c_2Ewords_2Edimword(X1),c_2Ebool_2Ethe__value(X1))) = ap(ap(c_2Earithmetic_2EMOD,X3),ap(c_2Ewords_2Edimword(X1),c_2Ebool_2Ethe__value(X1)))
| ap(c_2Ewords_2En2w(X1),X2) != ap(c_2Ewords_2En2w(X1),X3)
| ~ mem(X3,ty_2Enum_2Enum)
| ~ mem(X2,ty_2Enum_2Enum)
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_107,plain,
( p(ap(c_2Ebool_2E_21(X2),X1))
| ~ p(ap(X1,esk2_2(X2,X1)))
| ~ mem(X1,arr(X2,bool))
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_108,plain,
( X2 = X3
| ~ p(ap(ap(c_2Emin_2E_3D(X1),X2),X3))
| ~ mem(X3,X1)
| ~ mem(X2,X1)
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_109,plain,
( mem(c_2Ebool_2ECOND(X1),arr(bool,arr(X1,arr(X1,X1))))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_110,plain,
( p(ap(X2,X3))
| ~ p(ap(c_2Ebool_2E_21(X1),X2))
| ~ mem(X3,X1)
| ~ mem(X2,arr(X1,bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_111,plain,
( p(X2)
| ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,X1),X2))
| ~ p(X1)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_112,plain,
( p(X1)
| p(X2)
| ~ p(ap(ap(c_2Ebool_2E_5C_2F,X1),X2))
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_113,plain,
( p(X1)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X1),X2))
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_114,plain,
( p(X1)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X2),X1))
| ~ mem(X1,bool)
| ~ mem(X2,bool) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_115,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X2),c_2Ebool_2EF),X1),X3) = X3
| ~ mem(X1,X2)
| ~ mem(X3,X2)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_116,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X2),c_2Ebool_2ET),X1),X3) = X1
| ~ mem(X1,X2)
| ~ mem(X3,X2)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_117,plain,
( p(ap(ap(c_2Emin_2E_3D(X3),X1),X2))
| X1 != X2
| ~ mem(X2,X3)
| ~ mem(X1,X3)
| ~ ne(X3) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_118,plain,
( mem(esk2_2(X1,X2),X1)
| p(ap(c_2Ebool_2E_21(X1),X2))
| ~ mem(X2,arr(X1,bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_119,plain,
( mem(c_2Ewords_2Eword__2comp(X1),arr(ty_2Efcp_2Ecart(bool,X1),ty_2Efcp_2Ecart(bool,X1)))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_120,plain,
( ~ mem(X1,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X1),c_2Enum_2E0)) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_121,plain,
( p(ap(ap(c_2Ebool_2E_2F_5C,X1),X2))
| ~ p(X1)
| ~ p(X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_122,plain,
( mem(ap(X1,X4),X3)
| ~ mem(X1,arr(X2,X3))
| ~ mem(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_123,plain,
( p(ap(ap(c_2Ebool_2E_5C_2F,X1),X2))
| ~ p(X1)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_124,plain,
( p(ap(ap(c_2Ebool_2E_5C_2F,X2),X1))
| ~ p(X1)
| ~ mem(X1,bool)
| ~ mem(X2,bool) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_125,plain,
( p(ap(ap(c_2Emin_2E_3D_3D_3E,X2),X1))
| ~ p(X1)
| ~ mem(X1,bool)
| ~ mem(X2,bool) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_126,plain,
( p(X1)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X1),X2))
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_127,plain,
( mem(c_2Emin_2E_3D(X1),arr(X1,arr(X1,bool)))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_128,plain,
( mem(c_2Ebool_2E_21(X1),arr(arr(X1,bool),bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_129,plain,
( mem(c_2Ewords_2En2w(X1),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X1)))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_130,plain,
( mem(c_2Einteger__word_2Ei2w(X1),arr(ty_2Einteger_2Eint,ty_2Efcp_2Ecart(bool,X1)))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_131,negated_conjecture,
ap(c_2Einteger__word_2Ei2w(esk3_0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) != ap(c_2Ewords_2En2w(esk3_0),c_2Enum_2E0),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_132,plain,
( ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_133,plain,
mem(c_2Earithmetic_2EMOD,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))),
inference(split_conjunct,[status(thm)],[mem_c_2Earithmetic_2EMOD]),
[final] ).
cnf(i_0_134,plain,
mem(c_2Eprim__rec_2E_3C,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Eprim__rec_2E_3C]),
[final] ).
cnf(i_0_135,plain,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2Eint__lt]),
[final] ).
cnf(i_0_136,plain,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_2F_5C]),
[final] ).
cnf(i_0_137,plain,
mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_5C_2F]),
[final] ).
cnf(i_0_138,plain,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Emin_2E_3D_3D_3E]),
[final] ).
cnf(i_0_139,plain,
( ~ p(ap(c_2Ebool_2E_7E,X1))
| ~ p(X1)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_140,plain,
( ap(k(X2,X3),X1) = X3
| ~ mem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_141,plain,
( mem(c_2Ewords_2Edimword(X1),arr(ty_2Ebool_2Eitself(X1),ty_2Enum_2Enum))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_142,plain,
( X1 = X2
| ~ p(X1)
| ~ p(X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_143,plain,
( ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X1)) = X1
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_144,plain,
( p(X1)
| p(ap(c_2Ebool_2E_7E,X1))
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_145,plain,
( p(X1)
| p(X2)
| X1 = X2
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_146,plain,
( ne(ty_2Efcp_2Ecart(X1,X2))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_147,plain,
( ne(arr(X1,X2))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_148,plain,
( ap(i(X2),X1) = X1
| ~ mem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_149,plain,
ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
inference(split_conjunct,[status(thm)],[conj_thm_2Einteger_2EINT__NEG__0]),
[final] ).
cnf(i_0_150,plain,
( mem(c_2Ebool_2Ethe__value(X1),ty_2Ebool_2Eitself(X1))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_151,plain,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_7E]),
[final] ).
cnf(i_0_152,plain,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2Eint__of__num]),
[final] ).
cnf(i_0_153,plain,
mem(c_2Einteger_2ENum,arr(ty_2Einteger_2Eint,ty_2Enum_2Enum)),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2ENum]),
[final] ).
cnf(i_0_154,plain,
mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2Eint__neg]),
[final] ).
cnf(i_0_155,plain,
( ne(ty_2Ebool_2Eitself(X1))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_156,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
inference(split_conjunct,[status(thm)],[mem_c_2Enum_2E0]),
[final] ).
cnf(i_0_157,plain,
mem(c_2Ebool_2EF,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2EF]),
[final] ).
cnf(i_0_158,plain,
mem(c_2Ebool_2ET,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2ET]),
[final] ).
cnf(i_0_159,plain,
~ p(c_2Ebool_2EF),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_160,plain,
p(c_2Ebool_2ET),
inference(split_conjunct,[status(thm)],[ax_true_p]),
[final] ).
cnf(i_0_161,negated_conjecture,
ne(esk3_0),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_162,plain,
ne(ty_2Enum_2Enum),
inference(split_conjunct,[status(thm)],[ne_ty_2Enum_2Enum]),
[final] ).
cnf(i_0_163,plain,
ne(ty_2Einteger_2Eint),
inference(split_conjunct,[status(thm)],[ne_ty_2Einteger_2Eint]),
[final] ).
cnf(i_0_164,plain,
ne(ind),
inference(split_conjunct,[status(thm)],[ind_ne]),
[final] ).
cnf(i_0_165,plain,
ne(bool),
inference(split_conjunct,[status(thm)],[bool_ne]),
[final] ).
cnf(i_0_166,axiom,
X1 = X1 ).
cnf(i_0_167,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_168,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_169,axiom,
( X1 != X2
| ap(X1,X3) = ap(X2,X3) ) ).
cnf(i_0_170,axiom,
( X1 != X2
| ap(X3,X1) = ap(X3,X2) ) ).
cnf(i_0_171,axiom,
( X1 != X2
| ~ mem(X1,X3)
| mem(X2,X3) ) ).
cnf(i_0_172,axiom,
( X1 != X2
| ~ mem(X3,X1)
| mem(X3,X2) ) ).
cnf(i_0_173,axiom,
( X1 != X2
| ~ ne(X1)
| ne(X2) ) ).
cnf(i_0_174,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_285,plain,
~ p(ap(c_2Ebool_2E_21(bool),c_2Ebool_2E_7E)),
inference(scs_inference,[],[i_0_131,i_0_153,i_0_154,i_0_138,i_0_181,i_0_156,i_0_157,i_0_158,i_0_151,i_0_160,i_0_163,i_0_165,i_0_159,i_0_169,i_0_170,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_120,i_0_127,i_0_128,i_0_129,i_0_130,i_0_143,i_0_109,i_0_119,i_0_132,i_0_167,i_0_168,i_0_146,i_0_147,i_0_139,i_0_144,i_0_122,i_0_96,i_0_174,i_0_113,i_0_123,i_0_125,i_0_126,i_0_115,i_0_116,i_0_97,i_0_92,i_0_112,i_0_121,i_0_110]) ).
cnf(i_0_288,plain,
~ p(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),c_2Ebool_2EF)),
inference(scs_inference,[],[i_0_131,i_0_153,i_0_154,i_0_138,i_0_181,i_0_156,i_0_157,i_0_158,i_0_151,i_0_160,i_0_163,i_0_165,i_0_159,i_0_169,i_0_170,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_120,i_0_127,i_0_128,i_0_129,i_0_130,i_0_143,i_0_109,i_0_119,i_0_132,i_0_167,i_0_168,i_0_146,i_0_147,i_0_139,i_0_144,i_0_122,i_0_96,i_0_174,i_0_113,i_0_123,i_0_125,i_0_126,i_0_115,i_0_116,i_0_97,i_0_92,i_0_112,i_0_121,i_0_110,i_0_171,i_0_114]) ).
cnf(i_0_290,plain,
p(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET)),
inference(scs_inference,[],[i_0_131,i_0_153,i_0_154,i_0_138,i_0_181,i_0_156,i_0_157,i_0_158,i_0_151,i_0_160,i_0_163,i_0_165,i_0_159,i_0_169,i_0_170,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_120,i_0_127,i_0_128,i_0_129,i_0_130,i_0_143,i_0_109,i_0_119,i_0_132,i_0_167,i_0_168,i_0_146,i_0_147,i_0_139,i_0_144,i_0_122,i_0_96,i_0_174,i_0_113,i_0_123,i_0_125,i_0_126,i_0_115,i_0_116,i_0_97,i_0_92,i_0_112,i_0_121,i_0_110,i_0_171,i_0_114,i_0_124]) ).
cnf(i_0_292,plain,
~ p(ap(c_2Ebool_2E_7E,esk2_2(bool,c_2Ebool_2E_7E))),
inference(scs_inference,[],[i_0_131,i_0_153,i_0_154,i_0_138,i_0_181,i_0_156,i_0_157,i_0_158,i_0_151,i_0_160,i_0_163,i_0_165,i_0_159,i_0_169,i_0_170,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_120,i_0_127,i_0_128,i_0_129,i_0_130,i_0_143,i_0_109,i_0_119,i_0_132,i_0_167,i_0_168,i_0_146,i_0_147,i_0_139,i_0_144,i_0_122,i_0_96,i_0_174,i_0_113,i_0_123,i_0_125,i_0_126,i_0_115,i_0_116,i_0_97,i_0_92,i_0_112,i_0_121,i_0_110,i_0_171,i_0_114,i_0_124,i_0_107]) ).
cnf(i_0_296,plain,
~ p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF)),
inference(scs_inference,[],[i_0_131,i_0_182,i_0_153,i_0_154,i_0_138,i_0_181,i_0_156,i_0_157,i_0_158,i_0_151,i_0_160,i_0_163,i_0_165,i_0_159,i_0_169,i_0_170,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_120,i_0_127,i_0_128,i_0_129,i_0_130,i_0_143,i_0_109,i_0_119,i_0_132,i_0_167,i_0_168,i_0_146,i_0_147,i_0_139,i_0_144,i_0_122,i_0_96,i_0_174,i_0_113,i_0_123,i_0_125,i_0_126,i_0_115,i_0_116,i_0_97,i_0_92,i_0_112,i_0_121,i_0_110,i_0_171,i_0_114,i_0_124,i_0_107,i_0_180,i_0_108]) ).
cnf(i_0_298,plain,
~ p(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF)),
inference(scs_inference,[],[i_0_131,i_0_182,i_0_153,i_0_154,i_0_138,i_0_181,i_0_156,i_0_157,i_0_158,i_0_151,i_0_160,i_0_163,i_0_165,i_0_159,i_0_169,i_0_170,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_120,i_0_127,i_0_128,i_0_129,i_0_130,i_0_143,i_0_109,i_0_119,i_0_132,i_0_167,i_0_168,i_0_146,i_0_147,i_0_139,i_0_144,i_0_122,i_0_96,i_0_174,i_0_113,i_0_123,i_0_125,i_0_126,i_0_115,i_0_116,i_0_97,i_0_92,i_0_112,i_0_121,i_0_110,i_0_171,i_0_114,i_0_124,i_0_107,i_0_180,i_0_108,i_0_111]) ).
cnf(i_0_186,plain,
ne(esk3_0),
inference(equality_inference,[],[185]) ).
cnf(i_0_187,plain,
ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),c_2Enum_2E0),c_2Enum_2E0) != c_2Ebool_2EF,
inference(scs_inference,[],[i_0_183,i_0_159,i_0_174]) ).
cnf(i_0_188,plain,
p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2EF),c_2Ebool_2EF)),
inference(scs_inference,[],[i_0_183,i_0_157,i_0_165,i_0_159,i_0_174,i_0_180]) ).
cnf(i_0_301,plain,
mem(c_2Einteger_2ENum,arr(ty_2Einteger_2Eint,ty_2Enum_2Enum)),
inference(equality_inference,[],[287]) ).
cnf(i_0_302,plain,
ne(ty_2Ebool_2Eitself(arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint))),
inference(scs_inference,[],[i_0_254,i_0_155]) ).
cnf(i_0_306,plain,
ap(i(arr(bool,bool)),ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF)) = ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF),
inference(scs_inference,[],[i_0_254,i_0_260,i_0_155,i_0_150,i_0_148]) ).
cnf(i_0_308,plain,
ap(k(arr(bool,bool),X1),ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2EF)) = X1,
inference(scs_inference,[],[i_0_254,i_0_260,i_0_155,i_0_150,i_0_148,i_0_140]) ).
cnf(i_0_326,plain,
ap(ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),X1) = ap(c_2Enum_2E0,X1),
inference(scs_inference,[],[i_0_254,i_0_260,i_0_242,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_127,i_0_128,i_0_129,i_0_130,i_0_109,i_0_119,i_0_132,i_0_169]) ).
cnf(i_0_327,plain,
ap(X1,ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) = ap(X1,c_2Enum_2E0),
inference(scs_inference,[],[i_0_254,i_0_260,i_0_242,i_0_155,i_0_150,i_0_148,i_0_140,i_0_141,i_0_127,i_0_128,i_0_129,i_0_130,i_0_109,i_0_119,i_0_132,i_0_169,i_0_170]) ).
cnf(i_0_338,plain,
ap(k(arr(ty_2Einteger_2Eint,ty_2Enum_2Enum),X1),c_2Einteger_2ENum) = X1,
inference(rename_variables,[],[i_0_228]) ).
cnf(i_0_340,plain,
ap(k(arr(ty_2Einteger_2Eint,ty_2Enum_2Enum),X1),c_2Einteger_2ENum) = X1,
inference(rename_variables,[],[i_0_228]) ).
cnf(i_0_354,plain,
ap(k(arr(ty_2Einteger_2Eint,ty_2Enum_2Enum),X1),c_2Einteger_2ENum) = X1,
inference(rename_variables,[],[i_0_228]) ).
cnf(i_0_362,plain,
ne(ty_2Ebool_2Eitself(ty_2Efcp_2Ecart(ty_2Einteger_2Eint,ty_2Einteger_2Eint))),
inference(scs_inference,[],[i_0_252,i_0_155]) ).
cnf(i_0_191,plain,
ne(ty_2Einteger_2Eint),
inference(equality_inference,[],[190]) ).
cnf(i_0_192,plain,
ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2EF),c_2Ebool_2EF) != c_2Ebool_2EF,
inference(scs_inference,[],[i_0_188,i_0_159,i_0_174]) ).
cnf(i_0_193,plain,
p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2ET)),
inference(scs_inference,[],[i_0_188,i_0_158,i_0_165,i_0_159,i_0_174,i_0_180]) ).
cnf(c_0_349,plain,
( mem(ap(X1,X2),X3)
| ~ mem(X1,arr(X4,X3))
| ~ mem(X2,X4) ),
i_0_122 ).
cnf(c_0_350,plain,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
i_0_135 ).
cnf(c_0_351,plain,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
i_0_152 ).
cnf(c_0_352,plain,
( p(X1)
| p(X2)
| X1 = X2
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
i_0_145 ).
cnf(c_0_353,plain,
mem(c_2Ebool_2EF,bool),
i_0_157 ).
cnf(c_0_354,plain,
~ p(c_2Ebool_2EF),
i_0_159 ).
cnf(c_0_355,plain,
( mem(ap(c_2Einteger_2Eint__lt,X1),arr(ty_2Einteger_2Eint,bool))
| ~ mem(X1,ty_2Einteger_2Eint) ),
inference(spm,[status(thm)],[c_0_349,c_0_350]) ).
cnf(c_0_356,plain,
( mem(ap(c_2Einteger_2Eint__of__num,X1),ty_2Einteger_2Eint)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(spm,[status(thm)],[c_0_349,c_0_351]) ).
cnf(c_0_357,plain,
ap(X1,ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) = ap(X1,c_2Enum_2E0),
i_0_327 ).
cnf(c_0_358,plain,
( ap(i(X1),X2) = X2
| ~ mem(X2,X1) ),
i_0_148 ).
cnf(c_0_359,plain,
( X1 = c_2Ebool_2EF
| p(X1)
| ~ mem(X1,bool) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_352,c_0_353]),c_0_354]) ).
cnf(c_0_360,plain,
( mem(ap(ap(c_2Einteger_2Eint__lt,X1),X2),bool)
| ~ mem(X2,ty_2Einteger_2Eint)
| ~ mem(X1,ty_2Einteger_2Eint) ),
inference(spm,[status(thm)],[c_0_349,c_0_355]) ).
cnf(c_0_361,plain,
( mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ~ mem(ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ty_2Enum_2Enum) ),
inference(spm,[status(thm)],[c_0_356,c_0_357]) ).
cnf(c_0_362,plain,
( ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X1)) = X1
| ~ mem(X1,ty_2Enum_2Enum) ),
i_0_143 ).
cnf(c_0_363,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
i_0_156 ).
cnf(c_0_364,plain,
( ap(i(X1),c_2Enum_2E0) = ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))
| ~ mem(ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),X1) ),
inference(spm,[status(thm)],[c_0_357,c_0_358]) ).
cnf(c_0_365,plain,
mem(c_2Einteger_2ENum,arr(ty_2Einteger_2Eint,ty_2Enum_2Enum)),
i_0_153 ).
cnf(c_0_366,plain,
( ap(ap(c_2Einteger_2Eint__lt,X1),X2) = c_2Ebool_2EF
| p(ap(ap(c_2Einteger_2Eint__lt,X1),X2))
| ~ mem(X2,ty_2Einteger_2Eint)
| ~ mem(X1,ty_2Einteger_2Eint) ),
inference(spm,[status(thm)],[c_0_359,c_0_360]) ).
cnf(c_0_367,plain,
mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_361,c_0_362]),c_0_363])]) ).
cnf(c_0_368,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))),ap(c_2Einteger_2Eint__of__num,X2)))
| X1 != c_2Enum_2E0
| X2 != c_2Enum_2E0
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
i_0_93 ).
cnf(c_0_369,plain,
ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
i_0_149 ).
cnf(c_0_370,plain,
( ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = c_2Enum_2E0
| ~ mem(ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),X1)
| ~ mem(c_2Enum_2E0,X1) ),
inference(spm,[status(thm)],[c_0_358,c_0_364]) ).
cnf(c_0_371,plain,
( mem(ap(c_2Einteger_2ENum,X1),ty_2Enum_2Enum)
| ~ mem(X1,ty_2Einteger_2Eint) ),
inference(spm,[status(thm)],[c_0_349,c_0_365]) ).
cnf(c_0_372,plain,
( ap(ap(c_2Einteger_2Eint__lt,X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = c_2Ebool_2EF
| p(ap(ap(c_2Einteger_2Eint__lt,X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)))
| ~ mem(X1,ty_2Einteger_2Eint) ),
inference(spm,[status(thm)],[c_0_366,c_0_367]) ).
cnf(c_0_373,plain,
~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_368])]),c_0_369]),c_0_363])]) ).
cnf(c_0_374,plain,
( ap(c_2Einteger__word_2Ei2w(X1),X2) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),ap(ap(c_2Einteger_2Eint__lt,X2),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X2))))),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,X2)))
| ~ ne(X1)
| ~ mem(X2,ty_2Einteger_2Eint) ),
i_0_91 ).
cnf(c_0_375,plain,
ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = c_2Enum_2E0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_370,c_0_371]),c_0_363]),c_0_367])]) ).
cnf(c_0_376,plain,
ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = c_2Ebool_2EF,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_372,c_0_367]),c_0_373]) ).
cnf(c_0_377,plain,
( ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),c_2Ebool_2EF),ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0))),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))
| ~ ne(X1) ),
inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_374,c_0_375]),c_0_369]),c_0_375]),c_0_367])]),c_0_376]) ).
cnf(c_0_378,plain,
( ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)
| ~ ne(X1) ),
i_0_132 ).
cnf(c_0_379,plain,
( ap(ap(ap(c_2Ebool_2ECOND(X1),c_2Ebool_2EF),X2),X3) = X3
| ~ mem(X2,X1)
| ~ mem(X3,X1)
| ~ ne(X1) ),
i_0_115 ).
cnf(c_0_380,plain,
( ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),c_2Ebool_2EF),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))
| ~ ne(X1) ),
inference(spm,[status(thm)],[c_0_377,c_0_378]) ).
cnf(c_0_381,plain,
( mem(c_2Ewords_2En2w(X1),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X1)))
| ~ ne(X1) ),
i_0_129 ).
cnf(c_0_382,plain,
( ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)
| ~ ne(ty_2Efcp_2Ecart(bool,X1))
| ~ ne(X1)
| ~ mem(ap(c_2Ewords_2En2w(X1),c_2Enum_2E0),ty_2Efcp_2Ecart(bool,X1)) ),
inference(spm,[status(thm)],[c_0_379,c_0_380]) ).
cnf(c_0_383,plain,
( mem(ap(c_2Ewords_2En2w(X1),X2),ty_2Efcp_2Ecart(bool,X1))
| ~ ne(X1)
| ~ mem(X2,ty_2Enum_2Enum) ),
inference(spm,[status(thm)],[c_0_349,c_0_381]) ).
cnf(c_0_384,negated_conjecture,
ap(c_2Einteger__word_2Ei2w(esk3_0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) != ap(c_2Ewords_2En2w(esk3_0),c_2Enum_2E0),
i_0_131 ).
cnf(c_0_385,plain,
( ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)
| ~ ne(ty_2Efcp_2Ecart(bool,X1))
| ~ ne(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_382,c_0_383]),c_0_363])]) ).
cnf(c_0_386,negated_conjecture,
ne(esk3_0),
i_0_161 ).
cnf(c_0_387,negated_conjecture,
~ ne(ty_2Efcp_2Ecart(bool,esk3_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_384,c_0_385]),c_0_386])]) ).
cnf(c_0_388,plain,
( ne(ty_2Efcp_2Ecart(X1,X2))
| ~ ne(X1)
| ~ ne(X2) ),
i_0_146 ).
cnf(c_0_389,plain,
ne(bool),
i_0_165 ).
cnf(c_0_390,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_387,c_0_388]),c_0_386]),c_0_389])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : ITP015+2 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.00/0.11 % 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.15/0.32 % Computer : n007.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 19:40:09 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 113.13/90.92 % Version : CSE_E---1.7
% 113.13/90.92 % Problem : theBenchmark.p
% 113.13/90.92 % SZS status Theorem for theBenchmark.p
% 113.13/90.92 % SZS output start CNFRefutation
% See solution above
% 116.26/94.05 % Total time : 90.424s
%------------------------------------------------------------------------------