%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU392+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.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 02:57:19 PM UTC 2026
% Result : Theorem 154.84s 23.08s
% Output : CNFRefutation 154.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of formulae : 223 ( 19 unt; 0 def)
% Number of atoms : 1242 ( 34 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 1724 ( 705 ~; 832 |; 130 &)
% ( 18 <=>; 37 =>; 0 <=; 2 <~>)
% Maximal formula depth : 19 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 495 ( 0 sgn 472 !; 23 ?; 235 :)
% Comments :
%------------------------------------------------------------------------------
fof(f27,axiom,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,powerset(the_carrier(X0)))
=> ( X2 = lim_points_of_net(X0,X1)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X2)
<=> ! [X4] :
( point_neighbourhood(X4,X0,X3)
=> is_eventually_in(X0,X1,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d18_yellow_6) ).
fof(f28,axiom,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,powerset(the_carrier(X0)))
=> ( point_neighbourhood(X2,X0,X1)
<=> in(X1,interior(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_connsp_2) ).
fof(f30,axiom,
! [X0] :
( ( top_str(X0)
& topological_space(X0) )
=> ! [X1,X2] :
( is_a_convergence_point_of_set(X0,X1,X2)
<=> ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( ( in(X2,X3)
& open_subset(X3,X0) )
=> in(X3,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_waybel_7) ).
fof(f32,axiom,
! [X0,X1] :
( ( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1)
& top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_yellow_6) ).
fof(f33,axiom,
! [X0,X1] :
( ( element(X1,powerset(the_carrier(X0)))
& top_str(X0) )
=> element(interior(X0,X1),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_tops_1) ).
fof(f41,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f44,axiom,
! [X0,X1] :
( ( element(X1,the_carrier(X0))
& top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X2] :
( point_neighbourhood(X2,X0,X1)
=> element(X2,powerset(the_carrier(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_connsp_2) ).
fof(f77,axiom,
! [X0,X1] :
( ( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0) )
=> open_subset(interior(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_tops_1) ).
fof(f122,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& ~ empty_carrier(X1) )
=> ! [X2] :
( in(X2,filter_of_net_str(X0,X1))
<=> ( element(X2,powerset(the_carrier(X0)))
& is_eventually_in(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_yellow19) ).
fof(f123,conjecture,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_yellow19) ).
fof(f124,negated_conjecture,
~ ! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f123]) ).
fof(f128,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f129,axiom,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset(interior(X0,X1),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t44_tops_1) ).
fof(f130,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X2))
& in(X0,X1) )
=> element(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f131,axiom,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( ( in(X2,X1)
& open_subset(X1,X0) )
=> point_neighbourhood(X1,X0,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_connsp_2) ).
fof(f136,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& ~ empty_carrier(X1) )
=> ! [X2,X3] :
( subset(X2,X3)
=> ( ( is_often_in(X0,X1,X2)
=> is_often_in(X0,X1,X3) )
& ( is_eventually_in(X0,X1,X2)
=> is_eventually_in(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_waybel_0) ).
fof(f260,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( X2 = lim_points_of_net(X0,X1)
<=> ! [X3] :
( ~ element(X3,the_carrier(X0))
| ( in(X3,X2)
<=> ! [X4] :
( ~ point_neighbourhood(X4,X0,X3)
| is_eventually_in(X0,X1,X4) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f261,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( X2 = lim_points_of_net(X0,X1)
<=> ! [X3] :
( ~ element(X3,the_carrier(X0))
| ( in(X3,X2)
<=> ! [X4] :
( ~ point_neighbourhood(X4,X0,X3)
| is_eventually_in(X0,X1,X4) ) ) ) ) ) ) ),
inference(flattening,[],[f260]) ).
fof(f262,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( point_neighbourhood(X2,X0,X1)
<=> in(X1,interior(X0,X2)) ) ) ) ),
inference(ennf_transformation,[],[f28]) ).
fof(f263,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( point_neighbourhood(X2,X0,X1)
<=> in(X1,interior(X0,X2)) ) ) ) ),
inference(flattening,[],[f262]) ).
fof(f266,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ! [X1,X2] :
( is_a_convergence_point_of_set(X0,X1,X2)
<=> ! [X3] :
( ~ element(X3,powerset(the_carrier(X0)))
| ~ in(X2,X3)
| ~ open_subset(X3,X0)
| in(X3,X1) ) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f267,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ! [X1,X2] :
( is_a_convergence_point_of_set(X0,X1,X2)
<=> ! [X3] :
( ~ element(X3,powerset(the_carrier(X0)))
| ~ in(X2,X3)
| ~ open_subset(X3,X0)
| in(X3,X1) ) ) ),
inference(flattening,[],[f266]) ).
fof(f269,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f32]) ).
fof(f270,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(flattening,[],[f269]) ).
fof(f271,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| element(interior(X0,X1),powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f33]) ).
fof(f272,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| element(interior(X0,X1),powerset(the_carrier(X0))) ),
inference(flattening,[],[f271]) ).
fof(f277,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f279,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X2] :
( ~ point_neighbourhood(X2,X0,X1)
| element(X2,powerset(the_carrier(X0))) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f280,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X2] :
( ~ point_neighbourhood(X2,X0,X1)
| element(X2,powerset(the_carrier(X0))) ) ),
inference(flattening,[],[f279]) ).
fof(f315,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| open_subset(interior(X0,X1),X0) ),
inference(ennf_transformation,[],[f77]) ).
fof(f316,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| open_subset(interior(X0,X1),X0) ),
inference(flattening,[],[f315]) ).
fof(f355,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( in(X2,filter_of_net_str(X0,X1))
<=> ( element(X2,powerset(the_carrier(X0)))
& is_eventually_in(X0,X1,X2) ) ) ) ),
inference(ennf_transformation,[],[f122]) ).
fof(f356,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( in(X2,filter_of_net_str(X0,X1))
<=> ( element(X2,powerset(the_carrier(X0)))
& is_eventually_in(X0,X1,X2) ) ) ) ),
inference(flattening,[],[f355]) ).
fof(f357,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,X1))
<~> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(ennf_transformation,[],[f124]) ).
fof(f358,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,X1))
<~> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(flattening,[],[f357]) ).
fof(f363,plain,
! [X0] :
( ~ top_str(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| subset(interior(X0,X1),X1) ) ),
inference(ennf_transformation,[],[f129]) ).
fof(f364,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(ennf_transformation,[],[f130]) ).
fof(f365,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(flattening,[],[f364]) ).
fof(f366,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ in(X2,X1)
| ~ open_subset(X1,X0)
| point_neighbourhood(X1,X0,X2) ) ) ),
inference(ennf_transformation,[],[f131]) ).
fof(f367,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ in(X2,X1)
| ~ open_subset(X1,X0)
| point_neighbourhood(X1,X0,X2) ) ) ),
inference(flattening,[],[f366]) ).
fof(f372,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2,X3] :
( ~ subset(X2,X3)
| ( ( ~ is_often_in(X0,X1,X2)
| is_often_in(X0,X1,X3) )
& ( ~ is_eventually_in(X0,X1,X2)
| is_eventually_in(X0,X1,X3) ) ) ) ) ),
inference(ennf_transformation,[],[f136]) ).
fof(f373,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2,X3] :
( ~ subset(X2,X3)
| ( ( ~ is_often_in(X0,X1,X2)
| is_often_in(X0,X1,X3) )
& ( ~ is_eventually_in(X0,X1,X2)
| is_eventually_in(X0,X1,X3) ) ) ) ) ),
inference(flattening,[],[f372]) ).
fof(f379,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( ( lim_points_of_net(X0,X1) != X2
| ! [X3] :
( ~ element(X3,the_carrier(X0))
| ( ( ~ in(X3,X2)
| ! [X4] :
( ~ point_neighbourhood(X4,X0,X3)
| is_eventually_in(X0,X1,X4) ) )
& ( ? [X4] :
( point_neighbourhood(X4,X0,X3)
& ~ is_eventually_in(X0,X1,X4) )
| in(X3,X2) ) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& ( in(X3,X2)
| ! [X4] :
( ~ point_neighbourhood(X4,X0,X3)
| is_eventually_in(X0,X1,X4) ) )
& ( ~ in(X3,X2)
| ? [X4] :
( point_neighbourhood(X4,X0,X3)
& ~ is_eventually_in(X0,X1,X4) ) ) )
| X2 = lim_points_of_net(X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f261]) ).
fof(f380,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( ( lim_points_of_net(X0,X1) != X2
| ! [X3] :
( ~ element(X3,the_carrier(X0))
| ( ( ~ in(X3,X2)
| ! [X4] :
( ~ point_neighbourhood(X4,X0,X3)
| is_eventually_in(X0,X1,X4) ) )
& ( ? [X4] :
( point_neighbourhood(X4,X0,X3)
& ~ is_eventually_in(X0,X1,X4) )
| in(X3,X2) ) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& ( in(X3,X2)
| ! [X4] :
( ~ point_neighbourhood(X4,X0,X3)
| is_eventually_in(X0,X1,X4) ) )
& ( ~ in(X3,X2)
| ? [X4] :
( point_neighbourhood(X4,X0,X3)
& ~ is_eventually_in(X0,X1,X4) ) ) )
| X2 = lim_points_of_net(X0,X1) ) ) ) ) ),
inference(flattening,[],[f379]) ).
fof(f381,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( ( lim_points_of_net(X0,X1) != X2
| ! [X6] :
( ~ element(X6,the_carrier(X0))
| ( ( ~ in(X6,X2)
| ! [X8] :
( ~ point_neighbourhood(X8,X0,X6)
| is_eventually_in(X0,X1,X8) ) )
& ( ? [X7] :
( point_neighbourhood(X7,X0,X6)
& ~ is_eventually_in(X0,X1,X7) )
| in(X6,X2) ) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& ( in(X3,X2)
| ! [X5] :
( ~ point_neighbourhood(X5,X0,X3)
| is_eventually_in(X0,X1,X5) ) )
& ( ~ in(X3,X2)
| ? [X4] :
( point_neighbourhood(X4,X0,X3)
& ~ is_eventually_in(X0,X1,X4) ) ) )
| X2 = lim_points_of_net(X0,X1) ) ) ) ) ),
inference(rectify,[],[f380]) ).
fof(f382,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( ( lim_points_of_net(X0,X1) != X2
| ! [X6] :
( ~ element(X6,the_carrier(X0))
| ( ( ~ in(X6,X2)
| ! [X8] :
( ~ point_neighbourhood(X8,X0,X6)
| is_eventually_in(X0,X1,X8) ) )
& ( ( point_neighbourhood(sK4(X0,X1,X6),X0,X6)
& ~ is_eventually_in(X0,X1,sK4(X0,X1,X6)) )
| in(X6,X2) ) ) ) )
& ( ( element(sK2(X0,X1,X2),the_carrier(X0))
& ( in(sK2(X0,X1,X2),X2)
| ! [X5] :
( ~ point_neighbourhood(X5,X0,sK2(X0,X1,X2))
| is_eventually_in(X0,X1,X5) ) )
& ( ~ in(sK2(X0,X1,X2),X2)
| ( point_neighbourhood(sK3(X0,X1,X2),X0,sK2(X0,X1,X2))
& ~ is_eventually_in(X0,X1,sK3(X0,X1,X2)) ) ) )
| X2 = lim_points_of_net(X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2)),skolemize(X7,sK4(X0,X1,X6))],[f381]) ).
fof(f383,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ! [X2] :
( ~ element(X2,powerset(the_carrier(X0)))
| ( ( ~ point_neighbourhood(X2,X0,X1)
| in(X1,interior(X0,X2)) )
& ( ~ in(X1,interior(X0,X2))
| point_neighbourhood(X2,X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f263]) ).
fof(f384,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ! [X1,X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ! [X3] :
( ~ element(X3,powerset(the_carrier(X0)))
| ~ in(X2,X3)
| ~ open_subset(X3,X0)
| in(X3,X1) ) )
& ( ? [X3] :
( element(X3,powerset(the_carrier(X0)))
& in(X2,X3)
& open_subset(X3,X0)
& ~ in(X3,X1) )
| is_a_convergence_point_of_set(X0,X1,X2) ) ) ),
inference(nnf_transformation,[],[f267]) ).
fof(f385,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ! [X1,X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ! [X4] :
( ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X2,X4)
| ~ open_subset(X4,X0)
| in(X4,X1) ) )
& ( ? [X3] :
( element(X3,powerset(the_carrier(X0)))
& in(X2,X3)
& open_subset(X3,X0)
& ~ in(X3,X1) )
| is_a_convergence_point_of_set(X0,X1,X2) ) ) ),
inference(rectify,[],[f384]) ).
fof(f386,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ! [X1,X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ! [X4] :
( ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X2,X4)
| ~ open_subset(X4,X0)
| in(X4,X1) ) )
& ( ( element(sK5(X0,X1,X2),powerset(the_carrier(X0)))
& in(X2,sK5(X0,X1,X2))
& open_subset(sK5(X0,X1,X2),X0)
& ~ in(sK5(X0,X1,X2),X1) )
| is_a_convergence_point_of_set(X0,X1,X2) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1,X2))],[f385]) ).
fof(f434,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ in(X2,filter_of_net_str(X0,X1))
| ( element(X2,powerset(the_carrier(X0)))
& is_eventually_in(X0,X1,X2) ) )
& ( ~ element(X2,powerset(the_carrier(X0)))
| ~ is_eventually_in(X0,X1,X2)
| in(X2,filter_of_net_str(X0,X1)) ) ) ) ),
inference(nnf_transformation,[],[f356]) ).
fof(f435,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ! [X2] :
( ( ~ in(X2,filter_of_net_str(X0,X1))
| ( element(X2,powerset(the_carrier(X0)))
& is_eventually_in(X0,X1,X2) ) )
& ( ~ element(X2,powerset(the_carrier(X0)))
| ~ is_eventually_in(X0,X1,X2)
| in(X2,filter_of_net_str(X0,X1)) ) ) ) ),
inference(flattening,[],[f434]) ).
fof(f436,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,X1))
| is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
& ( ~ in(X2,lim_points_of_net(X0,X1))
| ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(nnf_transformation,[],[f358]) ).
fof(f437,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,X1))
| is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
& ( ~ in(X2,lim_points_of_net(X0,X1))
| ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(flattening,[],[f436]) ).
fof(f438,plain,
( top_str(sK49)
& topological_space(sK49)
& ~ empty_carrier(sK49)
& net_str(sK50,sK49)
& directed_relstr(sK50)
& transitive_relstr(sK50)
& ~ empty_carrier(sK50)
& element(sK51,the_carrier(sK49))
& ( in(sK51,lim_points_of_net(sK49,sK50))
| is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) )
& ( ~ in(sK51,lim_points_of_net(sK49,sK50))
| ~ is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49,sK50,sK51]),skolemize(X0,sK49),skolemize(X1,sK50),skolemize(X2,sK51)],[f437]) ).
fof(f441,plain,
! [X0,X1] :
( ( ~ element(X0,powerset(X1))
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f128]) ).
fof(f506,plain,
! [X2,X0,X1,X8,X6] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(X2,powerset(the_carrier(X0)))
| lim_points_of_net(X0,X1) != X2
| ~ element(X6,the_carrier(X0))
| ~ in(X6,X2)
| ~ point_neighbourhood(X8,X0,X6)
| is_eventually_in(X0,X1,X8) ),
inference(cnf_transformation,[],[f382]) ).
fof(f507,plain,
! [X2,X0,X1,X6] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(X2,powerset(the_carrier(X0)))
| lim_points_of_net(X0,X1) != X2
| ~ element(X6,the_carrier(X0))
| point_neighbourhood(sK4(X0,X1,X6),X0,X6)
| in(X6,X2) ),
inference(cnf_transformation,[],[f382]) ).
fof(f508,plain,
! [X2,X0,X1,X6] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(X2,powerset(the_carrier(X0)))
| lim_points_of_net(X0,X1) != X2
| ~ element(X6,the_carrier(X0))
| ~ is_eventually_in(X0,X1,sK4(X0,X1,X6))
| in(X6,X2) ),
inference(cnf_transformation,[],[f382]) ).
fof(f513,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ point_neighbourhood(X2,X0,X1)
| in(X1,interior(X0,X2)) ),
inference(cnf_transformation,[],[f383]) ).
fof(f516,plain,
! [X2,X0,X1,X4] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ~ is_a_convergence_point_of_set(X0,X1,X2)
| ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X2,X4)
| ~ open_subset(X4,X0)
| in(X4,X1) ),
inference(cnf_transformation,[],[f386]) ).
fof(f517,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| element(sK5(X0,X1,X2),powerset(the_carrier(X0)))
| is_a_convergence_point_of_set(X0,X1,X2) ),
inference(cnf_transformation,[],[f386]) ).
fof(f518,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| in(X2,sK5(X0,X1,X2))
| is_a_convergence_point_of_set(X0,X1,X2) ),
inference(cnf_transformation,[],[f386]) ).
fof(f519,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| open_subset(sK5(X0,X1,X2),X0)
| is_a_convergence_point_of_set(X0,X1,X2) ),
inference(cnf_transformation,[],[f386]) ).
fof(f520,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| ~ in(sK5(X0,X1,X2),X1)
| is_a_convergence_point_of_set(X0,X1,X2) ),
inference(cnf_transformation,[],[f386]) ).
fof(f523,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f270]) ).
fof(f524,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| element(interior(X0,X1),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f272]) ).
fof(f530,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f532,plain,
! [X2,X0,X1] :
( ~ element(X1,the_carrier(X0))
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ point_neighbourhood(X2,X0,X1)
| element(X2,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f280]) ).
fof(f589,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| open_subset(interior(X0,X1),X0) ),
inference(cnf_transformation,[],[f316]) ).
fof(f767,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ in(X2,filter_of_net_str(X0,X1))
| is_eventually_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f435]) ).
fof(f768,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ is_eventually_in(X0,X1,X2)
| in(X2,filter_of_net_str(X0,X1)) ),
inference(cnf_transformation,[],[f435]) ).
fof(f769,plain,
top_str(sK49),
inference(cnf_transformation,[],[f438]) ).
fof(f770,plain,
topological_space(sK49),
inference(cnf_transformation,[],[f438]) ).
fof(f771,plain,
~ empty_carrier(sK49),
inference(cnf_transformation,[],[f438]) ).
fof(f772,plain,
net_str(sK50,sK49),
inference(cnf_transformation,[],[f438]) ).
fof(f773,plain,
directed_relstr(sK50),
inference(cnf_transformation,[],[f438]) ).
fof(f774,plain,
transitive_relstr(sK50),
inference(cnf_transformation,[],[f438]) ).
fof(f775,plain,
~ empty_carrier(sK50),
inference(cnf_transformation,[],[f438]) ).
fof(f776,plain,
element(sK51,the_carrier(sK49)),
inference(cnf_transformation,[],[f438]) ).
fof(f777,plain,
( in(sK51,lim_points_of_net(sK49,sK50))
| is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) ),
inference(cnf_transformation,[],[f438]) ).
fof(f778,plain,
( ~ in(sK51,lim_points_of_net(sK49,sK50))
| ~ is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) ),
inference(cnf_transformation,[],[f438]) ).
fof(f783,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f441]) ).
fof(f784,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f441]) ).
fof(f785,plain,
! [X0,X1] :
( ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| subset(interior(X0,X1),X1) ),
inference(cnf_transformation,[],[f363]) ).
fof(f786,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f365]) ).
fof(f787,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ element(X2,the_carrier(X0))
| ~ in(X2,X1)
| ~ open_subset(X1,X0)
| point_neighbourhood(X1,X0,X2) ),
inference(cnf_transformation,[],[f367]) ).
fof(f793,plain,
! [X2,X3,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ subset(X2,X3)
| ~ is_eventually_in(X0,X1,X2)
| is_eventually_in(X0,X1,X3) ),
inference(cnf_transformation,[],[f373]) ).
fof(f794,plain,
! [X0,X1,X6] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| ~ element(X6,the_carrier(X0))
| ~ is_eventually_in(X0,X1,sK4(X0,X1,X6))
| in(X6,lim_points_of_net(X0,X1)) ),
inference(equality_resolution,[],[f508]) ).
fof(f795,plain,
! [X0,X1,X6] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| ~ element(X6,the_carrier(X0))
| point_neighbourhood(sK4(X0,X1,X6),X0,X6)
| in(X6,lim_points_of_net(X0,X1)) ),
inference(equality_resolution,[],[f507]) ).
fof(f796,plain,
! [X0,X1,X8,X6] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| ~ element(X6,the_carrier(X0))
| ~ in(X6,lim_points_of_net(X0,X1))
| ~ point_neighbourhood(X8,X0,X6)
| is_eventually_in(X0,X1,X8) ),
inference(equality_resolution,[],[f506]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(X2,lim_points_of_net(X0,X1))
| ~ directed_relstr(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X0))
| ~ element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| ~ is_eventually_in(X0,X1,sK4(X0,X1,X2)) ),
inference(cnf_transformation,[],[f794]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(X2,lim_points_of_net(X0,X1))
| point_neighbourhood(sK4(X0,X1,X2),X0,X2)
| ~ directed_relstr(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X0))
| ~ element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f795]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_eventually_in(X0,X1,X3)
| ~ directed_relstr(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X0))
| ~ point_neighbourhood(X3,X0,X2)
| ~ in(X2,lim_points_of_net(X0,X1))
| ~ element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f796]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| in(X2,interior(X1,X0))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,the_carrier(X1))
| ~ point_neighbourhood(X0,X1,X2)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f513]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X1,X2)
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ in(sK5(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f520]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X1,X2)
| open_subset(sK5(X0,X1,X2),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[],[f519]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X2,X1)
| in(X1,sK5(X0,X2,X1))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[],[f518]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X1,X2)
| element(sK5(X0,X1,X2),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[],[f517]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X0,X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ open_subset(X0,X1)
| ~ in(X3,X0)
| ~ is_a_convergence_point_of_set(X1,X2,X3)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f516]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| element(lim_points_of_net(X1,X0),powerset(the_carrier(X1)))
| ~ directed_relstr(X0)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X0)
| ~ net_str(X0,X1) ),
inference(cnf_transformation,[],[f523]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i] :
( element(interior(X1,X0),powerset(the_carrier(X1)))
| ~ top_str(X1)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f524]) ).
tcf(c_115,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| element(X0,powerset(the_carrier(X1)))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,the_carrier(X1))
| ~ point_neighbourhood(X0,X1,X2) ),
inference(cnf_transformation,[],[f532]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] :
( open_subset(interior(X1,X0),X1)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f589]) ).
tcf(c_351,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| in(X0,filter_of_net_str(X1,X2))
| ~ one_sorted_str(X1)
| ~ net_str(X2,X1)
| ~ is_eventually_in(X1,X2,X0)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f768]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_eventually_in(X1,X2,X0)
| ~ one_sorted_str(X1)
| ~ net_str(X2,X1)
| ~ in(X0,filter_of_net_str(X1,X2)) ),
inference(cnf_transformation,[],[f767]) ).
tcf(c_354,negated_conjecture,
( ~ in(sK51,lim_points_of_net(sK49,sK50))
| ~ is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) ),
inference(cnf_transformation,[],[f778]) ).
tcf(c_355,negated_conjecture,
( in(sK51,lim_points_of_net(sK49,sK50))
| is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) ),
inference(cnf_transformation,[],[f777]) ).
tcf(c_356,negated_conjecture,
element(sK51,the_carrier(sK49)),
inference(cnf_transformation,[],[f776]) ).
tcf(c_357,negated_conjecture,
~ empty_carrier(sK50),
inference(cnf_transformation,[],[f775]) ).
tcf(c_358,negated_conjecture,
transitive_relstr(sK50),
inference(cnf_transformation,[],[f774]) ).
tcf(c_359,negated_conjecture,
directed_relstr(sK50),
inference(cnf_transformation,[],[f773]) ).
tcf(c_360,negated_conjecture,
net_str(sK50,sK49),
inference(cnf_transformation,[],[f772]) ).
tcf(c_361,negated_conjecture,
~ empty_carrier(sK49),
inference(cnf_transformation,[],[f771]) ).
tcf(c_362,negated_conjecture,
topological_space(sK49),
inference(cnf_transformation,[],[f770]) ).
tcf(c_363,negated_conjecture,
top_str(sK49),
inference(cnf_transformation,[],[f769]) ).
tcf(c_368,plain,
! [X0: $i,X1: $i] :
( element(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f784]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f783]) ).
tcf(c_370,plain,
! [X0: $i,X1: $i] :
( subset(interior(X1,X0),X0)
| ~ top_str(X1)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f785]) ).
tcf(c_371,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f786]) ).
tcf(c_372,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| point_neighbourhood(X0,X1,X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ open_subset(X0,X1)
| ~ in(X2,X0)
| ~ element(X2,the_carrier(X1))
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f787]) ).
tcf(c_377,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| is_eventually_in(X0,X1,X3)
| ~ one_sorted_str(X0)
| ~ subset(X2,X3)
| ~ net_str(X1,X0)
| ~ is_eventually_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f793]) ).
tcf(c_531,plain,
! [X0: $i,X1: $i] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_369]) ).
tcf(c_532,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(renaming,[status(thm)],[c_531]) ).
tcf(c_533,plain,
! [X0: $i,X1: $i] :
( element(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_368]) ).
tcf(c_619,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(prop_impl_just,[status(thm)],[c_115]) ).
tcf(c_766,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X0,X2)
| ~ subset(X1,X2)
| ~ in(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_371,c_533]) ).
tcf(c_781,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| in(X2,interior(X1,X0))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,the_carrier(X1))
| ~ point_neighbourhood(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_99,c_117,c_99]) ).
tcf(c_2148,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| in(X0,lim_points_of_net(X1,X2))
| point_neighbourhood(sK4(X1,X2,X0),X1,X0)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ element(X0,the_carrier(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_96,c_108]) ).
tcf(c_2149,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(X2,lim_points_of_net(X0,X1))
| ~ directed_relstr(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X0))
| ~ is_eventually_in(X0,X1,sK4(X0,X1,X2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_95,c_108]) ).
tcf(c_2150,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_eventually_in(X1,X2,X3)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ element(X0,the_carrier(X1))
| ~ point_neighbourhood(X3,X1,X0)
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_97,c_108]) ).
tcf(c_2838,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( element(X4,X3)
| ~ in(X4,X1)
| ~ element(X0,powerset(X2))
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_532,c_766]) ).
tcf(c_2839,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(unflattening,[status(thm)],[c_2838]) ).
tcf(c_2909,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| point_neighbourhood(X0,X1,X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ open_subset(X0,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_372,c_2839]) ).
tcf(c_4066,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(X2,lim_points_of_net(X0,X1))
| ~ directed_relstr(X1)
| ~ top_str(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X0))
| ~ is_eventually_in(X0,X1,sK4(X0,X1,X2))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_2149,c_362]) ).
tcf(c_4067,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK49)
| empty_carrier(X0)
| in(X1,lim_points_of_net(sK49,X0))
| ~ top_str(sK49)
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| ~ net_str(X0,sK49)
| ~ element(X1,the_carrier(sK49))
| ~ is_eventually_in(sK49,X0,sK4(sK49,X0,X1)) ),
inference(unflattening,[status(thm)],[c_4066]) ).
tcf(c_4069,plain,
! [X0: $i,X1: $i] :
( ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| ~ net_str(X0,sK49)
| ~ element(X1,the_carrier(sK49))
| ~ is_eventually_in(sK49,X0,sK4(sK49,X0,X1))
| in(X1,lim_points_of_net(sK49,X0))
| empty_carrier(X0) ),
inference(global_subsumption_just,[status(thm)],[c_4067,c_363,c_361,c_4067]) ).
tcf(c_4070,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| in(X1,lim_points_of_net(sK49,X0))
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| ~ net_str(X0,sK49)
| ~ element(X1,the_carrier(sK49))
| ~ is_eventually_in(sK49,X0,sK4(sK49,X0,X1)) ),
inference(renaming,[status(thm)],[c_4069]) ).
tcf(c_4198,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X1,X2)
| element(sK5(X0,X1,X2),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_104,c_362]) ).
tcf(c_4199,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X0,X1)
| element(sK5(sK49,X0,X1),powerset(the_carrier(sK49)))
| ~ top_str(sK49) ),
inference(unflattening,[status(thm)],[c_4198]) ).
tcf(c_4210,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X2,X1)
| in(X1,sK5(X0,X2,X1))
| ~ top_str(X0)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_103,c_362]) ).
tcf(c_4211,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X1,X0)
| in(X0,sK5(sK49,X1,X0))
| ~ top_str(sK49) ),
inference(unflattening,[status(thm)],[c_4210]) ).
tcf(c_4222,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X1,X2)
| open_subset(sK5(X0,X1,X2),X0)
| ~ top_str(X0)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_102,c_362]) ).
tcf(c_4223,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X0,X1)
| open_subset(sK5(sK49,X0,X1),sK49)
| ~ top_str(sK49) ),
inference(unflattening,[status(thm)],[c_4222]) ).
tcf(c_4234,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_convergence_point_of_set(X0,X1,X2)
| ~ top_str(X0)
| ~ in(sK5(X0,X1,X2),X1)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_101,c_362]) ).
tcf(c_4235,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X0,X1)
| ~ top_str(sK49)
| ~ in(sK5(sK49,X0,X1),X0) ),
inference(unflattening,[status(thm)],[c_4234]) ).
tcf(c_4306,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| point_neighbourhood(X1,X0,X2)
| ~ top_str(X0)
| ~ open_subset(X1,X0)
| ~ in(X2,X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_2909,c_362]) ).
tcf(c_4307,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK49)
| point_neighbourhood(X0,sK49,X1)
| ~ top_str(sK49)
| ~ open_subset(X0,sK49)
| ~ in(X1,X0)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(unflattening,[status(thm)],[c_4306]) ).
tcf(c_4308,plain,
! [X0: $i,X1: $i] :
( ~ open_subset(X0,sK49)
| ~ in(X1,X0)
| ~ element(X0,powerset(the_carrier(sK49)))
| point_neighbourhood(X0,sK49,X1) ),
inference(global_subsumption_just,[status(thm)],[c_4307,c_363,c_361,c_4307]) ).
tcf(c_4309,plain,
! [X0: $i,X1: $i] :
( point_neighbourhood(X0,sK49,X1)
| ~ open_subset(X0,sK49)
| ~ in(X1,X0)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(renaming,[status(thm)],[c_4308]) ).
tcf(c_4322,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X2)
| empty_carrier(X0)
| is_eventually_in(X0,X2,X3)
| ~ directed_relstr(X2)
| ~ top_str(X0)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X0)
| ~ element(X1,the_carrier(X0))
| ~ point_neighbourhood(X3,X0,X1)
| ~ in(X1,lim_points_of_net(X0,X2))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_2150,c_362]) ).
tcf(c_4323,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK49)
| empty_carrier(X1)
| is_eventually_in(sK49,X1,X2)
| ~ top_str(sK49)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ net_str(X1,sK49)
| ~ element(X0,the_carrier(sK49))
| ~ point_neighbourhood(X2,sK49,X0)
| ~ in(X0,lim_points_of_net(sK49,X1)) ),
inference(unflattening,[status(thm)],[c_4322]) ).
tcf(c_4325,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ net_str(X1,sK49)
| ~ element(X0,the_carrier(sK49))
| ~ point_neighbourhood(X2,sK49,X0)
| ~ in(X0,lim_points_of_net(sK49,X1))
| is_eventually_in(sK49,X1,X2)
| empty_carrier(X1) ),
inference(global_subsumption_just,[status(thm)],[c_4323,c_363,c_361,c_4323]) ).
tcf(c_4326,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| is_eventually_in(sK49,X1,X2)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ net_str(X1,sK49)
| ~ element(X0,the_carrier(sK49))
| ~ point_neighbourhood(X2,sK49,X0)
| ~ in(X0,lim_points_of_net(sK49,X1)) ),
inference(renaming,[status(thm)],[c_4325]) ).
tcf(c_4352,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X0)
| in(X1,lim_points_of_net(X0,X2))
| point_neighbourhood(sK4(X0,X2,X1),X0,X1)
| ~ directed_relstr(X2)
| ~ top_str(X0)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X0)
| ~ element(X1,the_carrier(X0))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_2148,c_362]) ).
tcf(c_4353,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK49)
| empty_carrier(X1)
| in(X0,lim_points_of_net(sK49,X1))
| point_neighbourhood(sK4(sK49,X1,X0),sK49,X0)
| ~ top_str(sK49)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ net_str(X1,sK49)
| ~ element(X0,the_carrier(sK49)) ),
inference(unflattening,[status(thm)],[c_4352]) ).
tcf(c_4355,plain,
! [X0: $i,X1: $i] :
( ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ net_str(X1,sK49)
| ~ element(X0,the_carrier(sK49))
| point_neighbourhood(sK4(sK49,X1,X0),sK49,X0)
| in(X0,lim_points_of_net(sK49,X1))
| empty_carrier(X1) ),
inference(global_subsumption_just,[status(thm)],[c_4353,c_363,c_361,c_4353]) ).
tcf(c_4356,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| in(X0,lim_points_of_net(sK49,X1))
| point_neighbourhood(sK4(sK49,X1,X0),sK49,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ net_str(X1,sK49)
| ~ element(X0,the_carrier(sK49)) ),
inference(renaming,[status(thm)],[c_4355]) ).
tcf(c_4379,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| in(X2,interior(X0,X1))
| ~ top_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ point_neighbourhood(X1,X0,X2)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_781,c_362]) ).
tcf(c_4380,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK49)
| in(X1,interior(sK49,X0))
| ~ top_str(sK49)
| ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,X1) ),
inference(unflattening,[status(thm)],[c_4379]) ).
tcf(c_4382,plain,
! [X0: $i,X1: $i] :
( ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,X1)
| in(X1,interior(sK49,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_4380,c_363,c_361,c_4380]) ).
tcf(c_4383,plain,
! [X0: $i,X1: $i] :
( in(X1,interior(sK49,X0))
| ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,X1) ),
inference(renaming,[status(thm)],[c_4382]) ).
tcf(c_4394,plain,
! [X0: $i,X1: $i] :
( open_subset(interior(X0,X1),X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_174,c_362]) ).
tcf(c_4395,plain,
! [X0: $i] :
( open_subset(interior(sK49,X0),sK49)
| ~ top_str(sK49)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(unflattening,[status(thm)],[c_4394]) ).
tcf(c_4418,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ point_neighbourhood(X1,X0,X2)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_117,c_362]) ).
tcf(c_4419,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK49)
| element(X0,powerset(the_carrier(sK49)))
| ~ top_str(sK49)
| ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,X1) ),
inference(unflattening,[status(thm)],[c_4418]) ).
tcf(c_4421,plain,
! [X0: $i,X1: $i] :
( ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,X1)
| element(X0,powerset(the_carrier(sK49))) ),
inference(global_subsumption_just,[status(thm)],[c_4419,c_363,c_361,c_4419]) ).
tcf(c_4422,plain,
! [X0: $i,X1: $i] :
( element(X0,powerset(the_carrier(sK49)))
| ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,X1) ),
inference(renaming,[status(thm)],[c_4421]) ).
tcf(c_4454,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X1,X2)
| ~ top_str(X0)
| ~ open_subset(X1,X0)
| ~ in(X3,X1)
| ~ is_a_convergence_point_of_set(X0,X2,X3)
| ~ element(X1,powerset(the_carrier(X0)))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_105,c_362]) ).
tcf(c_4455,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X1)
| ~ top_str(sK49)
| ~ open_subset(X0,sK49)
| ~ in(X2,X0)
| ~ is_a_convergence_point_of_set(sK49,X1,X2)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(unflattening,[status(thm)],[c_4454]) ).
tcf(c_4456,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X1)
| ~ element(X0,powerset(the_carrier(sK49)))
| ~ is_a_convergence_point_of_set(sK49,X1,X2)
| ~ in(X2,X0)
| ~ open_subset(X0,sK49) ),
inference(global_subsumption_just,[status(thm)],[c_4455,c_363,c_4455]) ).
tcf(c_4457,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X1)
| ~ open_subset(X0,sK49)
| ~ in(X2,X0)
| ~ is_a_convergence_point_of_set(sK49,X1,X2)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(renaming,[status(thm)],[c_4456]) ).
tcf(c_4719,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_619,c_363]) ).
tcf(c_4720,plain,
one_sorted_str(sK49),
inference(unflattening,[status(thm)],[c_4719]) ).
tcf(c_4778,plain,
! [X0: $i,X1: $i] :
( subset(interior(X0,X1),X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_370,c_363]) ).
tcf(c_4779,plain,
! [X0: $i] :
( subset(interior(sK49,X0),X0)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(unflattening,[status(thm)],[c_4778]) ).
tcf(c_4811,plain,
! [X0: $i,X1: $i] :
( element(interior(X0,X1),powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ( X0 != sK49 ) ),
inference(resolution_lifted,[status(thm)],[c_109,c_363]) ).
tcf(c_4812,plain,
! [X0: $i] :
( element(interior(sK49,X0),powerset(the_carrier(sK49)))
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(unflattening,[status(thm)],[c_4811]) ).
tcf(c_5921,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| in(X1,lim_points_of_net(sK49,X0))
| point_neighbourhood(sK4(sK49,X0,X1),sK49,X1)
| ~ transitive_relstr(X0)
| ~ net_str(X0,sK49)
| ~ element(X1,the_carrier(sK49))
| ( X0 != sK50 ) ),
inference(resolution_lifted,[status(thm)],[c_4356,c_359]) ).
tcf(c_5922,plain,
! [X0: $i] :
( empty_carrier(sK50)
| in(X0,lim_points_of_net(sK49,sK50))
| point_neighbourhood(sK4(sK49,sK50,X0),sK49,X0)
| ~ transitive_relstr(sK50)
| ~ net_str(sK50,sK49)
| ~ element(X0,the_carrier(sK49)) ),
inference(unflattening,[status(thm)],[c_5921]) ).
tcf(c_5924,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(sK49))
| point_neighbourhood(sK4(sK49,sK50,X0),sK49,X0)
| in(X0,lim_points_of_net(sK49,sK50)) ),
inference(global_subsumption_just,[status(thm)],[c_5922,c_358,c_360,c_357,c_5922]) ).
tcf(c_5925,plain,
! [X0: $i] :
( in(X0,lim_points_of_net(sK49,sK50))
| point_neighbourhood(sK4(sK49,sK50,X0),sK49,X0)
| ~ element(X0,the_carrier(sK49)) ),
inference(renaming,[status(thm)],[c_5924]) ).
tcf(c_5936,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| is_eventually_in(sK49,X0,X2)
| ~ transitive_relstr(X0)
| ~ net_str(X0,sK49)
| ~ element(X1,the_carrier(sK49))
| ~ point_neighbourhood(X2,sK49,X1)
| ~ in(X1,lim_points_of_net(sK49,X0))
| ( X0 != sK50 ) ),
inference(resolution_lifted,[status(thm)],[c_4326,c_359]) ).
tcf(c_5937,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK50)
| is_eventually_in(sK49,sK50,X1)
| ~ transitive_relstr(sK50)
| ~ net_str(sK50,sK49)
| ~ element(X0,the_carrier(sK49))
| ~ point_neighbourhood(X1,sK49,X0)
| ~ in(X0,lim_points_of_net(sK49,sK50)) ),
inference(unflattening,[status(thm)],[c_5936]) ).
tcf(c_5939,plain,
! [X0: $i,X1: $i] :
( ~ in(X0,lim_points_of_net(sK49,sK50))
| ~ point_neighbourhood(X1,sK49,X0)
| ~ element(X0,the_carrier(sK49))
| is_eventually_in(sK49,sK50,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5937,c_358,c_360,c_357,c_5937]) ).
tcf(c_5940,plain,
! [X0: $i,X1: $i] :
( is_eventually_in(sK49,sK50,X1)
| ~ element(X0,the_carrier(sK49))
| ~ point_neighbourhood(X1,sK49,X0)
| ~ in(X0,lim_points_of_net(sK49,sK50)) ),
inference(renaming,[status(thm)],[c_5939]) ).
tcf(c_6139,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| in(X1,lim_points_of_net(sK49,X0))
| ~ transitive_relstr(X0)
| ~ net_str(X0,sK49)
| ~ element(X1,the_carrier(sK49))
| ~ is_eventually_in(sK49,X0,sK4(sK49,X0,X1))
| ( X0 != sK50 ) ),
inference(resolution_lifted,[status(thm)],[c_4070,c_359]) ).
tcf(c_6140,plain,
! [X0: $i] :
( empty_carrier(sK50)
| in(X0,lim_points_of_net(sK49,sK50))
| ~ transitive_relstr(sK50)
| ~ net_str(sK50,sK49)
| ~ element(X0,the_carrier(sK49))
| ~ is_eventually_in(sK49,sK50,sK4(sK49,sK50,X0)) ),
inference(unflattening,[status(thm)],[c_6139]) ).
tcf(c_6142,plain,
! [X0: $i] :
( ~ is_eventually_in(sK49,sK50,sK4(sK49,sK50,X0))
| ~ element(X0,the_carrier(sK49))
| in(X0,lim_points_of_net(sK49,sK50)) ),
inference(global_subsumption_just,[status(thm)],[c_6140,c_358,c_360,c_357,c_6140]) ).
tcf(c_6143,plain,
! [X0: $i] :
( in(X0,lim_points_of_net(sK49,sK50))
| ~ element(X0,the_carrier(sK49))
| ~ is_eventually_in(sK49,sK50,sK4(sK49,sK50,X0)) ),
inference(renaming,[status(thm)],[c_6142]) ).
tcf(c_13936,plain,
! [X0: $i] :
( open_subset(interior(sK49,X0),sK49)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(prop_impl_just,[status(thm)],[c_363,c_4395]) ).
tcf(c_13938,plain,
! [X0: $i] :
( subset(interior(sK49,X0),X0)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(prop_impl_just,[status(thm)],[c_4779]) ).
tcf(c_13940,plain,
! [X0: $i] :
( element(interior(sK49,X0),powerset(the_carrier(sK49)))
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(prop_impl_just,[status(thm)],[c_4812]) ).
tcf(c_13962,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X0,X1)
| element(sK5(sK49,X0,X1),powerset(the_carrier(sK49))) ),
inference(prop_impl_just,[status(thm)],[c_363,c_4199]) ).
tcf(c_13966,plain,
! [X0: $i,X1: $i] :
( open_subset(sK5(sK49,X0,X1),sK49)
| is_a_convergence_point_of_set(sK49,X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_363,c_4223]) ).
tcf(c_13967,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X0,X1)
| open_subset(sK5(sK49,X0,X1),sK49) ),
inference(renaming,[status(thm)],[c_13966]) ).
tcf(c_13968,plain,
! [X0: $i,X1: $i] :
( ~ in(sK5(sK49,X0,X1),X0)
| is_a_convergence_point_of_set(sK49,X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_363,c_4235]) ).
tcf(c_13969,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X0,X1)
| ~ in(sK5(sK49,X0,X1),X0) ),
inference(renaming,[status(thm)],[c_13968]) ).
tcf(c_13970,plain,
! [X0: $i,X1: $i] :
( is_a_convergence_point_of_set(sK49,X1,X0)
| in(X0,sK5(sK49,X1,X0)) ),
inference(prop_impl_just,[status(thm)],[c_363,c_4211]) ).
tcf(c_26644,plain,
( in(sK51,lim_points_of_net(sK49,sK50))
| point_neighbourhood(sK4(sK49,sK50,sK51),sK49,sK51)
| ~ element(sK51,the_carrier(sK49)) ),
inference(instantiation,[status(thm)],[c_5925]) ).
tcf(c_27759,plain,
! [X0: $i] :
( is_eventually_in(sK49,sK50,X0)
| ~ element(sK51,the_carrier(sK49))
| ~ point_neighbourhood(X0,sK49,sK51)
| ~ in(sK51,lim_points_of_net(sK49,sK50)) ),
inference(instantiation,[status(thm)],[c_5940]) ).
tcf(c_27773,plain,
( is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51)
| ~ in(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),filter_of_net_str(sK49,sK50)) ),
inference(instantiation,[status(thm)],[c_13969]) ).
tcf(c_27774,plain,
( is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51)
| open_subset(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),sK49) ),
inference(instantiation,[status(thm)],[c_13967]) ).
tcf(c_27775,plain,
( is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51)
| element(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_13962]) ).
tcf(c_27776,plain,
( is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51)
| in(sK51,sK5(sK49,filter_of_net_str(sK49,sK50),sK51)) ),
inference(instantiation,[status(thm)],[c_13970]) ).
tcf(c_30370,plain,
( in(sK51,interior(sK49,sK4(sK49,sK50,sK51)))
| ~ element(sK51,the_carrier(sK49))
| ~ point_neighbourhood(sK4(sK49,sK50,sK51),sK49,sK51) ),
inference(instantiation,[status(thm)],[c_4383]) ).
tcf(c_30371,plain,
( element(sK4(sK49,sK50,sK51),powerset(the_carrier(sK49)))
| ~ element(sK51,the_carrier(sK49))
| ~ point_neighbourhood(sK4(sK49,sK50,sK51),sK49,sK51) ),
inference(instantiation,[status(thm)],[c_4422]) ).
tcf(c_30638,plain,
( point_neighbourhood(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),sK49,sK51)
| ~ open_subset(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),sK49)
| ~ in(sK51,sK5(sK49,filter_of_net_str(sK49,sK50),sK51))
| ~ element(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_4309]) ).
tcf(c_34813,plain,
( subset(interior(sK49,sK4(sK49,sK50,sK51)),sK4(sK49,sK50,sK51))
| ~ element(sK4(sK49,sK50,sK51),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_13938]) ).
tcf(c_34814,plain,
( element(interior(sK49,sK4(sK49,sK50,sK51)),powerset(the_carrier(sK49)))
| ~ element(sK4(sK49,sK50,sK51),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_13940]) ).
tcf(c_34815,plain,
( open_subset(interior(sK49,sK4(sK49,sK50,sK51)),sK49)
| ~ element(sK4(sK49,sK50,sK51),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_13936]) ).
tcf(c_41926,plain,
( is_eventually_in(sK49,sK50,sK5(sK49,filter_of_net_str(sK49,sK50),sK51))
| ~ element(sK51,the_carrier(sK49))
| ~ in(sK51,lim_points_of_net(sK49,sK50))
| ~ point_neighbourhood(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),sK49,sK51) ),
inference(instantiation,[status(thm)],[c_27759]) ).
tcf(c_48252,plain,
( empty_carrier(sK50)
| empty_carrier(sK49)
| in(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),filter_of_net_str(sK49,sK50))
| ~ one_sorted_str(sK49)
| ~ net_str(sK50,sK49)
| ~ is_eventually_in(sK49,sK50,sK5(sK49,filter_of_net_str(sK49,sK50),sK51))
| ~ element(sK5(sK49,filter_of_net_str(sK49,sK50),sK51),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_62014,plain,
! [X0: $i,X1: $i] :
( in(X0,X1)
| ~ open_subset(X0,sK49)
| ~ in(sK51,X0)
| ~ is_a_convergence_point_of_set(sK49,X1,sK51)
| ~ element(X0,powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_4457]) ).
tcf(c_65238,plain,
! [X0: $i] :
( in(X0,filter_of_net_str(sK49,sK50))
| ~ open_subset(X0,sK49)
| ~ in(sK51,X0)
| ~ element(X0,powerset(the_carrier(sK49)))
| ~ is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51) ),
inference(instantiation,[status(thm)],[c_62014]) ).
tcf(c_67179,plain,
( in(interior(sK49,sK4(sK49,sK50,sK51)),filter_of_net_str(sK49,sK50))
| ~ is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51)
| ~ open_subset(interior(sK49,sK4(sK49,sK50,sK51)),sK49)
| ~ in(sK51,interior(sK49,sK4(sK49,sK50,sK51)))
| ~ element(interior(sK49,sK4(sK49,sK50,sK51)),powerset(the_carrier(sK49))) ),
inference(instantiation,[status(thm)],[c_65238]) ).
tcf(c_72896,negated_conjecture,
is_a_convergence_point_of_set(sK49,filter_of_net_str(sK49,sK50),sK51),
inference(global_subsumption_just,[status(thm)],[c_355,c_361,c_360,c_357,c_356,c_355,c_4720,c_27775,c_27774,c_27773,c_27776,c_30638,c_41926,c_48252]) ).
tcf(c_138070,plain,
( empty_carrier(sK50)
| empty_carrier(sK49)
| is_eventually_in(sK49,sK50,interior(sK49,sK4(sK49,sK50,sK51)))
| ~ one_sorted_str(sK49)
| ~ net_str(sK50,sK49)
| ~ in(interior(sK49,sK4(sK49,sK50,sK51)),filter_of_net_str(sK49,sK50)) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_144143,plain,
! [X0: $i] :
( empty_carrier(sK50)
| empty_carrier(sK49)
| is_eventually_in(sK49,sK50,X0)
| ~ one_sorted_str(sK49)
| ~ net_str(sK50,sK49)
| ~ subset(interior(sK49,sK4(sK49,sK50,sK51)),X0)
| ~ is_eventually_in(sK49,sK50,interior(sK49,sK4(sK49,sK50,sK51))) ),
inference(instantiation,[status(thm)],[c_377]) ).
tcf(c_163457,plain,
( empty_carrier(sK50)
| empty_carrier(sK49)
| is_eventually_in(sK49,sK50,sK4(sK49,sK50,sK51))
| ~ one_sorted_str(sK49)
| ~ net_str(sK50,sK49)
| ~ is_eventually_in(sK49,sK50,interior(sK49,sK4(sK49,sK50,sK51)))
| ~ subset(interior(sK49,sK4(sK49,sK50,sK51)),sK4(sK49,sK50,sK51)) ),
inference(instantiation,[status(thm)],[c_144143]) ).
tcf(c_173923,plain,
( in(sK51,lim_points_of_net(sK49,sK50))
| ~ element(sK51,the_carrier(sK49))
| ~ is_eventually_in(sK49,sK50,sK4(sK49,sK50,sK51)) ),
inference(instantiation,[status(thm)],[c_6143]) ).
tcf(c_173924,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_173923,c_163457,c_138070,c_72896,c_67179,c_34813,c_34814,c_34815,c_30370,c_30371,c_26644,c_4720,c_354,c_356,c_357,c_360,c_361]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU392+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 14:00:41 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 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...
% 154.84/23.08 % SZS status Started for theBenchmark.p
% 154.84/23.08 % SZS status Theorem for theBenchmark.p
% 154.84/23.08
% 154.84/23.08 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 154.84/23.08
% 154.84/23.08 % ------ iProver source info
% 154.84/23.08
% 154.84/23.08 % git: date: 2026-07-19 20:42:38 +0200
% 154.84/23.08 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 154.84/23.08 % git: non_committed_changes: false
% 154.84/23.08
% 154.84/23.08 % ------ Parsing...
% 154.84/23.08 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 154.84/23.08
% 154.84/23.08 % ------ Preprocessing... sup_sim: 0 sf_s rm: 12 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 0 sf_s rm: 19 0s sf_e pe_s pe_e %
% 154.84/23.08
% 154.84/23.08 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 154.84/23.08
% 154.84/23.08 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 154.84/23.08 % ------ Proving...
% 154.84/23.08 % ------ Problem Properties
% 154.84/23.08
% 154.84/23.08 %
% 154.84/23.08 % clauses 325
% 154.84/23.08 % conjectures 6
% 154.84/23.08 % EPR 49
% 154.84/23.08 % Horn 285
% 154.84/23.08 % unary 145
% 154.84/23.08 % binary 117
% 154.84/23.08 % lits 634
% 154.84/23.08 % lits eq 87
% 154.84/23.08 % fd_pure 0
% 154.84/23.08 % fd_pseudo 0
% 154.84/23.08 % fd_cond 9
% 154.84/23.08 % fd_pseudo_cond 9
% 154.84/23.08 % AC symbols 0
% 154.84/23.08
% 154.84/23.08 % ------ Input Options Time Limit: Unbounded
% 154.84/23.08
% 154.84/23.08
% 154.84/23.08 % ------
% 154.84/23.08 % Current options:
% 154.84/23.08 % ------
% 154.84/23.08
% 154.84/23.08
% 154.84/23.08 %
% 154.84/23.08
% 154.84/23.08 % ------ Proving...
% 154.84/23.08 %
% 154.84/23.08
% 154.84/23.08 % SZS status Theorem for theBenchmark.p
% 154.84/23.08
% 154.84/23.08 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 154.84/23.08
% 154.84/23.08
%------------------------------------------------------------------------------