%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Thu Sep 24 02:22:31 PM UTC 2026
% Result : Theorem 0.09s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:14:42 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.09/0.42 % Refutation found
% 0.09/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.42 fof(f34,axiom,(
% 0.09/0.42 (! [A] :( one_sorted_str(A)=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f37,axiom,(
% 0.09/0.42 (! [A,B,C] :( ( ~ empty_carrier(A)& one_sorted_str(A)& ~ empty(B)& element(B,powerset(the_carrier(A)))& ~ empty(C)& filtered_subset(C,boole_POSet(B))& upper_relstr_subset(C,boole_POSet(B))& element(C,powerset(the_carrier(boole_POSet(B)))) )=> ( ~ empty_carrier(net_of_bool_filter(A,B,C))& strict_net_str(net_of_bool_filter(A,B,C),A)& net_str(net_of_bool_filter(A,B,C),A) ) ) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f40,axiom,(
% 0.09/0.42 (! [A] :( top_str(A)=> one_sorted_str(A) ) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f63,axiom,(
% 0.09/0.42 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(cast_as_carrier_subset(A)) ) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f73,axiom,(
% 0.09/0.42 (! [A,B,C] :( ( ~ empty_carrier(A)& one_sorted_str(A)& ~ empty(B)& element(B,powerset(the_carrier(A)))& ~ empty(C)& filtered_subset(C,boole_POSet(B))& upper_relstr_subset(C,boole_POSet(B))& element(C,powerset(the_carrier(boole_POSet(B)))) )=> ( ~ empty_carrier(net_of_bool_filter(A,B,C))& reflexive_relstr(net_of_bool_filter(A,B,C))& transitive_relstr(net_of_bool_filter(A,B,C))& strict_net_str(net_of_bool_filter(A,B,C),A) ) ) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f76,axiom,(
% 0.09/0.42 (! [A,B,C] :( ( ~ empty_carrier(A)& one_sorted_str(A)& ~ empty(B)& element(B,powerset(the_carrier(A)))& ~ empty(C)& filtered_subset(C,boole_POSet(B))& upper_relstr_subset(C,boole_POSet(B))& proper_element(C,powerset(the_carrier(boole_POSet(B))))& element(C,powerset(the_carrier(boole_POSet(B)))) )=> ( ~ empty_carrier(net_of_bool_filter(A,B,C))& reflexive_relstr(net_of_bool_filter(A,B,C))& transitive_relstr(net_of_bool_filter(A,B,C))& strict_net_str(net_of_bool_filter(A,B,C),A)& directed_relstr(net_of_bool_filter(A,B,C)) ) ) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f125,axiom,(
% 0.09/0.42 (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& transitive_relstr(B)& directed_relstr(B)& net_str(B,A) )=> (! [C] :( element(C,the_carrier(A))=> ( in(C,lim_points_of_net(A,B))<=> is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C) ) ) )) )) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f126,axiom,(
% 0.09/0.42 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )=> B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) )) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f127,conjecture,(
% 0.09/0.42 (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )=> (! [C] :( element(C,the_carrier(A))=> ( in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))<=> is_a_convergence_point_of_set(A,B,C) ) ) )) )) )),
% 0.09/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f128,negated_conjecture,(
% 0.09/0.42 ~((! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )=> (! [C] :( element(C,the_carrier(A))=> ( in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))<=> is_a_convergence_point_of_set(A,B,C) ) ) )) )) ))),
% 0.09/0.42 inference(negated_conjecture,[status(cth)],[f127])).
% 0.09/0.42 fof(f248,plain,(
% 0.09/0.42 ![A]: (~one_sorted_str(A)|element(cast_as_carrier_subset(A),powerset(the_carrier(A))))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.09/0.42 fof(f249,plain,(
% 0.09/0.42 ![X0]: (~one_sorted_str(X0)|element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f248])).
% 0.09/0.42 fof(f252,plain,(
% 0.09/0.42 ![A,B,C]: ((((((((empty_carrier(A)|~one_sorted_str(A))|empty(B))|~element(B,powerset(the_carrier(A))))|empty(C))|~filtered_subset(C,boole_POSet(B)))|~upper_relstr_subset(C,boole_POSet(B)))|~element(C,powerset(the_carrier(boole_POSet(B)))))|((~empty_carrier(net_of_bool_filter(A,B,C))&strict_net_str(net_of_bool_filter(A,B,C),A))&net_str(net_of_bool_filter(A,B,C),A)))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.09/0.42 fof(f253,plain,(
% 0.09/0.42 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(X1)|~element(X1,powerset(the_carrier(X0)))|empty(X2)|~filtered_subset(X2,boole_POSet(X1))|~upper_relstr_subset(X2,boole_POSet(X1))|~element(X2,powerset(the_carrier(boole_POSet(X1))))|~empty_carrier(net_of_bool_filter(X0,X1,X2)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f252])).
% 0.09/0.42 fof(f255,plain,(
% 0.09/0.42 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(X1)|~element(X1,powerset(the_carrier(X0)))|empty(X2)|~filtered_subset(X2,boole_POSet(X1))|~upper_relstr_subset(X2,boole_POSet(X1))|~element(X2,powerset(the_carrier(boole_POSet(X1))))|net_str(net_of_bool_filter(X0,X1,X2),X0))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f252])).
% 0.09/0.42 fof(f261,plain,(
% 0.09/0.42 ![A]: (~top_str(A)|one_sorted_str(A))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.09/0.42 fof(f262,plain,(
% 0.09/0.42 ![X0]: (~top_str(X0)|one_sorted_str(X0))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f261])).
% 0.09/0.42 fof(f324,plain,(
% 0.09/0.42 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(cast_as_carrier_subset(A)))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.09/0.42 fof(f325,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(cast_as_carrier_subset(X0)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f324])).
% 0.09/0.42 fof(f369,plain,(
% 0.09/0.42 ![A,B,C]: ((((((((empty_carrier(A)|~one_sorted_str(A))|empty(B))|~element(B,powerset(the_carrier(A))))|empty(C))|~filtered_subset(C,boole_POSet(B)))|~upper_relstr_subset(C,boole_POSet(B)))|~element(C,powerset(the_carrier(boole_POSet(B)))))|(((~empty_carrier(net_of_bool_filter(A,B,C))&reflexive_relstr(net_of_bool_filter(A,B,C)))&transitive_relstr(net_of_bool_filter(A,B,C)))&strict_net_str(net_of_bool_filter(A,B,C),A)))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.09/0.42 fof(f372,plain,(
% 0.09/0.42 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(X1)|~element(X1,powerset(the_carrier(X0)))|empty(X2)|~filtered_subset(X2,boole_POSet(X1))|~upper_relstr_subset(X2,boole_POSet(X1))|~element(X2,powerset(the_carrier(boole_POSet(X1))))|transitive_relstr(net_of_bool_filter(X0,X1,X2)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f369])).
% 0.09/0.42 fof(f379,plain,(
% 0.09/0.42 ![A,B,C]: (((((((((empty_carrier(A)|~one_sorted_str(A))|empty(B))|~element(B,powerset(the_carrier(A))))|empty(C))|~filtered_subset(C,boole_POSet(B)))|~upper_relstr_subset(C,boole_POSet(B)))|~proper_element(C,powerset(the_carrier(boole_POSet(B)))))|~element(C,powerset(the_carrier(boole_POSet(B)))))|((((~empty_carrier(net_of_bool_filter(A,B,C))&reflexive_relstr(net_of_bool_filter(A,B,C)))&transitive_relstr(net_of_bool_filter(A,B,C)))&strict_net_str(net_of_bool_filter(A,B,C),A))&directed_relstr(net_of_bool_filter(A,B,C))))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 0.09/0.42 fof(f384,plain,(
% 0.09/0.42 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(X1)|~element(X1,powerset(the_carrier(X0)))|empty(X2)|~filtered_subset(X2,boole_POSet(X1))|~upper_relstr_subset(X2,boole_POSet(X1))|~proper_element(X2,powerset(the_carrier(boole_POSet(X1))))|~element(X2,powerset(the_carrier(boole_POSet(X1))))|directed_relstr(net_of_bool_filter(X0,X1,X2)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f379])).
% 0.09/0.42 fof(f691,plain,(
% 0.09/0.42 ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: ((((empty_carrier(B)|~transitive_relstr(B))|~directed_relstr(B))|~net_str(B,A))|(![C]: (~element(C,the_carrier(A))|(in(C,lim_points_of_net(A,B))<=>is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C)))))))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 0.09/0.42 fof(f692,plain,(
% 0.09/0.42 ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: ((((empty_carrier(B)|~transitive_relstr(B))|~directed_relstr(B))|~net_str(B,A))|(![C]: (~element(C,the_carrier(A))|((~in(C,lim_points_of_net(A,B))|is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C))&(in(C,lim_points_of_net(A,B))|~is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C))))))))),
% 0.09/0.42 inference(NNF_transformation,[status(thm)],[f691])).
% 0.09/0.42 fof(f693,plain,(
% 0.09/0.42 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~transitive_relstr(X1)|~directed_relstr(X1)|~net_str(X1,X0)|~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))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f692])).
% 0.09/0.42 fof(f694,plain,(
% 0.09/0.42 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~transitive_relstr(X1)|~directed_relstr(X1)|~net_str(X1,X0)|~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))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f692])).
% 0.09/0.42 fof(f695,plain,(
% 0.09/0.42 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: (((((empty(B)|~filtered_subset(B,boole_POSet(cast_as_carrier_subset(A))))|~upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A))))|~proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))|~element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))|B=filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f126])).
% 0.09/0.42 fof(f696,plain,(
% 0.09/0.42 ![X0,X1]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(X1)|~filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))|~upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))|~proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))|~element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))|X1=filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f695])).
% 0.09/0.42 fof(f697,plain,(
% 0.09/0.42 (?[A]: (((~empty_carrier(A)&topological_space(A))&top_str(A))&(?[B]: (((((~empty(B)&filtered_subset(B,boole_POSet(cast_as_carrier_subset(A))))&upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A))))&proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))&element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))&(?[C]: (element(C,the_carrier(A))&(in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))<~>is_a_convergence_point_of_set(A,B,C))))))))),
% 0.09/0.42 inference(pre_NNF_transformation,[status(thm)],[f128])).
% 0.09/0.42 fof(f698,plain,(
% 0.09/0.42 ?[A]: (((~empty_carrier(A)&topological_space(A))&top_str(A))&(?[B]: (((((~empty(B)&filtered_subset(B,boole_POSet(cast_as_carrier_subset(A))))&upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A))))&proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))&element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))&(?[C]: (element(C,the_carrier(A))&((in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))|is_a_convergence_point_of_set(A,B,C))&(~in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))|~is_a_convergence_point_of_set(A,B,C))))))))),
% 0.09/0.42 inference(NNF_transformation,[status(thm)],[f697])).
% 0.09/0.42 fof(f699,plain,(
% 0.09/0.42 (((~empty_carrier(sK45_skl)&topological_space(sK45_skl))&top_str(sK45_skl))&(((((~empty(sK46_skl)&filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))))&upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))))&proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))&element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))&(element(sK47_skl,the_carrier(sK45_skl))&((in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl))&(~in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|~is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl))))))),
% 0.09/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl,sK46_skl,sK47_skl]),skolemize(A,sK45_skl),skolemize(B,sK46_skl),skolemize(C,sK47_skl)],[f698])).
% 0.09/0.42 fof(f700,plain,(
% 0.09/0.42 ~empty_carrier(sK45_skl)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f701,plain,(
% 0.09/0.42 topological_space(sK45_skl)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f702,plain,(
% 0.09/0.42 top_str(sK45_skl)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f703,plain,(
% 0.09/0.42 ~empty(sK46_skl)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f704,plain,(
% 0.09/0.42 filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f705,plain,(
% 0.09/0.42 upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f706,plain,(
% 0.09/0.42 proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f707,plain,(
% 0.09/0.42 element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f708,plain,(
% 0.09/0.42 element(sK47_skl,the_carrier(sK45_skl))),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f709,plain,(
% 0.09/0.42 in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f710,plain,(
% 0.09/0.42 ~in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|~is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f699])).
% 0.09/0.42 fof(f753,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))|empty(sK46_skl)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl),X0))),
% 0.09/0.42 inference(resolution,[status(thm)],[f255,f704])).
% 0.09/0.42 fof(f754,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl),X0))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f753,f703])).
% 0.09/0.42 fof(f760,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl),X0))),
% 0.09/0.42 inference(resolution,[status(thm)],[f754,f707])).
% 0.09/0.42 fof(f761,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))|net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl),X0))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f760,f705])).
% 0.09/0.42 fof(f762,plain,(
% 0.09/0.42 empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f761,f249])).
% 0.09/0.42 fof(f763,plain,(
% 0.09/0.42 empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f762])).
% 0.09/0.42 fof(f764,plain,(
% 0.09/0.42 ~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f763,f700])).
% 0.09/0.42 fof(f795,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)|~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f764,f262])).
% 0.09/0.42 fof(f796,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f795,f702])).
% 0.09/0.42 fof(f817,plain,(
% 0.09/0.42 ![X0,X1]: (empty_carrier(sK45_skl)|~top_str(sK45_skl)|empty_carrier(X0)|~transitive_relstr(X0)|~directed_relstr(X0)|~net_str(X0,sK45_skl)|~element(X1,the_carrier(sK45_skl))|in(X1,lim_points_of_net(sK45_skl,X0))|~is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,X0),X1))),
% 0.09/0.42 inference(resolution,[status(thm)],[f694,f701])).
% 0.09/0.42 fof(f818,plain,(
% 0.09/0.42 ![X0,X1]: (~top_str(sK45_skl)|empty_carrier(X0)|~transitive_relstr(X0)|~directed_relstr(X0)|~net_str(X0,sK45_skl)|~element(X1,the_carrier(sK45_skl))|in(X1,lim_points_of_net(sK45_skl,X0))|~is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,X0),X1))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f817,f700])).
% 0.09/0.42 fof(f819,plain,(
% 0.09/0.42 ![X0,X1]: (empty_carrier(X0)|~transitive_relstr(X0)|~directed_relstr(X0)|~net_str(X0,sK45_skl)|~element(X1,the_carrier(sK45_skl))|in(X1,lim_points_of_net(sK45_skl,X0))|~is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,X0),X1))),
% 0.09/0.42 inference(resolution,[status(thm)],[f818,f702])).
% 0.09/0.42 fof(f821,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(X0)|~transitive_relstr(X0)|~directed_relstr(X0)|~net_str(X0,sK45_skl)|in(sK47_skl,lim_points_of_net(sK45_skl,X0))|~is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,X0),sK47_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f819,f708])).
% 0.09/0.42 fof(f823,plain,(
% 0.09/0.42 empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f696,f704])).
% 0.09/0.42 fof(f824,plain,(
% 0.09/0.42 ~one_sorted_str(sK45_skl)|empty(sK46_skl)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f823,f700])).
% 0.09/0.42 fof(f825,plain,(
% 0.09/0.42 empty(sK46_skl)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f824,f262])).
% 0.09/0.42 fof(f826,plain,(
% 0.09/0.42 ~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~top_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f825,f703])).
% 0.09/0.42 fof(f827,plain,(
% 0.09/0.42 ~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f826,f707])).
% 0.09/0.42 fof(f829,plain,(
% 0.09/0.42 ~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~top_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f827,f705])).
% 0.09/0.42 fof(f831,plain,(
% 0.09/0.42 ~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f829,f702])).
% 0.09/0.42 fof(f835,plain,(
% 0.09/0.42 sK46_skl=filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f831,f706])).
% 0.09/0.42 fof(f836,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)|in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|~is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)),
% 0.09/0.42 inference(paramodulation,[status(thm)],[f835,f821])).
% 0.09/0.42 fof(f837,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(sK45_skl)|~topological_space(sK45_skl)|~top_str(sK45_skl)|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0))),
% 0.09/0.42 inference(paramodulation,[status(thm)],[f835,f693])).
% 0.09/0.42 fof(f839,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)|~is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f836,f710])).
% 0.09/0.42 fof(f840,plain,(
% 0.09/0.42 ![X0]: (~topological_space(sK45_skl)|~top_str(sK45_skl)|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f837,f700])).
% 0.09/0.42 fof(f855,plain,(
% 0.09/0.42 ![X0]: (~topological_space(sK45_skl)|~top_str(sK45_skl)|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(resolution,[status(thm)],[f840,f796])).
% 0.09/0.42 fof(f857,plain,(
% 0.09/0.42 ![X0]: (~top_str(sK45_skl)|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f855,f701])).
% 0.09/0.42 fof(f858,plain,(
% 0.09/0.42 ![X0]: (~top_str(sK45_skl)|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f857,f372])).
% 0.09/0.42 fof(f859,plain,(
% 0.09/0.42 ![X0]: (~top_str(sK45_skl)|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f858])).
% 0.09/0.42 fof(f860,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f859,f702])).
% 0.09/0.42 fof(f885,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~one_sorted_str(sK45_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f860,f249])).
% 0.09/0.42 fof(f888,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f885])).
% 0.09/0.42 fof(f889,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f888,f325])).
% 0.09/0.42 fof(f898,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f889,f707])).
% 0.09/0.42 fof(f900,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f898,f700])).
% 0.09/0.42 fof(f911,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~top_str(sK45_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f900,f262])).
% 0.09/0.42 fof(f912,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~top_str(sK45_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f911,f703])).
% 0.09/0.42 fof(f913,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f912,f702])).
% 0.09/0.42 fof(f914,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f913,f704])).
% 0.09/0.42 fof(f915,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f914,f384])).
% 0.09/0.42 fof(f916,plain,(
% 0.09/0.42 ![X0]: (empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f915])).
% 0.09/0.42 fof(f917,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f916,f253])).
% 0.09/0.42 fof(f921,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f917,f707])).
% 0.09/0.42 fof(f926,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f921,f705])).
% 0.09/0.42 fof(f928,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty_carrier(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f926,f262])).
% 0.09/0.42 fof(f929,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f928,f700])).
% 0.09/0.42 fof(f930,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~one_sorted_str(sK45_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f929,f249])).
% 0.09/0.42 fof(f931,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~one_sorted_str(sK45_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f930,f703])).
% 0.09/0.42 fof(f933,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~top_str(sK45_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f931,f262])).
% 0.09/0.42 fof(f935,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl))),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f933])).
% 0.09/0.42 fof(f936,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f935,f704])).
% 0.09/0.42 fof(f938,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f936,f702])).
% 0.09/0.42 fof(f939,plain,(
% 0.09/0.42 ![X0]: (~element(X0,the_carrier(sK45_skl))|~in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)|empty(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f938,f706])).
% 0.09/0.42 fof(f940,plain,(
% 0.09/0.42 ~in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))|is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)|empty(cast_as_carrier_subset(sK45_skl))),
% 0.09/0.42 inference(resolution,[status(thm)],[f939,f708])).
% 0.09/0.42 fof(f941,plain,(
% 0.09/0.42 is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)|empty(cast_as_carrier_subset(sK45_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f940,f709])).
% 0.09/0.42 fof(f942,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f941,f839])).
% 0.09/0.42 fof(f945,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f942,f796])).
% 0.09/0.42 fof(f949,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f945,f372])).
% 0.09/0.42 fof(f950,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f949])).
% 0.09/0.42 fof(f951,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f950,f325])).
% 0.09/0.42 fof(f972,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(resolution,[status(thm)],[f951,f707])).
% 0.09/0.42 fof(f976,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~one_sorted_str(sK45_skl)|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f972,f700])).
% 0.09/0.42 fof(f978,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f976,f249])).
% 0.09/0.42 fof(f980,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~one_sorted_str(sK45_skl)|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f978])).
% 0.09/0.42 fof(f981,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~one_sorted_str(sK45_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f980,f703])).
% 0.09/0.42 fof(f982,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f981,f262])).
% 0.09/0.42 fof(f983,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~top_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f982,f704])).
% 0.09/0.42 fof(f984,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))),
% 0.09/0.42 inference(resolution,[status(thm)],[f983,f702])).
% 0.09/0.42 fof(f985,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|~directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f984,f705])).
% 0.09/0.42 fof(f986,plain,(
% 0.09/0.42 empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))|empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f985,f384])).
% 0.09/0.42 fof(f987,plain,(
% 0.09/0.42 empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f986,f253])).
% 0.09/0.42 fof(f988,plain,(
% 0.09/0.42 empty_carrier(sK45_skl)|empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f987,f262])).
% 0.09/0.42 fof(f989,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f988,f700])).
% 0.09/0.42 fof(f990,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|empty(sK46_skl)|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f989,f249])).
% 0.09/0.42 fof(f991,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f990,f703])).
% 0.09/0.42 fof(f992,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f991,f707])).
% 0.09/0.42 fof(f995,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f992,f704])).
% 0.09/0.42 fof(f1000,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)|~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f995,f262])).
% 0.09/0.42 fof(f1002,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f1000])).
% 0.09/0.42 fof(f1003,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))|~top_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1002,f705])).
% 0.09/0.42 fof(f1005,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))|~proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))),
% 0.09/0.42 inference(resolution,[status(thm)],[f1003,f702])).
% 0.09/0.42 fof(f1006,plain,(
% 0.09/0.42 empty(cast_as_carrier_subset(sK45_skl))),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1005,f706])).
% 0.09/0.42 fof(f1008,plain,(
% 0.09/0.42 empty_carrier(sK45_skl)|~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f1006,f325])).
% 0.09/0.42 fof(f1019,plain,(
% 0.09/0.42 ~one_sorted_str(sK45_skl)),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1008,f700])).
% 0.09/0.42 fof(f1067,plain,(
% 0.09/0.42 ~top_str(sK45_skl)),
% 0.09/0.42 inference(resolution,[status(thm)],[f1019,f262])).
% 0.09/0.42 fof(f1068,plain,(
% 0.09/0.42 $false),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1067,f702])).
% 0.09/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.44 % Elapsed time: 0.068838 seconds
% 0.09/0.44 % CPU time: 0.286703 seconds
% 0.09/0.44 % Total memory used: 68.232 MB
% 0.09/0.44 % Net memory used: 68.018 MB
%------------------------------------------------------------------------------