%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ITP019+2 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n024.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:40 PM UTC 2026
% Result : Theorem 0.13s 1.52s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 51)
% Comments :
%------------------------------------------------------------------------------
fof(ax_neg_p,axiom,
! [X5] :
( mem(X5,bool)
=> ( p(ap(c_2Ebool_2E_7E,X5))
<=> ~ p(X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_neg_p) ).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__NZ,conjecture,
! [X14] :
( mem(X14,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
=> ( X14 != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
=> ap(c_2Ecomplex_2Ecomplex__inv,X14) != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ecomplex_2ECOMPLEX__INV__NZ) ).
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/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',funcext) ).
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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax_eq_p) ).
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/sandbox2/benchmark/theBenchmark.p',ax_imp_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/sandbox2/benchmark/theBenchmark.p',ax_and_p) ).
fof(ap_tp,axiom,
! [X1,X2,X3] :
( mem(X3,arr(X1,X2))
=> ! [X4] :
( mem(X4,X1)
=> mem(ap(X3,X4),X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__EQ__0,axiom,
! [X14] :
( mem(X14,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
=> ( ap(c_2Ecomplex_2Ecomplex__inv,X14) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
<=> X14 = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ecomplex_2ECOMPLEX__INV__EQ__0) ).
fof(mem_c_2Emin_2E_3D,axiom,
! [X11] :
( ne(X11)
=> mem(c_2Emin_2E_3D(X11),arr(X11,arr(X11,bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D) ).
fof(mem_c_2Ebool_2E_21,axiom,
! [X11] :
( ne(X11)
=> mem(c_2Ebool_2E_21(X11),arr(arr(X11,bool),bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2E_21) ).
fof(conj_thm_2Ebool_2EFORALL__SIMP,axiom,
! [X11] :
( ne(X11)
=> ! [X12] :
( mem(X12,bool)
=> ( ! [X13] :
( mem(X13,X11)
=> p(X12) )
<=> p(X12) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2EFORALL__SIMP) ).
fof(kbeta,axiom,
! [X1,X8,X4] :
( mem(X4,X1)
=> ap(k(X1,X8),X4) = X8 ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',kbeta) ).
fof(boolext,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( ( p(X5)
<=> p(X6) )
=> X5 = X6 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
fof(ne_ty_2Epair_2Eprod,axiom,
! [X9] :
( ne(X9)
=> ! [X10] :
( ne(X10)
=> ne(ty_2Epair_2Eprod(X9,X10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Epair_2Eprod) ).
fof(arr_ne,axiom,
! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ne(arr(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',arr_ne) ).
fof(ibeta,axiom,
! [X1,X4] :
( mem(X4,X1)
=> ap(i(X1),X4) = X4 ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ibeta) ).
fof(ax_false_p,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
fof(mem_c_2Ecomplex_2Ecomplex__inv,axiom,
mem(c_2Ecomplex_2Ecomplex__inv,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ecomplex_2Ecomplex__inv) ).
fof(mem_c_2Ecomplex_2Ecomplex__of__num,axiom,
mem(c_2Ecomplex_2Ecomplex__of__num,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ecomplex_2Ecomplex__of__num) ).
fof(mem_c_2Ebool_2E_2F_5C,axiom,
mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2E_2F_5C) ).
fof(mem_c_2Emin_2E_3D_3D_3E,axiom,
mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D_3D_3E) ).
fof(mem_c_2Ebool_2E_7E,axiom,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2E_7E) ).
fof(mem_c_2Enum_2E0,axiom,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Enum_2E0) ).
fof(mem_c_2Ebool_2ET,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
fof(mem_c_2Ebool_2EF,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(ax_true_p,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
fof(ne_ty_2Erealax_2Ereal,axiom,
ne(ty_2Erealax_2Ereal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Erealax_2Ereal) ).
fof(ne_ty_2Enum_2Enum,axiom,
ne(ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Enum_2Enum) ).
fof(ind_ne,axiom,
ne(ind),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ind_ne) ).
fof(bool_ne,axiom,
ne(bool),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',bool_ne) ).
fof(i_0_31,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_32,negated_conjecture,
~ ! [X14] :
( mem(X14,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
=> ( X14 != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
=> ap(c_2Ecomplex_2Ecomplex__inv,X14) != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ),
inference(assume_negation,[status(cth)],[conj_thm_2Ecomplex_2ECOMPLEX__INV__NZ]) ).
fof(i_0_33,plain,
! [X62,X63,X64,X65] :
( ( mem(esk1_4(X62,X63,X64,X65),X62)
| X64 = X65
| ~ mem(X65,arr(X62,X63))
| ~ mem(X64,arr(X62,X63)) )
& ( ap(X64,esk1_4(X62,X63,X64,X65)) != ap(X65,esk1_4(X62,X63,X64,X65))
| X64 = X65
| ~ mem(X65,arr(X62,X63))
| ~ mem(X64,arr(X62,X63)) ) ),
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_34,plain,
! [X84,X85,X86] :
( ( ~ p(ap(c_2Ebool_2E_21(X84),X85))
| ~ mem(X86,X84)
| p(ap(X85,X86))
| ~ mem(X85,arr(X84,bool))
| ~ ne(X84) )
& ( mem(esk2_2(X84,X85),X84)
| p(ap(c_2Ebool_2E_21(X84),X85))
| ~ mem(X85,arr(X84,bool))
| ~ ne(X84) )
& ( ~ p(ap(X85,esk2_2(X84,X85)))
| p(ap(c_2Ebool_2E_21(X84),X85))
| ~ mem(X85,arr(X84,bool))
| ~ ne(X84) ) ),
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_35,plain,
! [X80,X81,X82] :
( ( ~ p(ap(ap(c_2Emin_2E_3D(X80),X81),X82))
| X81 = X82
| ~ mem(X82,X80)
| ~ mem(X81,X80)
| ~ ne(X80) )
& ( X81 != X82
| p(ap(ap(c_2Emin_2E_3D(X80),X81),X82))
| ~ mem(X82,X80)
| ~ mem(X81,X80)
| ~ ne(X80) ) ),
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_36,plain,
! [X73,X74] :
( ( ~ p(ap(ap(c_2Emin_2E_3D_3D_3E,X73),X74))
| ~ p(X73)
| p(X74)
| ~ mem(X74,bool)
| ~ mem(X73,bool) )
& ( p(X73)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X73),X74))
| ~ mem(X74,bool)
| ~ mem(X73,bool) )
& ( ~ p(X74)
| p(ap(ap(c_2Emin_2E_3D_3D_3E,X73),X74))
| ~ mem(X74,bool)
| ~ mem(X73,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_37,plain,
! [X75,X76] :
( ( p(X75)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X75),X76))
| ~ mem(X76,bool)
| ~ mem(X75,bool) )
& ( p(X76)
| ~ p(ap(ap(c_2Ebool_2E_2F_5C,X75),X76))
| ~ mem(X76,bool)
| ~ mem(X75,bool) )
& ( ~ p(X75)
| ~ p(X76)
| p(ap(ap(c_2Ebool_2E_2F_5C,X75),X76))
| ~ mem(X76,bool)
| ~ mem(X75,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_38,plain,
! [X56,X57,X58,X59] :
( ~ mem(X58,arr(X56,X57))
| ~ mem(X59,X56)
| mem(ap(X58,X59),X57) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])]) ).
fof(i_0_39,plain,
! [X92] :
( ( ap(c_2Ecomplex_2Ecomplex__inv,X92) != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| X92 = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| ~ mem(X92,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )
& ( X92 != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| ap(c_2Ecomplex_2Ecomplex__inv,X92) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| ~ mem(X92,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ecomplex_2ECOMPLEX__INV__EQ__0])])]) ).
fof(i_0_40,plain,
! [X79] :
( ~ ne(X79)
| mem(c_2Emin_2E_3D(X79),arr(X79,arr(X79,bool))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Emin_2E_3D])]) ).
fof(i_0_41,plain,
! [X83] :
( ~ ne(X83)
| mem(c_2Ebool_2E_21(X83),arr(arr(X83,bool),bool)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ebool_2E_21])]) ).
fof(i_0_42,plain,
! [X88,X89,X91] :
( ( mem(esk3_2(X88,X89),X88)
| p(X89)
| ~ mem(X89,bool)
| ~ ne(X88) )
& ( ~ p(X89)
| p(X89)
| ~ mem(X89,bool)
| ~ ne(X88) )
& ( ~ p(X89)
| ~ mem(X91,X88)
| p(X89)
| ~ mem(X89,bool)
| ~ ne(X88) ) ),
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)],[conj_thm_2Ebool_2EFORALL__SIMP])])])])])]) ).
fof(i_0_43,plain,
! [X72] :
( ( ~ p(ap(c_2Ebool_2E_7E,X72))
| ~ p(X72)
| ~ mem(X72,bool) )
& ( p(X72)
| p(ap(c_2Ebool_2E_7E,X72))
| ~ mem(X72,bool) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_31])])]) ).
fof(i_0_44,plain,
! [X67,X68,X69] :
( ~ mem(X69,X67)
| ap(k(X67,X68),X69) = X68 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kbeta])]) ).
fof(i_0_45,plain,
! [X60,X61] :
( ( ~ p(X60)
| ~ p(X61)
| X60 = X61
| ~ mem(X61,bool)
| ~ mem(X60,bool) )
& ( p(X60)
| p(X61)
| X60 = X61
| ~ mem(X61,bool)
| ~ mem(X60,bool) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[boolext])])])]) ).
fof(i_0_46,plain,
! [X77,X78] :
( ~ ne(X77)
| ~ ne(X78)
| ne(ty_2Epair_2Eprod(X77,X78)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ne_ty_2Epair_2Eprod])])]) ).
fof(i_0_47,plain,
! [X54,X55] :
( ~ ne(X54)
| ~ ne(X55)
| ne(arr(X54,X55)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arr_ne])])]) ).
fof(i_0_48,plain,
! [X70,X71] :
( ~ mem(X71,X70)
| ap(i(X70),X71) = X71 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ibeta])]) ).
fof(i_0_49,negated_conjecture,
( mem(esk4_0,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
& esk4_0 != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
& ap(c_2Ecomplex_2Ecomplex__inv,esk4_0) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_32])])]) ).
fof(i_0_50,plain,
~ p(c_2Ebool_2EF),
inference(fof_simplification,[status(thm)],[ax_false_p]) ).
cnf(i_0_51,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_33]),
[final] ).
cnf(i_0_52,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_33]),
[final] ).
cnf(i_0_53,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_34]),
[final] ).
cnf(i_0_54,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_35]),
[final] ).
cnf(i_0_55,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_34]),
[final] ).
cnf(i_0_56,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_36]),
[final] ).
cnf(i_0_57,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_37]),
[final] ).
cnf(i_0_58,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_37]),
[final] ).
cnf(i_0_59,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_35]),
[final] ).
cnf(i_0_60,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_34]),
[final] ).
cnf(i_0_61,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_37]),
[final] ).
cnf(i_0_62,plain,
( mem(ap(X1,X4),X3)
| ~ mem(X1,arr(X2,X3))
| ~ mem(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_63,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_36]),
[final] ).
cnf(i_0_64,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_36]),
[final] ).
cnf(i_0_65,plain,
mem(c_2Ecomplex_2Ecomplex__inv,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),
inference(split_conjunct,[status(thm)],[mem_c_2Ecomplex_2Ecomplex__inv]),
[final] ).
cnf(i_0_66,plain,
( X1 = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| ap(c_2Ecomplex_2Ecomplex__inv,X1) != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| ~ mem(X1,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_67,plain,
( mem(c_2Emin_2E_3D(X1),arr(X1,arr(X1,bool)))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_68,plain,
( ap(c_2Ecomplex_2Ecomplex__inv,X1) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| X1 != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)
| ~ mem(X1,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_69,plain,
( mem(c_2Ebool_2E_21(X1),arr(arr(X1,bool),bool))
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_70,plain,
mem(c_2Ecomplex_2Ecomplex__of__num,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),
inference(split_conjunct,[status(thm)],[mem_c_2Ecomplex_2Ecomplex__of__num]),
[final] ).
cnf(i_0_71,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_72,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_73,plain,
( mem(esk3_2(X1,X2),X1)
| p(X2)
| ~ mem(X2,bool)
| ~ ne(X1) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_74,plain,
( ~ p(ap(c_2Ebool_2E_7E,X1))
| ~ p(X1)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_75,plain,
( ap(k(X2,X3),X1) = X3
| ~ mem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_76,plain,
( X1 = X2
| ~ p(X1)
| ~ p(X2)
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_77,plain,
( p(X1)
| p(ap(c_2Ebool_2E_7E,X1))
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_78,plain,
( p(X1)
| p(X2)
| X1 = X2
| ~ mem(X2,bool)
| ~ mem(X1,bool) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_79,plain,
( ne(ty_2Epair_2Eprod(X1,X2))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_80,plain,
( ne(arr(X1,X2))
| ~ ne(X1)
| ~ ne(X2) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_81,plain,
( ap(i(X2),X1) = X1
| ~ mem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_82,negated_conjecture,
mem(esk4_0,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_83,plain,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2E_7E]),
[final] ).
cnf(i_0_84,negated_conjecture,
ap(c_2Ecomplex_2Ecomplex__inv,esk4_0) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_85,negated_conjecture,
esk4_0 != ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_86,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
inference(split_conjunct,[status(thm)],[mem_c_2Enum_2E0]),
[final] ).
cnf(i_0_87,plain,
mem(c_2Ebool_2ET,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2ET]),
[final] ).
cnf(i_0_88,plain,
mem(c_2Ebool_2EF,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2EF]),
[final] ).
cnf(i_0_89,plain,
~ p(c_2Ebool_2EF),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_90,plain,
p(c_2Ebool_2ET),
inference(split_conjunct,[status(thm)],[ax_true_p]),
[final] ).
cnf(i_0_91,plain,
ne(ty_2Erealax_2Ereal),
inference(split_conjunct,[status(thm)],[ne_ty_2Erealax_2Ereal]),
[final] ).
cnf(i_0_92,plain,
ne(ty_2Enum_2Enum),
inference(split_conjunct,[status(thm)],[ne_ty_2Enum_2Enum]),
[final] ).
cnf(i_0_93,plain,
ne(ind),
inference(split_conjunct,[status(thm)],[ind_ne]),
[final] ).
cnf(i_0_94,plain,
ne(bool),
inference(split_conjunct,[status(thm)],[bool_ne]),
[final] ).
cnf(i_0_95,axiom,
X1 = X1 ).
cnf(i_0_96,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_97,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_98,axiom,
( X1 != X2
| ap(X1,X3) = ap(X2,X3) ) ).
cnf(i_0_99,axiom,
( X1 != X2
| ap(X3,X1) = ap(X3,X2) ) ).
cnf(i_0_100,axiom,
( X1 != X2
| ~ mem(X1,X3)
| mem(X2,X3) ) ).
cnf(i_0_101,axiom,
( X1 != X2
| ~ mem(X3,X1)
| mem(X3,X2) ) ).
cnf(i_0_102,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_103,axiom,
( X1 != X2
| ~ ne(X1)
| ne(X2) ) ).
cnf(i_0_95_001,axiom,
X1 = X1 ).
cnf(i_0_96_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_97_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_98_004,axiom,
( X1 != X2
| ap(X1,X3) = ap(X2,X3) ) ).
cnf(i_0_99_005,axiom,
( X1 != X2
| ap(X3,X1) = ap(X3,X2) ) ).
cnf(i_0_100_006,axiom,
( X1 != X2
| ~ mem(X1,X3)
| mem(X2,X3) ) ).
cnf(i_0_101_007,axiom,
( X1 != X2
| ~ mem(X3,X1)
| mem(X3,X2) ) ).
cnf(i_0_102_008,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_103_009,axiom,
( X1 != X2
| ~ ne(X1)
| ne(X2) ) ).
cnf(i_0_104,plain,
( X1 = X1
| ~ mem(X1,arr(X2,X3))
| ~ mem(X1,arr(X2,X3)) ),
inference(equality_inference,[],[51]) ).
cnf(i_0_105,plain,
( ~ mem(X1,X2)
| ~ mem(X1,X2)
| ~ ne(X2)
| p(ap(ap(c_2Emin_2E_3D(X2),X1),X1)) ),
inference(equality_inference,[],[59]) ).
cnf(i_0_106,plain,
( ~ mem(ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
| ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ),
inference(equality_inference,[],[68]) ).
cnf(i_0_107,plain,
$false,
inference(scs_inference,[],[i_0_85,i_0_84,i_0_82,i_0_66]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : ITP019+2 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.07/0.25 % Computer : n024.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Mon May 4 14:43:11 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 % start to proof: theBenchmark
% 0.13/1.52 % Version : CSE_E---1.7
% 0.13/1.52 % Problem : theBenchmark.p
% 0.13/1.52 % SZS status Theorem for theBenchmark.p
% 0.13/1.52 % SZS output start CNFRefutation
% See solution above
% 0.13/1.53 % Total time : 1.263s
%------------------------------------------------------------------------------