%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ITP019+1 : 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:39 PM UTC 2026
% Result : Theorem 0.15s 1.52s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 59)
% Comments :
%------------------------------------------------------------------------------
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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',reserved_2Elogic_2E_7E) ).
fof(thm_2Ecomplex_2ECOMPLEX__INV__NZ,conjecture,
! [X15] :
( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X15) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
=> s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X15))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ecomplex_2ECOMPLEX__INV__NZ) ).
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/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__CLAUSES) ).
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/sandbox2/benchmark/theBenchmark.p',reserved_2Eho_2Es__thm) ).
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/sandbox2/benchmark/theBenchmark.p',reserved_2Eho_2Eeq__ext) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Ebool_2E_2F_5C_2E2) ).
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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',reserved_2Equant_2E_3F) ).
fof(arityeq1_2Ec_2Ecomplex_2Ecomplex__inv_2E1,axiom,
! [X13] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X13))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__inv_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X13))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Ecomplex_2Ecomplex__inv_2E1) ).
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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a) ).
fof(thm_2Ecomplex_2ECOMPLEX__INV__EQ__0,axiom,
! [X15] :
( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X15))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
<=> s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X15) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ecomplex_2ECOMPLEX__INV__EQ__0) ).
fof(arityeq1_2Ec_2Ecomplex_2Ecomplex__of__num_2E1,axiom,
! [X13] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,X13))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__of__num_2E0),s(tyop_2Enum_2Enum,X13))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Ecomplex_2Ecomplex__of__num_2E1) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',reserved_2Eho_2Ei__thm) ).
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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',reserved_2Eho_2Enotfalse) ).
fof(thm_2Ebool_2ETRUTH,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH) ).
fof(reserved_2Eho_2Etruth,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reserved_2Eho_2Etruth) ).
fof(i_0_28,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_29,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_30,negated_conjecture,
~ ! [X15] :
( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X15) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
=> s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X15))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
inference(assume_negation,[status(cth)],[thm_2Ecomplex_2ECOMPLEX__INV__NZ]) ).
fof(i_0_31,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_32,plain,
! [X88,X89,X90,X91,X92,X93] : s(X90,app_2E2(s(tyop_2Emin_2Efun(X88,X90),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X88,X89),tyop_2Emin_2Efun(X88,X90)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X88,tyop_2Emin_2Efun(X89,X90)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X88,X89),tyop_2Emin_2Efun(X88,X90))),combin_s_2E0),s(tyop_2Emin_2Efun(X88,tyop_2Emin_2Efun(X89,X90)),X91))),s(tyop_2Emin_2Efun(X88,X89),X92))),s(X88,X93))) = s(X90,app_2E2(s(tyop_2Emin_2Efun(X89,X90),app_2E2(s(tyop_2Emin_2Efun(X88,tyop_2Emin_2Efun(X89,X90)),X91),s(X88,X93))),s(X89,app_2E2(s(tyop_2Emin_2Efun(X88,X89),X92),s(X88,X93))))),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Es__thm]) ).
fof(i_0_33,plain,
! [X74,X75,X76,X77] :
( s(X75,app_2E2(s(tyop_2Emin_2Efun(X74,X75),X76),s(X74,esk1_4(X74,X75,X76,X77)))) != s(X75,app_2E2(s(tyop_2Emin_2Efun(X74,X75),X77),s(X74,esk1_4(X74,X75,X76,X77))))
| s(tyop_2Emin_2Efun(X74,X75),X76) = s(tyop_2Emin_2Efun(X74,X75),X77) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Eho_2Eeq__ext])])]) ).
fof(i_0_34,plain,
! [X123,X124,X125] :
( ( s(X123,X124) != s(X123,X125)
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X123,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X123,tyop_2Emin_2Efun(X123,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X123,X124))),s(X123,X125)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X123,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X123,tyop_2Emin_2Efun(X123,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X123,X124))),s(X123,X125))))
| s(X123,X124) = s(X123,X125) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a])]) ).
fof(i_0_35,plain,
! [X121,X122] :
( ( p(s(tyop_2Emin_2Ebool,X121))
| 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,X121))),s(tyop_2Emin_2Ebool,X122)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X122))
| 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,X121))),s(tyop_2Emin_2Ebool,X122)))) )
& ( ~ 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,X121))),s(tyop_2Emin_2Ebool,X122))))
| ~ p(s(tyop_2Emin_2Ebool,X121))
| p(s(tyop_2Emin_2Ebool,X122)) ) ),
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_36,plain,
! [X118,X119] :
( ( ~ p(s(tyop_2Emin_2Ebool,X118))
| 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,X118))),s(tyop_2Emin_2Ebool,X119)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X119))
| 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,X118))),s(tyop_2Emin_2Ebool,X119)))) )
& ( ~ 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,X118))),s(tyop_2Emin_2Ebool,X119))))
| p(s(tyop_2Emin_2Ebool,X118))
| p(s(tyop_2Emin_2Ebool,X119)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Ebool_2E_5C_2F_2E2])])]) ).
fof(i_0_37,plain,
! [X116,X117] :
( ( ~ p(s(tyop_2Emin_2Ebool,X116))
| ~ p(s(tyop_2Emin_2Ebool,X117))
| 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,X116))),s(tyop_2Emin_2Ebool,X117)))) )
& ( p(s(tyop_2Emin_2Ebool,X116))
| ~ 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,X116))),s(tyop_2Emin_2Ebool,X117)))) )
& ( p(s(tyop_2Emin_2Ebool,X117))
| ~ 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,X116))),s(tyop_2Emin_2Ebool,X117)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Ebool_2E_2F_5C_2E2])])]) ).
fof(i_0_38,plain,
! [X84,X85,X86,X87] : s(X84,app_2E2(s(tyop_2Emin_2Efun(X85,X84),app_2E2(s(tyop_2Emin_2Efun(X84,tyop_2Emin_2Efun(X85,X84)),combin_k_2E0),s(X84,X86))),s(X85,X87))) = s(X84,X86),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Ek__thm]) ).
fof(i_0_39,plain,
! [X104,X105,X106,X107,X108] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X104,tyop_2Emin_2Ebool),X105))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X104,tyop_2Emin_2Ebool),X105),s(X104,X106)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X107,tyop_2Emin_2Ebool),X108),s(X107,esk2_2(X107,X108)))))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X107,tyop_2Emin_2Ebool),X108)))) ) ),
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_40,plain,
! [X110,X111,X113,X114,X115] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X110,tyop_2Emin_2Ebool),X111))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X110,tyop_2Emin_2Ebool),X111),s(X110,esk3_2(X110,X111))))) )
& ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X113,tyop_2Emin_2Ebool),X114),s(X113,X115))))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X113,tyop_2Emin_2Ebool),X114)))) ) ),
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_41,plain,
! [X130] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X130))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__inv_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X130))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ecomplex_2Ecomplex__inv_2E1]) ).
fof(i_0_42,plain,
! [X120] :
( ( p(s(tyop_2Emin_2Ebool,X120))
| 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,X120)))) )
& ( ~ 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,X120))))
| ~ p(s(tyop_2Emin_2Ebool,X120)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_28])]) ).
fof(i_0_43,plain,
! [X128,X129] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X128,tyop_2Emin_2Ebool),X129))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X128,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(X128,tyop_2Emin_2Ebool),X129))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a]) ).
fof(i_0_44,plain,
! [X126,X127] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X126,tyop_2Emin_2Ebool),X127))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X126,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(X126,tyop_2Emin_2Ebool),X127))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a]) ).
fof(i_0_45,plain,
! [X133] :
( ( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X133))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
| s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X133) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) )
& ( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X133) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
| s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X133))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Ecomplex_2ECOMPLEX__INV__EQ__0])]) ).
fof(i_0_46,plain,
! [X131] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,X131))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__of__num_2E0),s(tyop_2Enum_2Enum,X131))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ecomplex_2Ecomplex__of__num_2E1]) ).
fof(i_0_47,plain,
! [X99,X100] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X99),s(tyop_2Emin_2Ebool,X100))))
| ~ p(s(tyop_2Emin_2Ebool,X99))
| p(s(tyop_2Emin_2Ebool,X100)) )
& ( p(s(tyop_2Emin_2Ebool,X99))
| p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X99),s(tyop_2Emin_2Ebool,X100)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X100))
| p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X99),s(tyop_2Emin_2Ebool,X100)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_3D_3D_3E])])]) ).
fof(i_0_48,plain,
! [X101,X102,X103] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X101,X102),s(X101,X103))))
| s(X101,X102) = s(X101,X103) )
& ( s(X101,X102) != s(X101,X103)
| p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X101,X102),s(X101,X103)))) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_3D])]) ).
fof(i_0_49,plain,
! [X96,X97] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X96),s(tyop_2Emin_2Ebool,X97))))
| p(s(tyop_2Emin_2Ebool,X96))
| p(s(tyop_2Emin_2Ebool,X97)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X96))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X96),s(tyop_2Emin_2Ebool,X97)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X97))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X96),s(tyop_2Emin_2Ebool,X97)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_5C_2F])])]) ).
fof(i_0_50,plain,
! [X94,X95] :
( ( p(s(tyop_2Emin_2Ebool,X94))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X94),s(tyop_2Emin_2Ebool,X95)))) )
& ( p(s(tyop_2Emin_2Ebool,X95))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X94),s(tyop_2Emin_2Ebool,X95)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X94))
| ~ p(s(tyop_2Emin_2Ebool,X95))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X94),s(tyop_2Emin_2Ebool,X95)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_2F_5C])])]) ).
fof(i_0_51,plain,
! [X82,X83] : s(X82,app_2E2(s(tyop_2Emin_2Efun(X82,X82),combin_i_2E0),s(X82,X83))) = s(X82,X83),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Ei__thm]) ).
fof(i_0_52,plain,
! [X98] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X98))))
| ~ p(s(tyop_2Emin_2Ebool,X98)) )
& ( p(s(tyop_2Emin_2Ebool,X98))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X98)))) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_29])]) ).
fof(i_0_53,negated_conjecture,
( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),esk4_0) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
& s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),esk4_0))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_30])])]) ).
fof(i_0_54,plain,
! [X79,X80] :
( ( ~ p(s(tyop_2Emin_2Ebool,X79))
| ~ p(s(tyop_2Emin_2Ebool,X80))
| s(tyop_2Emin_2Ebool,X79) = s(tyop_2Emin_2Ebool,X80) )
& ( p(s(tyop_2Emin_2Ebool,X79))
| p(s(tyop_2Emin_2Ebool,X80))
| s(tyop_2Emin_2Ebool,X79) = s(tyop_2Emin_2Ebool,X80) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Eho_2Eboolext])])]) ).
fof(i_0_55,plain,
! [X132] :
( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X132)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X132))
| p(s(tyop_2Emin_2Ebool,X132)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X132))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X132)) )
& ( p(s(tyop_2Emin_2Ebool,X132))
| 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,X132))
| 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,X132))
| 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,X132)) )
& p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
& ( p(s(tyop_2Emin_2Ebool,X132))
| ~ p(s(tyop_2Emin_2Ebool,X132)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X132)) )
& ( p(s(tyop_2Emin_2Ebool,X132))
| ~ p(s(tyop_2Emin_2Ebool,X132))
| 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_31])])]) ).
fof(i_0_56,plain,
! [X81] :
( s(tyop_2Emin_2Ebool,X81) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| s(tyop_2Emin_2Ebool,X81) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Ebool__cases__ax]) ).
fof(i_0_57,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(fof_simplification,[status(thm)],[reserved_2Eho_2Enotfalse]) ).
cnf(i_0_58,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_32]),
[final] ).
cnf(i_0_59,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_33]),
[final] ).
cnf(i_0_60,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_34]),
[final] ).
cnf(i_0_61,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_35]),
[final] ).
cnf(i_0_62,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_36]),
[final] ).
cnf(i_0_63,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_37]),
[final] ).
cnf(i_0_64,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_37]),
[final] ).
cnf(i_0_65,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_34]),
[final] ).
cnf(i_0_66,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_37]),
[final] ).
cnf(i_0_67,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_35]),
[final] ).
cnf(i_0_68,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_36]),
[final] ).
cnf(i_0_69,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_36]),
[final] ).
cnf(i_0_70,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_35]),
[final] ).
cnf(i_0_71,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_38]),
[final] ).
cnf(i_0_72,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_39]),
[final] ).
cnf(i_0_73,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_40]),
[final] ).
cnf(i_0_74,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_40]),
[final] ).
cnf(i_0_75,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_39]),
[final] ).
cnf(i_0_76,plain,
s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__inv_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_77,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_42]),
[final] ).
cnf(i_0_78,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_43]),
[final] ).
cnf(i_0_79,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_44]),
[final] ).
cnf(i_0_80,plain,
( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
| s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_81,plain,
s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,X1))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__of__num_2E0),s(tyop_2Enum_2Enum,X1))),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_82,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_47]),
[final] ).
cnf(i_0_83,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_48]),
[final] ).
cnf(i_0_84,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_49]),
[final] ).
cnf(i_0_85,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_42]),
[final] ).
cnf(i_0_86,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_50]),
[final] ).
cnf(i_0_87,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_50]),
[final] ).
cnf(i_0_88,plain,
( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0)))
| s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_89,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_50]),
[final] ).
cnf(i_0_90,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_48]),
[final] ).
cnf(i_0_91,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_47]),
[final] ).
cnf(i_0_92,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_49]),
[final] ).
cnf(i_0_93,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_49]),
[final] ).
cnf(i_0_94,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_47]),
[final] ).
cnf(i_0_95,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_51]),
[final] ).
cnf(i_0_96,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_52]),
[final] ).
cnf(i_0_97,negated_conjecture,
s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),esk4_0))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_98,negated_conjecture,
s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),esk4_0) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_99,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_52]),
[final] ).
cnf(i_0_100,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_54]),
[final] ).
cnf(i_0_101,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_55]),
[final] ).
cnf(i_0_102,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_103,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_54]),
[final] ).
cnf(i_0_104,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_105,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_106,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_107,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_55]),
[final] ).
cnf(i_0_108,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_56]),
[final] ).
cnf(i_0_109,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_110,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_111,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(split_conjunct,[status(thm)],[thm_2Ebool_2ETRUTH]),
[final] ).
cnf(i_0_112,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(split_conjunct,[status(thm)],[reserved_2Eho_2Etruth]),
[final] ).
cnf(i_0_113,axiom,
X1 = X1 ).
cnf(i_0_114,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_115,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_116,axiom,
( X1 != X2
| s(X1,X3) = s(X2,X3) ) ).
cnf(i_0_117,axiom,
( X1 != X2
| s(X3,X1) = s(X3,X2) ) ).
cnf(i_0_118,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_113_001,axiom,
X1 = X1 ).
cnf(i_0_114_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_115_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_116_004,axiom,
( X1 != X2
| s(X1,X3) = s(X2,X3) ) ).
cnf(i_0_117_005,axiom,
( X1 != X2
| s(X3,X1) = s(X3,X2) ) ).
cnf(i_0_118_006,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_119,plain,
s(tyop_2Emin_2Efun(X1,X2),X3) = s(tyop_2Emin_2Efun(X1,X2),X3),
inference(equality_inference,[],[59]) ).
cnf(i_0_120,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,[],[65]) ).
cnf(i_0_121,plain,
s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))),
inference(equality_inference,[],[88]) ).
cnf(i_0_122,plain,
p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X1,X2),s(X1,X2)))),
inference(equality_inference,[],[90]) ).
cnf(i_0_123,plain,
$false,
inference(scs_inference,[],[i_0_98,i_0_97,i_0_80]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : ITP019+1 : 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.08/0.25 % Computer : n024.cluster.edu
% 0.08/0.25 % Model : x86_64 x86_64
% 0.08/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.25 % Memory : 8042.1875MB
% 0.08/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.25 % CPULimit : 300
% 0.08/0.25 % WCLimit : 300
% 0.08/0.25 % DateTime : Mon May 4 14:43:26 EDT 2026
% 0.08/0.25 % CPUTime :
% 0.08/0.25 % start to proof: theBenchmark
% 0.15/1.52 % Version : CSE_E---1.7
% 0.15/1.52 % Problem : theBenchmark.p
% 0.15/1.52 % SZS status Theorem for theBenchmark.p
% 0.15/1.52 % SZS output start CNFRefutation
% See solution above
% 0.15/1.53 % Total time : 1.263s
%------------------------------------------------------------------------------