%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP023+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:48:00 PM UTC 2026
% Result : Theorem 2.69s 1.17s
% Output : CNFRefutation 2.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 76 ( 32 unt; 5 def)
% Number of atoms : 211 ( 5 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 162 ( 75 ~; 67 |; 5 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 68 ( 0 sgn 66 !; 2 ?; 24 :)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(f13,axiom,
ne(ty_2Erealax_2Ereal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Erealax_2Ereal) ).
fof(f15,axiom,
mem(c_2Ereal__topology_2Eball,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ereal__topology_2Eball) ).
fof(f17,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> mem(c_2Epair_2E_2C(X0,X1),arr(X0,arr(X1,ty_2Epair_2Eprod(X0,X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Epair_2E_2C) ).
fof(f18,axiom,
mem(c_2Ereal__topology_2Ecball,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ereal__topology_2Ecball) ).
fof(f46,axiom,
! [X0] :
( mem(X0,ty_2Erealax_2Ereal)
=> ! [X1] :
( mem(X1,ty_2Erealax_2Ereal)
=> p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1))),ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ereal__topology_2EBALL__SUBSET__CBALL) ).
fof(f47,axiom,
! [X0] :
( mem(X0,arr(ty_2Erealax_2Ereal,bool))
=> ! [X1] :
( mem(X1,arr(ty_2Erealax_2Ereal,bool))
=> ( ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),X0),X1))
& p(ap(c_2Ereal__topology_2Ebounded__def,X1)) )
=> p(ap(c_2Ereal__topology_2Ebounded__def,X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ereal__topology_2EBOUNDED__SUBSET) ).
fof(f48,axiom,
! [X0] :
( mem(X0,ty_2Erealax_2Ereal)
=> ! [X1] :
( mem(X1,ty_2Erealax_2Ereal)
=> p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ereal__topology_2EBOUNDED__CBALL) ).
fof(f59,conjecture,
! [X0] :
( mem(X0,ty_2Erealax_2Ereal)
=> ! [X1] :
( mem(X1,ty_2Erealax_2Ereal)
=> p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ereal__topology_2EBOUNDED__BALL) ).
fof(f60,negated_conjecture,
~ ! [X0] :
( mem(X0,ty_2Erealax_2Ereal)
=> ! [X1] :
( mem(X1,ty_2Erealax_2Ereal)
=> p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ mem(X2,arr(X0,X1))
| ! [X3] :
( ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f90,plain,
! [X0] :
( ~ ne(X0)
| ! [X1] :
( ~ ne(X1)
| mem(c_2Epair_2E_2C(X0,X1),arr(X0,arr(X1,ty_2Epair_2Eprod(X0,X1)))) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f113,plain,
! [X0] :
( ~ mem(X0,ty_2Erealax_2Ereal)
| ! [X1] :
( ~ mem(X1,ty_2Erealax_2Ereal)
| p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1))),ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
inference(ennf_transformation,[],[f46]) ).
fof(f114,plain,
! [X0] :
( ~ mem(X0,arr(ty_2Erealax_2Ereal,bool))
| ! [X1] :
( ~ mem(X1,arr(ty_2Erealax_2Ereal,bool))
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),X0),X1))
| ~ p(ap(c_2Ereal__topology_2Ebounded__def,X1))
| p(ap(c_2Ereal__topology_2Ebounded__def,X0)) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f115,plain,
! [X0] :
( ~ mem(X0,arr(ty_2Erealax_2Ereal,bool))
| ! [X1] :
( ~ mem(X1,arr(ty_2Erealax_2Ereal,bool))
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),X0),X1))
| ~ p(ap(c_2Ereal__topology_2Ebounded__def,X1))
| p(ap(c_2Ereal__topology_2Ebounded__def,X0)) ) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ~ mem(X0,ty_2Erealax_2Ereal)
| ! [X1] :
( ~ mem(X1,ty_2Erealax_2Ereal)
| p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f129,plain,
? [X0] :
( mem(X0,ty_2Erealax_2Ereal)
& ? [X1] :
( mem(X1,ty_2Erealax_2Ereal)
& ~ p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ) ),
inference(ennf_transformation,[],[f60]) ).
fof(f228,plain,
( mem(sK21,ty_2Erealax_2Ereal)
& mem(sK22,ty_2Erealax_2Ereal)
& ~ p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),sK21),sK22)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22]),skolemize(X0,sK21),skolemize(X1,sK22)],[f129]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f245,plain,
ne(ty_2Erealax_2Ereal),
inference(cnf_transformation,[],[f13]) ).
fof(f247,plain,
mem(c_2Ereal__topology_2Eball,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))),
inference(cnf_transformation,[],[f15]) ).
fof(f249,plain,
! [X0,X1] :
( ~ ne(X0)
| ~ ne(X1)
| mem(c_2Epair_2E_2C(X0,X1),arr(X0,arr(X1,ty_2Epair_2Eprod(X0,X1)))) ),
inference(cnf_transformation,[],[f90]) ).
fof(f250,plain,
mem(c_2Ereal__topology_2Ecball,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))),
inference(cnf_transformation,[],[f18]) ).
fof(f325,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Erealax_2Ereal)
| ~ mem(X1,ty_2Erealax_2Ereal)
| p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1))),ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ),
inference(cnf_transformation,[],[f113]) ).
fof(f326,plain,
! [X0,X1] :
( ~ mem(X0,arr(ty_2Erealax_2Ereal,bool))
| ~ mem(X1,arr(ty_2Erealax_2Ereal,bool))
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),X0),X1))
| ~ p(ap(c_2Ereal__topology_2Ebounded__def,X1))
| p(ap(c_2Ereal__topology_2Ebounded__def,X0)) ),
inference(cnf_transformation,[],[f115]) ).
fof(f327,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Erealax_2Ereal)
| ~ mem(X1,ty_2Erealax_2Ereal)
| p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1)))) ),
inference(cnf_transformation,[],[f116]) ).
fof(f433,plain,
mem(sK21,ty_2Erealax_2Ereal),
inference(cnf_transformation,[],[f228]) ).
fof(f434,plain,
mem(sK22,ty_2Erealax_2Ereal),
inference(cnf_transformation,[],[f228]) ).
fof(f435,plain,
~ p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),sK21),sK22)))),
inference(cnf_transformation,[],[f228]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( mem(ap(X0,X3),X2)
| ~ mem(X3,X1)
| ~ mem(X0,arr(X1,X2)) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_65,plain,
ne(ty_2Erealax_2Ereal),
inference(cnf_transformation,[],[f245]) ).
tcf(c_67,plain,
mem(c_2Ereal__topology_2Eball,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))),
inference(cnf_transformation,[],[f247]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] :
( mem(c_2Epair_2E_2C(X0,X1),arr(X0,arr(X1,ty_2Epair_2Eprod(X0,X1))))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_70,plain,
mem(c_2Ereal__topology_2Ecball,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))),
inference(cnf_transformation,[],[f250]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1))),ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1))))
| ~ mem(X1,ty_2Erealax_2Ereal)
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i] :
( p(ap(c_2Ereal__topology_2Ebounded__def,X0))
| ~ p(ap(c_2Ereal__topology_2Ebounded__def,X1))
| ~ mem(X1,arr(ty_2Erealax_2Ereal,bool))
| ~ mem(X0,arr(ty_2Erealax_2Ereal,bool))
| ~ p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),X0),X1)) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] :
( p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0),X1))))
| ~ mem(X1,ty_2Erealax_2Ereal)
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_204,negated_conjecture,
~ p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Eball,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),sK21),sK22)))),
inference(cnf_transformation,[],[f435]) ).
tcf(c_205,negated_conjecture,
mem(sK22,ty_2Erealax_2Ereal),
inference(cnf_transformation,[],[f434]) ).
tcf(c_206,negated_conjecture,
mem(sK21,ty_2Erealax_2Ereal),
inference(cnf_transformation,[],[f433]) ).
tcf(c_3657,definition,
iPr_def_10 = c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_3658,definition,
iPr_def_11 = ap(iPr_def_10,sK21),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_3659,definition,
iPr_def_12 = ap(iPr_def_11,sK22),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_3660,definition,
iPr_def_13 = ap(c_2Ereal__topology_2Eball,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_3661,definition,
iPr_def_14 = ap(c_2Ereal__topology_2Ebounded__def,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_3662,negated_conjecture,
mem(sK21,ty_2Erealax_2Ereal),
inference(demodulation,[status(thm)],[c_206]) ).
tcf(c_3663,negated_conjecture,
mem(sK22,ty_2Erealax_2Ereal),
inference(demodulation,[status(thm)],[c_205]) ).
tcf(c_3664,negated_conjecture,
~ p(iPr_def_14),
inference(demodulation,[status(thm)],[c_204,c_3657,c_3658,c_3659,c_3660,c_3661]) ).
tcf(c_4514,plain,
! [X0: $i] :
( mem(ap(c_2Ereal__topology_2Eball,X0),arr(ty_2Erealax_2Ereal,bool))
| ~ mem(X0,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) ),
inference(superposition,[status(thm)],[c_67,c_52]) ).
tcf(c_4515,plain,
! [X0: $i] :
( mem(ap(c_2Ereal__topology_2Ecball,X0),arr(ty_2Erealax_2Ereal,bool))
| ~ mem(X0,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) ),
inference(superposition,[status(thm)],[c_70,c_52]) ).
tcf(c_4651,plain,
( mem(iPr_def_13,arr(ty_2Erealax_2Ereal,bool))
| ~ mem(iPr_def_12,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) ),
inference(superposition,[status(thm)],[c_3660,c_4514]) ).
tcf(c_4820,plain,
( mem(iPr_def_10,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))))
| ~ ne(ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3657,c_69]) ).
tcf(c_4824,plain,
mem(iPr_def_10,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))),
inference(forward_subsumption_resolution,[status(thm)],[c_4820,c_65]) ).
tcf(c_4852,plain,
! [X0: $i] :
( mem(ap(iPr_def_10,X0),arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_4824,c_52]) ).
tcf(c_4951,plain,
( mem(iPr_def_11,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))
| ~ mem(sK21,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3658,c_4852]) ).
tcf(c_4955,plain,
mem(iPr_def_11,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),
inference(forward_subsumption_resolution,[status(thm)],[c_4951,c_3662]) ).
tcf(c_4966,plain,
! [X0: $i] :
( mem(ap(iPr_def_11,X0),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_4955,c_52]) ).
tcf(c_4977,plain,
( mem(iPr_def_12,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))
| ~ mem(sK22,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3659,c_4966]) ).
tcf(c_4980,plain,
mem(iPr_def_12,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),
inference(forward_subsumption_resolution,[status(thm)],[c_4977,c_3663]) ).
tcf(c_4986,plain,
mem(iPr_def_13,arr(ty_2Erealax_2Ereal,bool)),
inference(backward_subsumption_resolution,[status(thm)],[c_4651,c_4980]) ).
tcf(c_5648,plain,
! [X0: $i,X1: $i] :
( p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(ap(iPr_def_10,X0),X1))))
| ~ mem(X1,ty_2Erealax_2Ereal)
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(light_normalisation,[status(thm)],[c_112,c_3657]) ).
tcf(c_5658,plain,
! [X0: $i] :
( p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(iPr_def_11,X0))))
| ~ mem(sK21,ty_2Erealax_2Ereal)
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3658,c_5648]) ).
tcf(c_5659,plain,
! [X0: $i] :
( p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,ap(iPr_def_11,X0))))
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5658,c_3662]) ).
tcf(c_5813,plain,
( p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,iPr_def_12)))
| ~ mem(sK22,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3659,c_5659]) ).
tcf(c_5814,plain,
p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,iPr_def_12))),
inference(forward_subsumption_resolution,[status(thm)],[c_5813,c_3663]) ).
tcf(c_7714,plain,
! [X0: $i,X1: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(ap(iPr_def_10,X0),X1))),ap(c_2Ereal__topology_2Ecball,ap(ap(iPr_def_10,X0),X1))))
| ~ mem(X1,ty_2Erealax_2Ereal)
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(light_normalisation,[status(thm)],[c_110,c_3657]) ).
tcf(c_7724,plain,
! [X0: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(iPr_def_11,X0))),ap(c_2Ereal__topology_2Ecball,ap(iPr_def_11,X0))))
| ~ mem(sK21,ty_2Erealax_2Ereal)
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3658,c_7714]) ).
tcf(c_7727,plain,
! [X0: $i] :
( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,ap(iPr_def_11,X0))),ap(c_2Ereal__topology_2Ecball,ap(iPr_def_11,X0))))
| ~ mem(X0,ty_2Erealax_2Ereal) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7724,c_3662]) ).
tcf(c_7809,plain,
( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),ap(c_2Ereal__topology_2Eball,iPr_def_12)),ap(c_2Ereal__topology_2Ecball,iPr_def_12)))
| ~ mem(sK22,ty_2Erealax_2Ereal) ),
inference(superposition,[status(thm)],[c_3659,c_7727]) ).
tcf(c_7812,plain,
( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),iPr_def_13),ap(c_2Ereal__topology_2Ecball,iPr_def_12)))
| ~ mem(sK22,ty_2Erealax_2Ereal) ),
inference(light_normalisation,[status(thm)],[c_7809,c_3660]) ).
tcf(c_7813,plain,
p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),iPr_def_13),ap(c_2Ereal__topology_2Ecball,iPr_def_12))),
inference(forward_subsumption_resolution,[status(thm)],[c_7812,c_3663]) ).
tcf(c_7820,plain,
( p(ap(c_2Ereal__topology_2Ebounded__def,iPr_def_13))
| ~ mem(iPr_def_13,arr(ty_2Erealax_2Ereal,bool))
| ~ p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,iPr_def_12)))
| ~ mem(ap(c_2Ereal__topology_2Ecball,iPr_def_12),arr(ty_2Erealax_2Ereal,bool)) ),
inference(superposition,[status(thm)],[c_7813,c_111]) ).
tcf(c_7821,plain,
( p(iPr_def_14)
| ~ mem(iPr_def_13,arr(ty_2Erealax_2Ereal,bool))
| ~ p(ap(c_2Ereal__topology_2Ebounded__def,ap(c_2Ereal__topology_2Ecball,iPr_def_12)))
| ~ mem(ap(c_2Ereal__topology_2Ecball,iPr_def_12),arr(ty_2Erealax_2Ereal,bool)) ),
inference(light_normalisation,[status(thm)],[c_7820,c_3661]) ).
tcf(c_7822,plain,
~ mem(ap(c_2Ereal__topology_2Ecball,iPr_def_12),arr(ty_2Erealax_2Ereal,bool)),
inference(forward_subsumption_resolution,[status(thm)],[c_7821,c_3664,c_4986,c_5814]) ).
tcf(c_7823,plain,
~ mem(iPr_def_12,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),
inference(superposition,[status(thm)],[c_4515,c_7822]) ).
tcf(c_7824,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_7823,c_4980]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP023+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 17:49:33 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 2.69/1.17 % SZS status Started for theBenchmark.p
% 2.69/1.17 % SZS status Theorem for theBenchmark.p
% 2.69/1.17
% 2.69/1.17 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.69/1.17
% 2.69/1.17 % ------ iProver source info
% 2.69/1.17
% 2.69/1.17 % git: date: 2026-07-19 20:42:38 +0200
% 2.69/1.17 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.69/1.17 % git: non_committed_changes: false
% 2.69/1.17
% 2.69/1.17 % ------ Parsing...
% 2.69/1.17 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.69/1.17
% 2.69/1.17 % ------ Preprocessing... sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 2.69/1.17
% 2.69/1.17 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.69/1.17
% 2.69/1.17 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.69/1.17 % ------ Proving...
% 2.69/1.17 % ------ Problem Properties
% 2.69/1.17
% 2.69/1.17 %
% 2.69/1.17 % clauses 62
% 2.69/1.17 % conjectures 3
% 2.69/1.17 % EPR 12
% 2.69/1.17 % Horn 54
% 2.69/1.17 % unary 22
% 2.69/1.17 % binary 6
% 2.69/1.17 % lits 174
% 2.69/1.17 % lits eq 13
% 2.69/1.17 % fd_pure 0
% 2.69/1.17 % fd_pseudo 0
% 2.69/1.17 % fd_cond 0
% 2.69/1.17 % fd_pseudo_cond 5
% 2.69/1.17 % AC symbols 0
% 2.69/1.17
% 2.69/1.17 % ------ Schedule dynamic 5 is on
% 2.69/1.17
% 2.69/1.17 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.69/1.17
% 2.69/1.17
% 2.69/1.17 % ------
% 2.69/1.17 % Current options:
% 2.69/1.17 % ------
% 2.69/1.17
% 2.69/1.17
% 2.69/1.17 %
% 2.69/1.17
% 2.69/1.17 % ------ Proving...
% 2.69/1.17 %
% 2.69/1.17
% 2.69/1.17 % SZS status Theorem for theBenchmark.p
% 2.69/1.17
% 2.69/1.17 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.69/1.17
%------------------------------------------------------------------------------