%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU395+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 : n013.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:20 PM UTC 2026
% Result : Theorem 3.55s 16.26s
% Output : CNFRefutation 3.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of formulae : 106 ( 22 unt; 0 def)
% Number of atoms : 632 ( 7 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 843 ( 317 ~; 372 |; 128 &)
% ( 5 <=>; 19 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 156 ( 0 sgn 144 !; 12 ?; 43 :)
% Comments :
%------------------------------------------------------------------------------
fof(f31,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(f34,axiom,
! [X0] :
( one_sorted_str(X0)
=> element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f37,axiom,
! [X0,X1,X2] :
( ( element(X2,powerset(the_carrier(boole_POSet(X1))))
& upper_relstr_subset(X2,boole_POSet(X1))
& filtered_subset(X2,boole_POSet(X1))
& ~ empty(X2)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X1)
& one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ( net_str(net_of_bool_filter(X0,X1,X2),X0)
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yellow19) ).
fof(f40,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f63,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ~ empty(cast_as_carrier_subset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_pre_topc) ).
fof(f73,axiom,
! [X0,X1,X2] :
( ( element(X2,powerset(the_carrier(boole_POSet(X1))))
& upper_relstr_subset(X2,boole_POSet(X1))
& filtered_subset(X2,boole_POSet(X1))
& ~ empty(X2)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X1)
& one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ( strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_yellow19) ).
fof(f76,axiom,
! [X0,X1,X2] :
( ( element(X2,powerset(the_carrier(boole_POSet(X1))))
& proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
& upper_relstr_subset(X2,boole_POSet(X1))
& filtered_subset(X2,boole_POSet(X1))
& ~ empty(X2)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X1)
& one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ( directed_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_yellow19) ).
fof(f125,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,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(f126,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_yellow19) ).
fof(f127,conjecture,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<=> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_yellow19) ).
fof(f128,negated_conjecture,
~ ! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<=> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f127]) ).
fof(f133,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X2))
& in(X0,X1) )
=> element(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f247,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,[],[f31]) ).
fof(f248,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,[],[f247]) ).
fof(f249,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f34]) ).
fof(f252,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ( net_str(net_of_bool_filter(X0,X1,X2),X0)
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f37]) ).
fof(f253,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ( net_str(net_of_bool_filter(X0,X1,X2),X0)
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(flattening,[],[f252]) ).
fof(f255,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f270,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(ennf_transformation,[],[f63]) ).
fof(f271,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(flattening,[],[f270]) ).
fof(f287,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ( strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f73]) ).
fof(f288,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ( strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(flattening,[],[f287]) ).
fof(f293,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ( directed_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f76]) ).
fof(f294,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ( directed_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(flattening,[],[f293]) ).
fof(f339,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,[],[f125]) ).
fof(f340,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,[],[f339]) ).
fof(f341,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(ennf_transformation,[],[f126]) ).
fof(f342,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(flattening,[],[f341]) ).
fof(f343,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<~> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(ennf_transformation,[],[f128]) ).
fof(f344,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<~> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(flattening,[],[f343]) ).
fof(f350,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(ennf_transformation,[],[f133]) ).
fof(f351,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(flattening,[],[f350]) ).
fof(f409,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) )
& ( ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1)) ) ) ) ) ),
inference(nnf_transformation,[],[f340]) ).
fof(f410,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
| is_a_convergence_point_of_set(X0,X1,X2) )
& ( ~ in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
| ~ is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(nnf_transformation,[],[f344]) ).
fof(f411,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1)
& ? [X2] :
( element(X2,the_carrier(X0))
& ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
| is_a_convergence_point_of_set(X0,X1,X2) )
& ( ~ in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
| ~ is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(flattening,[],[f410]) ).
fof(f412,plain,
( top_str(sK46)
& topological_space(sK46)
& ~ empty_carrier(sK46)
& element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
& proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
& upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
& filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
& ~ empty(sK47)
& element(sK48,the_carrier(sK46))
& ( in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| is_a_convergence_point_of_set(sK46,sK47,sK48) )
& ( ~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ is_a_convergence_point_of_set(sK46,sK47,sK48) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47,sK48]),skolemize(X0,sK46),skolemize(X1,sK47),skolemize(X2,sK48)],[f411]) ).
fof(f485,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,[],[f248]) ).
fof(f486,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f249]) ).
fof(f488,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| net_str(net_of_bool_filter(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f253]) ).
fof(f494,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f530,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(cnf_transformation,[],[f271]) ).
fof(f560,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| transitive_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f288]) ).
fof(f562,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f288]) ).
fof(f566,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| directed_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f294]) ).
fof(f773,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ 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(cnf_transformation,[],[f409]) ).
fof(f774,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X0))
| ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1)) ),
inference(cnf_transformation,[],[f409]) ).
fof(f775,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1 ),
inference(cnf_transformation,[],[f342]) ).
fof(f776,plain,
top_str(sK46),
inference(cnf_transformation,[],[f412]) ).
fof(f777,plain,
topological_space(sK46),
inference(cnf_transformation,[],[f412]) ).
fof(f778,plain,
~ empty_carrier(sK46),
inference(cnf_transformation,[],[f412]) ).
fof(f779,plain,
element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))),
inference(cnf_transformation,[],[f412]) ).
fof(f780,plain,
proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))),
inference(cnf_transformation,[],[f412]) ).
fof(f781,plain,
upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46))),
inference(cnf_transformation,[],[f412]) ).
fof(f782,plain,
filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46))),
inference(cnf_transformation,[],[f412]) ).
fof(f783,plain,
~ empty(sK47),
inference(cnf_transformation,[],[f412]) ).
fof(f784,plain,
element(sK48,the_carrier(sK46)),
inference(cnf_transformation,[],[f412]) ).
fof(f785,plain,
( in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| is_a_convergence_point_of_set(sK46,sK47,sK48) ),
inference(cnf_transformation,[],[f412]) ).
fof(f786,plain,
( ~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ is_a_convergence_point_of_set(sK46,sK47,sK48) ),
inference(cnf_transformation,[],[f412]) ).
fof(f792,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f351]) ).
tcf(c_97,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,[],[f485]) ).
tcf(c_98,plain,
! [X0: $i] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f486]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| net_str(net_of_bool_filter(X2,X1,X0),X2)
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ filtered_subset(X0,boole_POSet(X1))
| ~ element(X1,powerset(the_carrier(X2)))
| ~ element(X0,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f488]) ).
tcf(c_106,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f494]) ).
tcf(c_142,plain,
! [X0: $i] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ filtered_subset(X0,boole_POSet(X1))
| ~ element(X1,powerset(the_carrier(X2)))
| ~ empty_carrier(net_of_bool_filter(X2,X1,X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f562]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| transitive_relstr(net_of_bool_filter(X2,X1,X0))
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ filtered_subset(X0,boole_POSet(X1))
| ~ element(X1,powerset(the_carrier(X2)))
| ~ element(X0,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f560]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| directed_relstr(net_of_bool_filter(X2,X1,X0))
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ filtered_subset(X0,boole_POSet(X1))
| ~ element(X1,powerset(the_carrier(X2)))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X0,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f566]) ).
tcf(c_385,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_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ),
inference(cnf_transformation,[],[f774]) ).
tcf(c_386,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_a_convergence_point_of_set(X1,filter_of_net_str(X1,X2),X0)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ element(X0,the_carrier(X1))
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(cnf_transformation,[],[f773]) ).
tcf(c_387,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| ( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0)) = X0 )
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(X1)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(X1)))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) ),
inference(cnf_transformation,[],[f775]) ).
tcf(c_388,negated_conjecture,
( ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
inference(cnf_transformation,[],[f786]) ).
tcf(c_389,negated_conjecture,
( is_a_convergence_point_of_set(sK46,sK47,sK48)
| in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
inference(cnf_transformation,[],[f785]) ).
tcf(c_390,negated_conjecture,
element(sK48,the_carrier(sK46)),
inference(cnf_transformation,[],[f784]) ).
tcf(c_391,negated_conjecture,
~ empty(sK47),
inference(cnf_transformation,[],[f783]) ).
tcf(c_392,negated_conjecture,
filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46))),
inference(cnf_transformation,[],[f782]) ).
tcf(c_393,negated_conjecture,
upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46))),
inference(cnf_transformation,[],[f781]) ).
tcf(c_394,negated_conjecture,
proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))),
inference(cnf_transformation,[],[f780]) ).
tcf(c_395,negated_conjecture,
element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))),
inference(cnf_transformation,[],[f779]) ).
tcf(c_396,negated_conjecture,
~ empty_carrier(sK46),
inference(cnf_transformation,[],[f778]) ).
tcf(c_397,negated_conjecture,
topological_space(sK46),
inference(cnf_transformation,[],[f777]) ).
tcf(c_398,negated_conjecture,
top_str(sK46),
inference(cnf_transformation,[],[f776]) ).
tcf(c_404,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f792]) ).
tcf(c_478,plain,
( one_sorted_str(sK46)
| ~ top_str(sK46) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_483,plain,
( empty_carrier(sK46)
| ~ one_sorted_str(sK46)
| ~ empty(cast_as_carrier_subset(sK46)) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_487,plain,
( element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46)))
| ~ one_sorted_str(sK46) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_651,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| element(X0,the_carrier(X1))
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(superposition,[status(thm)],[c_97,c_404]) ).
tcf(c_657,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_a_convergence_point_of_set(X1,filter_of_net_str(X1,X2),X0)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(global_subsumption_just,[status(thm)],[c_386,c_386,c_651]) ).
tcf(c_720,plain,
! [X0: $i] :
( empty(sK47)
| empty_carrier(X0)
| empty(cast_as_carrier_subset(sK46))
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0))) ),
inference(superposition,[status(thm)],[c_395,c_173]) ).
tcf(c_721,plain,
( empty(sK47)
| empty_carrier(sK46)
| empty(cast_as_carrier_subset(sK46))
| transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(sK46)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46))) ),
inference(instantiation,[status(thm)],[c_720]) ).
tcf(c_772,plain,
! [X0: $i] :
( empty(sK47)
| empty_carrier(X0)
| empty(cast_as_carrier_subset(sK46))
| net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47),X0)
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0))) ),
inference(superposition,[status(thm)],[c_395,c_102]) ).
tcf(c_773,plain,
( empty(sK47)
| empty_carrier(sK46)
| empty(cast_as_carrier_subset(sK46))
| net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| ~ one_sorted_str(sK46)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46))) ),
inference(instantiation,[status(thm)],[c_772]) ).
tcf(c_798,plain,
! [X0: $i] :
( empty(sK47)
| empty_carrier(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(superposition,[status(thm)],[c_395,c_171]) ).
tcf(c_799,plain,
( empty(sK47)
| empty_carrier(sK46)
| empty(cast_as_carrier_subset(sK46))
| ~ one_sorted_str(sK46)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46)))
| ~ empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)) ),
inference(instantiation,[status(thm)],[c_798]) ).
tcf(c_826,plain,
! [X0: $i] :
( empty(sK47)
| empty_carrier(X0)
| empty(cast_as_carrier_subset(sK46))
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) ),
inference(superposition,[status(thm)],[c_395,c_182]) ).
tcf(c_827,plain,
( empty(sK47)
| empty_carrier(sK46)
| empty(cast_as_carrier_subset(sK46))
| directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(sK46)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46)))
| ~ proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) ),
inference(instantiation,[status(thm)],[c_826]) ).
tcf(c_852,plain,
( empty(sK47)
| empty_carrier(sK46)
| ( filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)) = sK47 )
| ~ one_sorted_str(sK46)
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) ),
inference(superposition,[status(thm)],[c_394,c_387]) ).
tcf(c_1510,plain,
filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)) = sK47,
inference(global_subsumption_just,[status(thm)],[c_852,c_398,c_396,c_391,c_393,c_392,c_478,c_395,c_852]) ).
tcf(c_1512,plain,
! [X0: $i] :
( empty_carrier(sK46)
| empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ top_str(sK46)
| ~ topological_space(sK46)
| ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ element(X0,the_carrier(sK46))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46) ),
inference(superposition,[status(thm)],[c_1510,c_385]) ).
tcf(c_1514,plain,
! [X0: $i] :
( empty_carrier(sK46)
| is_a_convergence_point_of_set(sK46,sK47,X0)
| empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ top_str(sK46)
| ~ topological_space(sK46)
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
inference(superposition,[status(thm)],[c_1510,c_657]) ).
tcf(c_1776,plain,
! [X0: $i] :
( ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| is_a_convergence_point_of_set(sK46,sK47,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1514,c_398,c_397,c_396,c_391,c_393,c_392,c_478,c_394,c_483,c_487,c_721,c_773,c_799,c_827,c_1514]) ).
tcf(c_1777,plain,
! [X0: $i] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
inference(renaming,[status(thm)],[c_1776]) ).
tcf(c_1783,plain,
is_a_convergence_point_of_set(sK46,sK47,sK48),
inference(backward_subsumption_resolution,[status(thm)],[c_389,c_1777]) ).
tcf(c_1784,plain,
~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))),
inference(backward_subsumption_resolution,[status(thm)],[c_388,c_1777]) ).
tcf(c_1786,plain,
! [X0: $i] :
( in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ element(X0,the_carrier(sK46)) ),
inference(global_subsumption_just,[status(thm)],[c_1512,c_398,c_397,c_396,c_391,c_393,c_392,c_478,c_394,c_483,c_487,c_721,c_773,c_799,c_827,c_1512]) ).
tcf(c_2178,plain,
( ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ element(sK48,the_carrier(sK46)) ),
inference(superposition,[status(thm)],[c_1786,c_1784]) ).
tcf(c_2179,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_2178,c_1783,c_390]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU395+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.13/15.43 % Computer : n013.cluster.edu
% 0.13/15.43 % Model : x86_64 x86_64
% 0.13/15.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/15.43 % Memory : 8046.5625MB
% 0.13/15.43 % OS : Linux 6.8.0-71-generic
% 0.13/15.43 % CPULimit : 300
% 0.13/15.43 % WCLimit : 300
% 0.13/15.43 % DateTime : Thu Sep 24 13:58:16 UTC 2026
% 0.13/15.43 % CPUTime :
% 0.13/15.43 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/15.47 Running first-order theorem proving
% 0.13/15.47 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.13/15.48
% 0.13/15.48 % ======== iProver multi-core TPTP/SMT =========
% 0.13/15.48
% 0.13/15.48 % Detected problem language: tptp
% 0.13/15.49 % Proving...
% 3.55/16.26 % SZS status Started for theBenchmark.p
% 3.55/16.26 % SZS status Theorem for theBenchmark.p
% 3.55/16.26
% 3.55/16.26 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.55/16.26
% 3.55/16.26 % ------ iProver source info
% 3.55/16.26
% 3.55/16.26 % git: date: 2026-07-19 20:42:38 +0200
% 3.55/16.26 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.55/16.26 % git: non_committed_changes: false
% 3.55/16.26
% 3.55/16.26 % ------ Parsing...
% 3.55/16.26 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 3.55/16.26 % ------ Proving...
% 3.55/16.26 % ------ Problem Properties
% 3.55/16.26
% 3.55/16.26 %
% 3.55/16.26 % clauses 360
% 3.55/16.26 % conjectures 11
% 3.55/16.26 % EPR 131
% 3.55/16.26 % Horn 284
% 3.55/16.26 % unary 148
% 3.55/16.26 % binary 70
% 3.55/16.26 % lits 1010
% 3.55/16.26 % lits eq 21
% 3.55/16.26 % fd_pure 0
% 3.55/16.26 % fd_pseudo 0
% 3.55/16.26 % fd_cond 1
% 3.55/16.26 % fd_pseudo_cond 9
% 3.55/16.26 % AC symbols 0
% 3.55/16.26
% 3.55/16.26 % ------ Input Options Time Limit: Unbounded
% 3.55/16.26
% 3.55/16.26
% 3.55/16.26 % ------
% 3.55/16.26 % Current options:
% 3.55/16.26 % ------
% 3.55/16.26
% 3.55/16.26
% 3.55/16.26 %
% 3.55/16.26
% 3.55/16.26 % ------ Proving...
% 3.55/16.26 %
% 3.55/16.26
% 3.55/16.26 % SZS status Theorem for theBenchmark.p
% 3.55/16.26
% 3.55/16.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.55/16.26
% 3.55/16.26
%------------------------------------------------------------------------------