%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ITP023+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 : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:32:44 PM UTC 2026
% Result : Theorem 0.93s 1.63s
% Output : CNFRefutation 0.93s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_39)
% Comments :
%------------------------------------------------------------------------------
fof(thm_2Esat_2Edc__eq,axiom,
! [X26,X27,X28] :
( ( p(s(tyop_2Emin_2Ebool,X28))
<=> s(tyop_2Emin_2Ebool,X27) = s(tyop_2Emin_2Ebool,X26) )
<=> ( ( p(s(tyop_2Emin_2Ebool,X28))
| p(s(tyop_2Emin_2Ebool,X27))
| p(s(tyop_2Emin_2Ebool,X26)) )
& ( p(s(tyop_2Emin_2Ebool,X28))
| ~ p(s(tyop_2Emin_2Ebool,X26))
| ~ p(s(tyop_2Emin_2Ebool,X27)) )
& ( p(s(tyop_2Emin_2Ebool,X27))
| ~ p(s(tyop_2Emin_2Ebool,X26))
| ~ p(s(tyop_2Emin_2Ebool,X28)) )
& ( p(s(tyop_2Emin_2Ebool,X26))
| ~ p(s(tyop_2Emin_2Ebool,X27))
| ~ p(s(tyop_2Emin_2Ebool,X28)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Esat_2Edc__eq) ).
fof(thm_2Ereal__topology_2EBOUNDED__BALL,conjecture,
! [X9,X21] : p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X9),s(tyop_2Erealax_2Ereal,X21)))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal__topology_2EBOUNDED__BALL) ).
fof(thm_2Ebool_2ENOT__FORALL__THM,axiom,
! [X1,X17] :
( ~ ! [X12] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,X12))))
<=> ? [X5] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,X5)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__FORALL__THM) ).
fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom,
! [X13] :
( ~ p(s(tyop_2Emin_2Ebool,X13))
<=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X13)))) ),
file('/export/starexec/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_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(thm_2Ebool_2EIMP__F,axiom,
! [X8] :
( ( p(s(tyop_2Emin_2Ebool,X8))
=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
=> ~ p(s(tyop_2Emin_2Ebool,X8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__F) ).
fof(thm_2Ebool_2EEQ__CLAUSES,axiom,
! [X8] :
( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X8)
<=> p(s(tyop_2Emin_2Ebool,X8)) )
& ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
<=> p(s(tyop_2Emin_2Ebool,X8)) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X8)
<=> ~ p(s(tyop_2Emin_2Ebool,X8)) )
& ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
<=> ~ p(s(tyop_2Emin_2Ebool,X8)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
fof(thm_2Ebool_2ENOT__CLAUSES,axiom,
( ! [X8] :
( ~ ~ p(s(tyop_2Emin_2Ebool,X8))
<=> p(s(tyop_2Emin_2Ebool,X8)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__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(thm_2Ereal__topology_2EBALL__SUBSET__CBALL,axiom,
! [X9,X21] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X9),s(tyop_2Erealax_2Ereal,X21))))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X9),s(tyop_2Erealax_2Ereal,X21)))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal__topology_2EBALL__SUBSET__CBALL) ).
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(thm_2Ereal__topology_2EBOUNDED__CBALL,axiom,
! [X9,X21] : p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X9),s(tyop_2Erealax_2Ereal,X21)))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal__topology_2EBOUNDED__CBALL) ).
fof(arityeq2_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2Etyop_2Erealax_2Ereal,axiom,
! [X13,X14] : s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X13),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X14))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Epred__set_2ESUBSET_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X13))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X14))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2Etyop_2Erealax_2Ereal) ).
fof(arityeq2_2Ec_2Epair_2E_2C_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal,axiom,
! [X13,X14] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X13),s(tyop_2Erealax_2Ereal,X14))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal))),c_2Epair_2E_2C_2E0),s(tyop_2Erealax_2Ereal,X13))),s(tyop_2Erealax_2Ereal,X14))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Epair_2E_2C_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal) ).
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(thm_2Ereal__topology_2EBOUNDED__SUBSET,axiom,
! [X22,X23] :
( ( p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X23))))
& p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X22),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X23)))) )
=> p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X22)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal__topology_2EBOUNDED__SUBSET) ).
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_2Ereal__topology_2Ecball_2E1,axiom,
! [X13] : s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X13))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Ecball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X13))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Ereal__topology_2Ecball_2E1) ).
fof(arityeq1_2Ec_2Ereal__topology_2Eball_2E1,axiom,
! [X13] : s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X13))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Eball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X13))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Ereal__topology_2Eball_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(arityeq1_2Ec_2Ereal__topology_2Ebounded__def_2E1,axiom,
! [X13] : s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X13))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ereal__topology_2Ebounded__def_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X13))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Ereal__topology_2Ebounded__def_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(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
! [X15,X16] :
( ( p(s(tyop_2Emin_2Ebool,X15))
=> p(s(tyop_2Emin_2Ebool,X16)) )
=> ( ( p(s(tyop_2Emin_2Ebool,X16))
=> p(s(tyop_2Emin_2Ebool,X15)) )
=> s(tyop_2Emin_2Ebool,X15) = s(tyop_2Emin_2Ebool,X16) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__ANTISYM__AX) ).
fof(reserved_2Eho_2Eboolext,axiom,
! [X6,X7] :
( ( p(s(tyop_2Emin_2Ebool,X6))
<=> p(s(tyop_2Emin_2Ebool,X7)) )
=> s(tyop_2Emin_2Ebool,X6) = s(tyop_2Emin_2Ebool,X7) ),
file('/export/starexec/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_39,plain,
! [X26,X27,X28] :
( epred1_3(X28,X27,X26)
<=> ( ( p(s(tyop_2Emin_2Ebool,X28))
| p(s(tyop_2Emin_2Ebool,X27))
| p(s(tyop_2Emin_2Ebool,X26)) )
& ( p(s(tyop_2Emin_2Ebool,X28))
| ~ p(s(tyop_2Emin_2Ebool,X26))
| ~ p(s(tyop_2Emin_2Ebool,X27)) )
& ( p(s(tyop_2Emin_2Ebool,X27))
| ~ p(s(tyop_2Emin_2Ebool,X26))
| ~ p(s(tyop_2Emin_2Ebool,X28)) ) ) ),
introduced(definition) ).
fof(i_0_40,plain,
! [X26,X27,X28] :
( ( p(s(tyop_2Emin_2Ebool,X28))
<=> s(tyop_2Emin_2Ebool,X27) = s(tyop_2Emin_2Ebool,X26) )
<=> ( epred1_3(X28,X27,X26)
& ( p(s(tyop_2Emin_2Ebool,X26))
| ~ p(s(tyop_2Emin_2Ebool,X27))
| ~ p(s(tyop_2Emin_2Ebool,X28)) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[thm_2Esat_2Edc__eq]),c_0_39]) ).
fof(i_0_41,negated_conjecture,
~ ! [X9,X21] : p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X9),s(tyop_2Erealax_2Ereal,X21)))))))),
inference(assume_negation,[status(cth)],[thm_2Ereal__topology_2EBOUNDED__BALL]) ).
fof(i_0_42,plain,
! [X1,X17] :
( ~ ! [X12] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,X12))))
<=> ? [X5] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X17),s(X1,X5)))) ),
inference(fof_simplification,[status(thm)],[thm_2Ebool_2ENOT__FORALL__THM]) ).
fof(i_0_43,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_44,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_45,plain,
! [X234,X235,X236] :
( ( epred1_3(X236,X235,X234)
| ~ p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) != s(tyop_2Emin_2Ebool,X234) )
& ( p(s(tyop_2Emin_2Ebool,X234))
| ~ p(s(tyop_2Emin_2Ebool,X235))
| ~ p(s(tyop_2Emin_2Ebool,X236))
| ~ p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) != s(tyop_2Emin_2Ebool,X234) )
& ( epred1_3(X236,X235,X234)
| p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) = s(tyop_2Emin_2Ebool,X234) )
& ( p(s(tyop_2Emin_2Ebool,X234))
| ~ p(s(tyop_2Emin_2Ebool,X235))
| ~ p(s(tyop_2Emin_2Ebool,X236))
| p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) = s(tyop_2Emin_2Ebool,X234) )
& ( ~ p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) = s(tyop_2Emin_2Ebool,X234)
| ~ p(s(tyop_2Emin_2Ebool,X234))
| ~ epred1_3(X236,X235,X234) )
& ( s(tyop_2Emin_2Ebool,X235) != s(tyop_2Emin_2Ebool,X234)
| p(s(tyop_2Emin_2Ebool,X236))
| ~ p(s(tyop_2Emin_2Ebool,X234))
| ~ epred1_3(X236,X235,X234) )
& ( ~ p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) = s(tyop_2Emin_2Ebool,X234)
| p(s(tyop_2Emin_2Ebool,X235))
| ~ epred1_3(X236,X235,X234) )
& ( s(tyop_2Emin_2Ebool,X235) != s(tyop_2Emin_2Ebool,X234)
| p(s(tyop_2Emin_2Ebool,X236))
| p(s(tyop_2Emin_2Ebool,X235))
| ~ epred1_3(X236,X235,X234) )
& ( ~ p(s(tyop_2Emin_2Ebool,X236))
| s(tyop_2Emin_2Ebool,X235) = s(tyop_2Emin_2Ebool,X234)
| p(s(tyop_2Emin_2Ebool,X236))
| ~ epred1_3(X236,X235,X234) )
& ( s(tyop_2Emin_2Ebool,X235) != s(tyop_2Emin_2Ebool,X234)
| p(s(tyop_2Emin_2Ebool,X236))
| p(s(tyop_2Emin_2Ebool,X236))
| ~ epred1_3(X236,X235,X234) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_40])])]) ).
fof(i_0_46,plain,
! [X250,X251,X252] :
( ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| ~ epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X251))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X252))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X250))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( ~ p(s(tyop_2Emin_2Ebool,X251))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X250))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) )
& ( p(s(tyop_2Emin_2Ebool,X252))
| p(s(tyop_2Emin_2Ebool,X251))
| ~ p(s(tyop_2Emin_2Ebool,X250))
| epred1_3(X252,X251,X250) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_39])])]) ).
fof(i_0_47,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_48,plain,
! [X8] :
( ( p(s(tyop_2Emin_2Ebool,X8))
=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
=> ~ p(s(tyop_2Emin_2Ebool,X8)) ),
inference(fof_simplification,[status(thm)],[thm_2Ebool_2EIMP__F]) ).
fof(i_0_49,plain,
! [X8] :
( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X8)
<=> p(s(tyop_2Emin_2Ebool,X8)) )
& ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
<=> p(s(tyop_2Emin_2Ebool,X8)) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X8)
<=> ~ p(s(tyop_2Emin_2Ebool,X8)) )
& ( s(tyop_2Emin_2Ebool,X8) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
<=> ~ p(s(tyop_2Emin_2Ebool,X8)) ) ),
inference(fof_simplification,[status(thm)],[thm_2Ebool_2EEQ__CLAUSES]) ).
fof(i_0_50,plain,
( ! [X8] : $true
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ),
inference(fof_simplification,[status(thm)],[thm_2Ebool_2ENOT__CLAUSES]) ).
fof(i_0_51,plain,
! [X152,X153,X154,X155,X156,X157] : s(X154,app_2E2(s(tyop_2Emin_2Efun(X152,X154),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X152,X153),tyop_2Emin_2Efun(X152,X154)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X152,tyop_2Emin_2Efun(X153,X154)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(X152,X153),tyop_2Emin_2Efun(X152,X154))),combin_s_2E0),s(tyop_2Emin_2Efun(X152,tyop_2Emin_2Efun(X153,X154)),X155))),s(tyop_2Emin_2Efun(X152,X153),X156))),s(X152,X157))) = s(X154,app_2E2(s(tyop_2Emin_2Efun(X153,X154),app_2E2(s(tyop_2Emin_2Efun(X152,tyop_2Emin_2Efun(X153,X154)),X155),s(X152,X157))),s(X153,app_2E2(s(tyop_2Emin_2Efun(X152,X153),X156),s(X152,X157))))),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Es__thm]) ).
fof(i_0_52,plain,
! [X222,X223] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X222),s(tyop_2Erealax_2Ereal,X223))))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X222),s(tyop_2Erealax_2Ereal,X223)))))))),
inference(variable_rename,[status(thm)],[thm_2Ereal__topology_2EBALL__SUBSET__CBALL]) ).
fof(i_0_53,negated_conjecture,
~ p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,esk6_0),s(tyop_2Erealax_2Ereal,esk7_0)))))))),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_41])])]) ).
fof(i_0_54,plain,
! [X138,X139,X140,X141] :
( s(X139,app_2E2(s(tyop_2Emin_2Efun(X138,X139),X140),s(X138,esk1_4(X138,X139,X140,X141)))) != s(X139,app_2E2(s(tyop_2Emin_2Efun(X138,X139),X141),s(X138,esk1_4(X138,X139,X140,X141))))
| s(tyop_2Emin_2Efun(X138,X139),X140) = s(tyop_2Emin_2Efun(X138,X139),X141) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Eho_2Eeq__ext])])]) ).
fof(i_0_55,plain,
! [X187,X188,X189] :
( ( s(X187,X188) != s(X187,X189)
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X187,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X187,tyop_2Emin_2Efun(X187,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X187,X188))),s(X187,X189)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X187,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X187,tyop_2Emin_2Efun(X187,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(X187,X188))),s(X187,X189))))
| s(X187,X188) = s(X187,X189) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a])]) ).
fof(i_0_56,plain,
! [X185,X186] :
( ( p(s(tyop_2Emin_2Ebool,X185))
| 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,X185))),s(tyop_2Emin_2Ebool,X186)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X186))
| 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,X185))),s(tyop_2Emin_2Ebool,X186)))) )
& ( ~ 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,X185))),s(tyop_2Emin_2Ebool,X186))))
| ~ p(s(tyop_2Emin_2Ebool,X185))
| p(s(tyop_2Emin_2Ebool,X186)) ) ),
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_57,plain,
! [X182,X183] :
( ( ~ p(s(tyop_2Emin_2Ebool,X182))
| 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,X182))),s(tyop_2Emin_2Ebool,X183)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X183))
| 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,X182))),s(tyop_2Emin_2Ebool,X183)))) )
& ( ~ 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,X182))),s(tyop_2Emin_2Ebool,X183))))
| p(s(tyop_2Emin_2Ebool,X182))
| p(s(tyop_2Emin_2Ebool,X183)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Ebool_2E_5C_2F_2E2])])]) ).
fof(i_0_58,plain,
! [X180,X181] :
( ( ~ p(s(tyop_2Emin_2Ebool,X180))
| ~ p(s(tyop_2Emin_2Ebool,X181))
| 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,X180))),s(tyop_2Emin_2Ebool,X181)))) )
& ( p(s(tyop_2Emin_2Ebool,X180))
| ~ 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,X180))),s(tyop_2Emin_2Ebool,X181)))) )
& ( p(s(tyop_2Emin_2Ebool,X181))
| ~ 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,X180))),s(tyop_2Emin_2Ebool,X181)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arityeq2_2Ec_2Ebool_2E_2F_5C_2E2])])]) ).
fof(i_0_59,plain,
! [X226,X227] : p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X226),s(tyop_2Erealax_2Ereal,X227)))))))),
inference(variable_rename,[status(thm)],[thm_2Ereal__topology_2EBOUNDED__CBALL]) ).
fof(i_0_60,plain,
! [X199,X200] : s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X199),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X200))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Epred__set_2ESUBSET_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X199))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X200))),
inference(variable_rename,[status(thm)],[arityeq2_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2Etyop_2Erealax_2Ereal]) ).
fof(i_0_61,plain,
! [X195,X196] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X195),s(tyop_2Erealax_2Ereal,X196))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal))),c_2Epair_2E_2C_2E0),s(tyop_2Erealax_2Ereal,X195))),s(tyop_2Erealax_2Ereal,X196))),
inference(variable_rename,[status(thm)],[arityeq2_2Ec_2Epair_2E_2C_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal]) ).
fof(i_0_62,plain,
! [X148,X149,X150,X151] : s(X148,app_2E2(s(tyop_2Emin_2Efun(X149,X148),app_2E2(s(tyop_2Emin_2Efun(X148,tyop_2Emin_2Efun(X149,X148)),combin_k_2E0),s(X148,X150))),s(X149,X151))) = s(X148,X150),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Ek__thm]) ).
fof(i_0_63,plain,
! [X224,X225] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X225))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X224),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X225))))
| p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X224)))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Ereal__topology_2EBOUNDED__SUBSET])]) ).
fof(i_0_64,plain,
! [X210,X211,X212,X214,X215,X216] :
( ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X210,tyop_2Emin_2Ebool),X211),s(X210,X212))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X210,tyop_2Emin_2Ebool),X211),s(X210,esk4_2(X210,X211))))) )
& ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X214,tyop_2Emin_2Ebool),X215),s(X214,X216))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X214,tyop_2Emin_2Ebool),X215),s(X214,esk5_2(X214,X215))))) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_42])])])])]) ).
fof(i_0_65,plain,
! [X168,X169,X170,X171,X172] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X168,tyop_2Emin_2Ebool),X169))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X168,tyop_2Emin_2Ebool),X169),s(X168,X170)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X171,tyop_2Emin_2Ebool),X172),s(X171,esk2_2(X171,X172)))))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X171,tyop_2Emin_2Ebool),X172)))) ) ),
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_66,plain,
! [X174,X175,X177,X178,X179] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X174,tyop_2Emin_2Ebool),X175))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X174,tyop_2Emin_2Ebool),X175),s(X174,esk3_2(X174,X175))))) )
& ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X177,tyop_2Emin_2Ebool),X178),s(X177,X179))))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X177,tyop_2Emin_2Ebool),X178)))) ) ),
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_67,plain,
! [X198] : s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X198))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Ecball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X198))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ereal__topology_2Ecball_2E1]) ).
fof(i_0_68,plain,
! [X197] : s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X197))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Eball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X197))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ereal__topology_2Eball_2E1]) ).
fof(i_0_69,plain,
! [X184] :
( ( p(s(tyop_2Emin_2Ebool,X184))
| 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,X184)))) )
& ( ~ 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,X184))))
| ~ p(s(tyop_2Emin_2Ebool,X184)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_43])]) ).
fof(i_0_70,plain,
! [X192,X193] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(X192,tyop_2Emin_2Ebool),X193))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X192,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(X192,tyop_2Emin_2Ebool),X193))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a]) ).
fof(i_0_71,plain,
! [X190,X191] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(X190,tyop_2Emin_2Ebool),X191))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X190,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(X190,tyop_2Emin_2Ebool),X191))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a]) ).
fof(i_0_72,plain,
! [X194] : s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X194))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ereal__topology_2Ebounded__def_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X194))),
inference(variable_rename,[status(thm)],[arityeq1_2Ec_2Ereal__topology_2Ebounded__def_2E1]) ).
fof(i_0_73,plain,
! [X163,X164] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X163),s(tyop_2Emin_2Ebool,X164))))
| ~ p(s(tyop_2Emin_2Ebool,X163))
| p(s(tyop_2Emin_2Ebool,X164)) )
& ( p(s(tyop_2Emin_2Ebool,X163))
| p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X163),s(tyop_2Emin_2Ebool,X164)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X164))
| p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,X163),s(tyop_2Emin_2Ebool,X164)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_3D_3D_3E])])]) ).
fof(i_0_74,plain,
! [X165,X166,X167] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X165,X166),s(X165,X167))))
| s(X165,X166) = s(X165,X167) )
& ( s(X165,X166) != s(X165,X167)
| p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X165,X166),s(X165,X167)))) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_3D])]) ).
fof(i_0_75,plain,
! [X160,X161] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X160),s(tyop_2Emin_2Ebool,X161))))
| p(s(tyop_2Emin_2Ebool,X160))
| p(s(tyop_2Emin_2Ebool,X161)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X160))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X160),s(tyop_2Emin_2Ebool,X161)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X161))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,X160),s(tyop_2Emin_2Ebool,X161)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_5C_2F])])]) ).
fof(i_0_76,plain,
! [X158,X159] :
( ( p(s(tyop_2Emin_2Ebool,X158))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X158),s(tyop_2Emin_2Ebool,X159)))) )
& ( p(s(tyop_2Emin_2Ebool,X159))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X158),s(tyop_2Emin_2Ebool,X159)))) )
& ( ~ p(s(tyop_2Emin_2Ebool,X158))
| ~ p(s(tyop_2Emin_2Ebool,X159))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,X158),s(tyop_2Emin_2Ebool,X159)))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Elogic_2E_2F_5C])])]) ).
fof(i_0_77,plain,
! [X146,X147] : s(X146,app_2E2(s(tyop_2Emin_2Efun(X146,X146),combin_i_2E0),s(X146,X147))) = s(X146,X147),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Ei__thm]) ).
fof(i_0_78,plain,
! [X162] :
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X162))))
| ~ p(s(tyop_2Emin_2Ebool,X162)) )
& ( p(s(tyop_2Emin_2Ebool,X162))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,X162)))) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_44])]) ).
cnf(i_0_79,plain,
( p(s(tyop_2Emin_2Ebool,X3))
| p(s(tyop_2Emin_2Ebool,X3))
| s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
| ~ epred1_3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_80,plain,
( epred1_3(X2,X1,X3)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
cnf(i_0_81,plain,
( epred1_3(X2,X1,X3)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
cnf(i_0_82,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| epred1_3(X2,X3,X1)
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
cnf(i_0_83,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X1))
| epred1_3(X2,X3,X1)
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
cnf(i_0_84,plain,
( p(s(tyop_2Emin_2Ebool,X2))
| epred1_3(X3,X1,X2)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
cnf(i_0_85,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X1))
| epred1_3(X3,X2,X1)
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
fof(i_0_86,plain,
! [X201,X202] :
( ( p(s(tyop_2Emin_2Ebool,X202))
| s(tyop_2Emin_2Ebool,X201) = s(tyop_2Emin_2Ebool,X202)
| p(s(tyop_2Emin_2Ebool,X201)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X201))
| s(tyop_2Emin_2Ebool,X201) = s(tyop_2Emin_2Ebool,X202)
| p(s(tyop_2Emin_2Ebool,X201)) )
& ( p(s(tyop_2Emin_2Ebool,X202))
| s(tyop_2Emin_2Ebool,X201) = s(tyop_2Emin_2Ebool,X202)
| ~ p(s(tyop_2Emin_2Ebool,X202)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X201))
| s(tyop_2Emin_2Ebool,X201) = s(tyop_2Emin_2Ebool,X202)
| ~ p(s(tyop_2Emin_2Ebool,X202)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Ebool_2EIMP__ANTISYM__AX])])]) ).
fof(i_0_87,plain,
! [X143,X144] :
( ( ~ p(s(tyop_2Emin_2Ebool,X143))
| ~ p(s(tyop_2Emin_2Ebool,X144))
| s(tyop_2Emin_2Ebool,X143) = s(tyop_2Emin_2Ebool,X144) )
& ( p(s(tyop_2Emin_2Ebool,X143))
| p(s(tyop_2Emin_2Ebool,X144))
| s(tyop_2Emin_2Ebool,X143) = s(tyop_2Emin_2Ebool,X144) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reserved_2Eho_2Eboolext])])]) ).
fof(i_0_88,plain,
! [X205] :
( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X205)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X205))
| p(s(tyop_2Emin_2Ebool,X205)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X205))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X205)) )
& ( p(s(tyop_2Emin_2Ebool,X205))
| 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,X205))
| 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,X205))
| 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,X205)) )
& p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
& ( p(s(tyop_2Emin_2Ebool,X205))
| ~ p(s(tyop_2Emin_2Ebool,X205)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X205)) )
& ( p(s(tyop_2Emin_2Ebool,X205))
| ~ p(s(tyop_2Emin_2Ebool,X205))
| 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_47])])]) ).
fof(i_0_89,plain,
! [X203] :
( ( p(s(tyop_2Emin_2Ebool,X203))
| ~ p(s(tyop_2Emin_2Ebool,X203)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X203)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])])]) ).
fof(i_0_90,plain,
! [X209] :
( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,X209)
| p(s(tyop_2Emin_2Ebool,X209)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X209))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X209) )
& ( s(tyop_2Emin_2Ebool,X209) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| p(s(tyop_2Emin_2Ebool,X209)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X209))
| s(tyop_2Emin_2Ebool,X209) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,X209)
| ~ p(s(tyop_2Emin_2Ebool,X209)) )
& ( p(s(tyop_2Emin_2Ebool,X209))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X209) )
& ( s(tyop_2Emin_2Ebool,X209) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| ~ p(s(tyop_2Emin_2Ebool,X209)) )
& ( p(s(tyop_2Emin_2Ebool,X209))
| s(tyop_2Emin_2Ebool,X209) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_49])]) ).
fof(i_0_91,plain,
( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[i_0_50])]) ).
fof(i_0_92,plain,
! [X145] :
( s(tyop_2Emin_2Ebool,X145) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| s(tyop_2Emin_2Ebool,X145) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(variable_rename,[status(thm)],[reserved_2Eho_2Ebool__cases__ax]) ).
fof(i_0_93,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(fof_simplification,[status(thm)],[reserved_2Eho_2Enotfalse]) ).
cnf(i_0_94,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_51]),
[final] ).
cnf(i_0_95,plain,
p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X1),s(tyop_2Erealax_2Ereal,X2))))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X1),s(tyop_2Erealax_2Ereal,X2)))))))),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_96,negated_conjecture,
~ p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,esk6_0),s(tyop_2Erealax_2Ereal,esk7_0)))))))),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_97,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_54]),
[final] ).
cnf(i_0_98,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_55]),
[final] ).
cnf(i_0_99,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_56]),
[final] ).
cnf(i_0_100,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_57]),
[final] ).
cnf(i_0_101,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_58]),
[final] ).
cnf(i_0_102,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_58]),
[final] ).
cnf(i_0_103,plain,
p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X1),s(tyop_2Erealax_2Ereal,X2)))))))),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_104,plain,
s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X2))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Epred__set_2ESUBSET_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X2))),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_105,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_55]),
[final] ).
cnf(i_0_106,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_58]),
[final] ).
cnf(i_0_107,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_56]),
[final] ).
cnf(i_0_108,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_57]),
[final] ).
cnf(i_0_109,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_57]),
[final] ).
cnf(i_0_110,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_56]),
[final] ).
cnf(i_0_111,plain,
s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X1),s(tyop_2Erealax_2Ereal,X2))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal))),c_2Epair_2E_2C_2E0),s(tyop_2Erealax_2Ereal,X1))),s(tyop_2Erealax_2Ereal,X2))),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_112,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_62]),
[final] ).
cnf(i_0_113,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1)))) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_114,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk5_2(X1,X2))))) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_115,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,X3))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(X1,esk4_2(X1,X2))))) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_116,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_65]),
[final] ).
cnf(i_0_117,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_66]),
[final] ).
cnf(i_0_118,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_66]),
[final] ).
cnf(i_0_119,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_65]),
[final] ).
cnf(i_0_120,plain,
s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Ecball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_121,plain,
s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Eball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X1))),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_122,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_69]),
[final] ).
cnf(i_0_123,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_70]),
[final] ).
cnf(i_0_124,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_71]),
[final] ).
cnf(i_0_125,plain,
s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ereal__topology_2Ebounded__def_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1))),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_126,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_73]),
[final] ).
cnf(i_0_127,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_74]),
[final] ).
cnf(i_0_128,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_75]),
[final] ).
cnf(i_0_129,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_69]),
[final] ).
cnf(i_0_130,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_76]),
[final] ).
cnf(i_0_131,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_76]),
[final] ).
cnf(i_0_132,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_76]),
[final] ).
cnf(i_0_133,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_74]),
[final] ).
cnf(i_0_134,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_73]),
[final] ).
cnf(i_0_135,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_75]),
[final] ).
cnf(i_0_136,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_75]),
[final] ).
cnf(i_0_137,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_73]),
[final] ).
cnf(i_0_138,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_77]),
[final] ).
cnf(i_0_139,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_78]),
[final] ).
cnf(i_0_140,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X3))
| ~ epred1_3(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_141,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X3))
| ~ epred1_3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_142,plain,
( s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X3)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X3))
| ~ epred1_3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_143,plain,
( p(s(tyop_2Emin_2Ebool,X3))
| s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ epred1_3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_144,plain,
( epred1_3(X2,X1,X3)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_145,plain,
( s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X3)
| p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ epred1_3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_146,plain,
( p(s(tyop_2Emin_2Ebool,X3))
| p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
| ~ epred1_3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_147,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| epred1_3(X2,X3,X1)
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_148,plain,
( p(s(tyop_2Emin_2Ebool,X2))
| epred1_3(X3,X1,X2)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_149,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X2))
| p(s(tyop_2Emin_2Ebool,X3))
| ~ epred1_3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_150,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_78]),
[final] ).
cnf(i_0_151,plain,
( p(s(tyop_2Emin_2Ebool,X3))
| s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,X2)
| ~ epred1_3(X3,X1,X2) ),
inference(cn,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_152,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X2))
| epred1_3(X1,X2,X3)
| ~ p(s(tyop_2Emin_2Ebool,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_153,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X2))
| epred1_3(X1,X3,X2)
| ~ p(s(tyop_2Emin_2Ebool,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_154,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X2))
| epred1_3(X3,X2,X1)
| ~ p(s(tyop_2Emin_2Ebool,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_155,plain,
( epred1_3(X2,X1,X3)
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(cn,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_156,plain,
( epred1_3(X2,X1,X3)
| ~ p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(cn,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_157,plain,
( epred1_3(X1,X2,X3)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X2) != s(tyop_2Emin_2Ebool,X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_158,plain,
( epred1_3(X2,X3,X1)
| p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(cn,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_159,plain,
( epred1_3(X2,X3,X1)
| p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(cn,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_160,plain,
( epred1_3(X3,X1,X2)
| p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(cn,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_161,plain,
( epred1_3(X3,X2,X1)
| p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ),
inference(cn,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_162,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_86]),
[final] ).
cnf(i_0_163,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_87]),
[final] ).
cnf(i_0_164,plain,
( epred1_3(X1,X2,X3)
| p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_165,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_88]),
[final] ).
cnf(i_0_166,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_167,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_168,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,X1)
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_169,plain,
( s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_170,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X1)
| p(s(tyop_2Emin_2Ebool,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_171,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_87]),
[final] ).
cnf(i_0_172,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_91]),
[final] ).
cnf(i_0_173,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_174,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_175,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X1)
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_176,plain,
( s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_177,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,X1) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_178,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X1) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_179,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_180,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_181,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X1) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_182,plain,
( p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_183,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_184,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_91]),
[final] ).
cnf(i_0_185,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_88]),
[final] ).
cnf(i_0_186,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_92]),
[final] ).
cnf(i_0_187,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(split_conjunct,[status(thm)],[i_0_93]),
[final] ).
cnf(i_0_188,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_189,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(split_conjunct,[status(thm)],[thm_2Ebool_2ETRUTH]),
[final] ).
cnf(i_0_190,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(split_conjunct,[status(thm)],[reserved_2Eho_2Etruth]),
[final] ).
cnf(i_0_191,axiom,
X1 = X1 ).
cnf(i_0_192,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_193,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_194,axiom,
( X1 != X2
| s(X1,X3) = s(X2,X3) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| s(X3,X1) = s(X3,X2) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| ~ epred1_3(X1,X3,X4)
| epred1_3(X2,X3,X4) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| ~ epred1_3(X3,X1,X4)
| epred1_3(X3,X2,X4) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ epred1_3(X3,X4,X1)
| epred1_3(X3,X4,X2) ) ).
cnf(i_0_191_001,axiom,
X1 = X1 ).
cnf(i_0_192_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_193_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_194_004,axiom,
( X1 != X2
| s(X1,X3) = s(X2,X3) ) ).
cnf(i_0_195_005,axiom,
( X1 != X2
| s(X3,X1) = s(X3,X2) ) ).
cnf(i_0_196_006,axiom,
( X1 != X2
| ~ p(X1)
| p(X2) ) ).
cnf(i_0_197_007,axiom,
( X1 != X2
| ~ epred1_3(X1,X3,X4)
| epred1_3(X2,X3,X4) ) ).
cnf(i_0_198_008,axiom,
( X1 != X2
| ~ epred1_3(X3,X1,X4)
| epred1_3(X3,X2,X4) ) ).
cnf(i_0_199_009,axiom,
( X1 != X2
| ~ epred1_3(X3,X4,X1)
| epred1_3(X3,X4,X2) ) ).
cnf(i_0_200,plain,
s(tyop_2Emin_2Efun(X1,X2),X3) = s(tyop_2Emin_2Efun(X1,X2),X3),
inference(equality_inference,[],[97]) ).
cnf(i_0_201,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,[],[105]) ).
cnf(i_0_202,plain,
p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(X1,X2),s(X1,X2)))),
inference(equality_inference,[],[133]) ).
cnf(i_0_203,plain,
( ~ epred1_3(X1,X2,X2)
| p(s(tyop_2Emin_2Ebool,X1)) ),
inference(equality_inference,[],[151]) ).
cnf(i_0_204,plain,
( epred1_3(X1,X2,X2)
| ~ p(s(tyop_2Emin_2Ebool,X1)) ),
inference(equality_inference,[],[157]) ).
cnf(i_0_205,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(equality_inference,[],[168]) ).
cnf(i_0_206,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(equality_inference,[],[169]) ).
cnf(i_0_207,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(equality_inference,[],[177]) ).
cnf(i_0_208,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(equality_inference,[],[178]) ).
cnf(i_0_209,plain,
$false,
inference(scs_inference,[],[i_0_96,i_0_103,i_0_95,i_0_113]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : ITP023+1 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.11/0.13 % 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.15/0.34 % Computer : n029.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 19:46:29 EDT 2026
% 0.15/0.35 % CPUTime :
% 0.15/0.36 % start to proof: theBenchmark
% 0.93/1.63 % Version : CSE_E---1.7
% 0.93/1.63 % Problem : theBenchmark.p
% 0.93/1.63 % SZS status Theorem for theBenchmark.p
% 0.93/1.63 % SZS output start CNFRefutation
% See solution above
% 0.93/1.66 % Total time : 1.274s
%------------------------------------------------------------------------------