%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:29 PM UTC 2026
% Result : Theorem 0.20s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n004.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 06:18:04 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.20/0.43 % Drodi V4.1.1
% 0.20/0.54 % Refutation found
% 0.20/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.54 % SZS output start CNFRefutation for theBenchmark
% 0.20/0.54 fof(f7,axiom,(
% 0.20/0.54 (! [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,powerset(the_carrier(A)))=> ( C = lim_points_of_net(A,B)<=> (! [D] :( element(D,the_carrier(A))=> ( in(D,C)<=> (! [E] :( point_neighbourhood(E,A,D)=> is_eventually_in(A,B,E) ) )) ) )) ) )) )) )),
% 0.20/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.54 fof(f8,axiom,(
% 0.20/0.54 (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( element(C,the_carrier(A))=> ( is_a_cluster_point_of_netstr(A,B,C)<=> (! [D] :( point_neighbourhood(D,A,C)=> is_often_in(A,B,D) ) )) ) )) )) )),
% 0.20/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.54 fof(f9,axiom,(
% 0.20/0.54 (! [A,B] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A)& ~ empty_carrier(B)& transitive_relstr(B)& directed_relstr(B)& net_str(B,A) )=> element(lim_points_of_net(A,B),powerset(the_carrier(A))) ) )),
% 0.20/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.54 fof(f13,axiom,(
% 0.20/0.54 (! [A] :( top_str(A)=> one_sorted_str(A) ) )),
% 0.20/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.54 fof(f37,axiom,(
% 0.20/0.54 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& transitive_relstr(B)& directed_relstr(B)& net_str(B,A) )=> (! [C] :( is_eventually_in(A,B,C)=> is_often_in(A,B,C) ) )) )) )),
% 0.20/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.54 fof(f38,conjecture,(
% 0.20/0.54 (! [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_cluster_point_of_netstr(A,B,C) ) ) )) )) )),
% 0.20/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.54 fof(f39,negated_conjecture,(
% 0.20/0.54 ~((! [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_cluster_point_of_netstr(A,B,C) ) ) )) )) ))),
% 0.20/0.54 inference(negated_conjecture,[status(cth)],[f38])).
% 0.20/0.54 fof(f60,plain,(
% 0.20/0.54 ![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,powerset(the_carrier(A)))|(C=lim_points_of_net(A,B)<=>(![D]: (~element(D,the_carrier(A))|(in(D,C)<=>(![E]: (~point_neighbourhood(E,A,D)|is_eventually_in(A,B,E))))))))))))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.20/0.54 fof(f61,plain,(
% 0.20/0.54 ![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,powerset(the_carrier(A)))|((~C=lim_points_of_net(A,B)|(![D]: (~element(D,the_carrier(A))|((~in(D,C)|(![E]: (~point_neighbourhood(E,A,D)|is_eventually_in(A,B,E))))&(in(D,C)|(?[E]: (point_neighbourhood(E,A,D)&~is_eventually_in(A,B,E))))))))&(C=lim_points_of_net(A,B)|(?[D]: (element(D,the_carrier(A))&((~in(D,C)|(?[E]: (point_neighbourhood(E,A,D)&~is_eventually_in(A,B,E))))&(in(D,C)|(![E]: (~point_neighbourhood(E,A,D)|is_eventually_in(A,B,E))))))))))))))),
% 0.20/0.54 inference(NNF_transformation,[status(thm)],[f60])).
% 0.20/0.54 fof(f62,plain,(
% 0.20/0.54 ![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,powerset(the_carrier(A)))|((~C=lim_points_of_net(A,B)|(![D]: (~element(D,the_carrier(A))|((~in(D,C)|(![E]: (~point_neighbourhood(E,A,D)|is_eventually_in(A,B,E))))&(in(D,C)|(point_neighbourhood(sK0_skl(D,C,B,A),A,D)&~is_eventually_in(A,B,sK0_skl(D,C,B,A))))))))&(C=lim_points_of_net(A,B)|(element(sK1_skl(C,B,A),the_carrier(A))&((~in(sK1_skl(C,B,A),C)|(point_neighbourhood(sK2_skl(C,B,A),A,sK1_skl(C,B,A))&~is_eventually_in(A,B,sK2_skl(C,B,A))))&(in(sK1_skl(C,B,A),C)|(![E]: (~point_neighbourhood(E,A,sK1_skl(C,B,A))|is_eventually_in(A,B,E)))))))))))))),
% 0.20/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(E,sK0_skl(D,C,B,A)),skolemize(D,sK1_skl(C,B,A)),skolemize(E,sK2_skl(C,B,A))],[f61])).
% 0.20/0.54 fof(f63,plain,(
% 0.20/0.54 ![X0,X1,X2,X3,X4]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~transitive_relstr(X1)|~directed_relstr(X1)|~net_str(X1,X0)|~element(X2,powerset(the_carrier(X0)))|~X2=lim_points_of_net(X0,X1)|~element(X3,the_carrier(X0))|~in(X3,X2)|~point_neighbourhood(X4,X0,X3)|is_eventually_in(X0,X1,X4))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f62])).
% 0.20/0.54 fof(f70,plain,(
% 0.20/0.54 ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: (~element(C,the_carrier(A))|(is_a_cluster_point_of_netstr(A,B,C)<=>(![D]: (~point_neighbourhood(D,A,C)|is_often_in(A,B,D)))))))))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.20/0.54 fof(f71,plain,(
% 0.20/0.54 ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: (~element(C,the_carrier(A))|((~is_a_cluster_point_of_netstr(A,B,C)|(![D]: (~point_neighbourhood(D,A,C)|is_often_in(A,B,D))))&(is_a_cluster_point_of_netstr(A,B,C)|(?[D]: (point_neighbourhood(D,A,C)&~is_often_in(A,B,D))))))))))),
% 0.20/0.54 inference(NNF_transformation,[status(thm)],[f70])).
% 0.20/0.54 fof(f72,plain,(
% 0.20/0.54 ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|(![C]: (~element(C,the_carrier(A))|((~is_a_cluster_point_of_netstr(A,B,C)|(![D]: (~point_neighbourhood(D,A,C)|is_often_in(A,B,D))))&(is_a_cluster_point_of_netstr(A,B,C)|(point_neighbourhood(sK3_skl(C,B,A),A,C)&~is_often_in(A,B,sK3_skl(C,B,A))))))))))),
% 0.20/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(D,sK3_skl(C,B,A))],[f71])).
% 0.20/0.54 fof(f74,plain,(
% 0.20/0.54 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~element(X2,the_carrier(X0))|is_a_cluster_point_of_netstr(X0,X1,X2)|point_neighbourhood(sK3_skl(X2,X1,X0),X0,X2))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f72])).
% 0.20/0.54 fof(f75,plain,(
% 0.20/0.54 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~element(X2,the_carrier(X0))|is_a_cluster_point_of_netstr(X0,X1,X2)|~is_often_in(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f72])).
% 0.20/0.54 fof(f76,plain,(
% 0.20/0.54 ![A,B]: (((((((empty_carrier(A)|~topological_space(A))|~top_str(A))|empty_carrier(B))|~transitive_relstr(B))|~directed_relstr(B))|~net_str(B,A))|element(lim_points_of_net(A,B),powerset(the_carrier(A))))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.20/0.54 fof(f77,plain,(
% 0.20/0.54 ![X0,X1]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~transitive_relstr(X1)|~directed_relstr(X1)|~net_str(X1,X0)|element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f76])).
% 0.20/0.54 fof(f80,plain,(
% 0.20/0.54 ![A]: (~top_str(A)|one_sorted_str(A))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.20/0.54 fof(f81,plain,(
% 0.20/0.54 ![X0]: (~top_str(X0)|one_sorted_str(X0))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f80])).
% 0.20/0.54 fof(f136,plain,(
% 0.20/0.54 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((((empty_carrier(B)|~transitive_relstr(B))|~directed_relstr(B))|~net_str(B,A))|(![C]: (~is_eventually_in(A,B,C)|is_often_in(A,B,C))))))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.20/0.54 fof(f137,plain,(
% 0.20/0.54 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~transitive_relstr(X1)|~directed_relstr(X1)|~net_str(X1,X0)|~is_eventually_in(X0,X1,X2)|is_often_in(X0,X1,X2))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f136])).
% 0.20/0.54 fof(f138,plain,(
% 0.20/0.54 (?[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_cluster_point_of_netstr(A,B,C))))))))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.20/0.54 fof(f139,plain,(
% 0.20/0.54 (((~empty_carrier(sK17_skl)&topological_space(sK17_skl))&top_str(sK17_skl))&((((~empty_carrier(sK18_skl)&transitive_relstr(sK18_skl))&directed_relstr(sK18_skl))&net_str(sK18_skl,sK17_skl))&(element(sK19_skl,the_carrier(sK17_skl))&(in(sK19_skl,lim_points_of_net(sK17_skl,sK18_skl))&~is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,sK19_skl)))))),
% 0.20/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(A,sK17_skl),skolemize(B,sK18_skl),skolemize(C,sK19_skl)],[f138])).
% 0.20/0.54 fof(f140,plain,(
% 0.20/0.54 ~empty_carrier(sK17_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f141,plain,(
% 0.20/0.54 topological_space(sK17_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f142,plain,(
% 0.20/0.54 top_str(sK17_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f143,plain,(
% 0.20/0.54 ~empty_carrier(sK18_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f144,plain,(
% 0.20/0.54 transitive_relstr(sK18_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f145,plain,(
% 0.20/0.54 directed_relstr(sK18_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f146,plain,(
% 0.20/0.54 net_str(sK18_skl,sK17_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f147,plain,(
% 0.20/0.54 element(sK19_skl,the_carrier(sK17_skl))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f148,plain,(
% 0.20/0.54 in(sK19_skl,lim_points_of_net(sK17_skl,sK18_skl))),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f149,plain,(
% 0.20/0.54 ~is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,sK19_skl)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f139])).
% 0.20/0.54 fof(f170,plain,(
% 0.20/0.54 ![X0,X1,X2,X3]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|empty_carrier(X1)|~transitive_relstr(X1)|~directed_relstr(X1)|~net_str(X1,X0)|~element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))|~element(X2,the_carrier(X0))|~in(X2,lim_points_of_net(X0,X1))|~point_neighbourhood(X3,X0,X2)|is_eventually_in(X0,X1,X3))),
% 0.20/0.54 inference(destructive_equality_resolution,[status(thm)],[f63])).
% 0.20/0.54 fof(f175,plain,(
% 0.20/0.54 ![X0,X1,X2,X3]: (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))|~point_neighbourhood(X3,X0,X2)|is_eventually_in(X0,X1,X3))),
% 0.20/0.54 inference(backward_subsumption_resolution,[status(thm)],[f170,f77])).
% 0.20/0.54 fof(f180,definition,(
% 0.20/0.54 sQ0_spl <=> (empty_carrier(sK17_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f181,plain,(
% 0.20/0.54 empty_carrier(sK17_skl)|~sQ0_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f180])).
% 0.20/0.54 fof(f183,definition,(
% 0.20/0.54 sQ1_spl <=> (topological_space(sK17_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f185,plain,(
% 0.20/0.54 ~topological_space(sK17_skl)|sQ1_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f183])).
% 0.20/0.54 fof(f186,definition,(
% 0.20/0.54 sQ2_spl <=> (top_str(sK17_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f188,plain,(
% 0.20/0.54 ~top_str(sK17_skl)|sQ2_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f186])).
% 0.20/0.54 fof(f189,definition,(
% 0.20/0.54 sQ3_spl <=> (empty_carrier(sK18_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f190,plain,(
% 0.20/0.54 empty_carrier(sK18_skl)|~sQ3_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f189])).
% 0.20/0.54 fof(f192,definition,(
% 0.20/0.54 sQ4_spl <=> (transitive_relstr(sK18_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f194,plain,(
% 0.20/0.54 ~transitive_relstr(sK18_skl)|sQ4_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f192])).
% 0.20/0.54 fof(f195,definition,(
% 0.20/0.54 sQ5_spl <=> (directed_relstr(sK18_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f197,plain,(
% 0.20/0.54 ~directed_relstr(sK18_skl)|sQ5_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f195])).
% 0.20/0.54 fof(f223,plain,(
% 0.20/0.54 one_sorted_str(sK17_skl)),
% 0.20/0.54 inference(resolution,[status(thm)],[f81,f142])).
% 0.20/0.54 fof(f232,plain,(
% 0.20/0.54 $false|sQ5_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f197,f145])).
% 0.20/0.54 fof(f233,plain,(
% 0.20/0.54 sQ5_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f232])).
% 0.20/0.54 fof(f234,plain,(
% 0.20/0.54 $false|sQ4_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f194,f144])).
% 0.20/0.54 fof(f235,plain,(
% 0.20/0.54 sQ4_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f234])).
% 0.20/0.54 fof(f236,plain,(
% 0.20/0.54 $false|~sQ3_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f190,f143])).
% 0.20/0.54 fof(f237,plain,(
% 0.20/0.54 ~sQ3_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f236])).
% 0.20/0.54 fof(f238,plain,(
% 0.20/0.54 $false|sQ2_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f188,f142])).
% 0.20/0.54 fof(f239,plain,(
% 0.20/0.54 sQ2_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f238])).
% 0.20/0.54 fof(f240,plain,(
% 0.20/0.54 $false|sQ1_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f185,f141])).
% 0.20/0.54 fof(f241,plain,(
% 0.20/0.54 sQ1_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f240])).
% 0.20/0.54 fof(f242,plain,(
% 0.20/0.54 $false|~sQ0_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f181,f140])).
% 0.20/0.54 fof(f243,plain,(
% 0.20/0.54 ~sQ0_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f242])).
% 0.20/0.54 fof(f432,plain,(
% 0.20/0.54 ![X0]: (empty_carrier(sK17_skl)|~topological_space(sK17_skl)|~top_str(sK17_skl)|empty_carrier(sK18_skl)|~transitive_relstr(sK18_skl)|~directed_relstr(sK18_skl)|~net_str(sK18_skl,sK17_skl)|~element(sK19_skl,the_carrier(sK17_skl))|~point_neighbourhood(X0,sK17_skl,sK19_skl)|is_eventually_in(sK17_skl,sK18_skl,X0))),
% 0.20/0.54 inference(resolution,[status(thm)],[f175,f148])).
% 0.20/0.54 fof(f434,definition,(
% 0.20/0.54 sQ31_spl <=> (net_str(sK18_skl,sK17_skl))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f436,plain,(
% 0.20/0.54 ~net_str(sK18_skl,sK17_skl)|sQ31_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f434])).
% 0.20/0.54 fof(f437,definition,(
% 0.20/0.54 sQ32_spl <=> (element(sK19_skl,the_carrier(sK17_skl)))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f439,plain,(
% 0.20/0.54 ~element(sK19_skl,the_carrier(sK17_skl))|sQ32_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f437])).
% 0.20/0.54 fof(f440,definition,(
% 0.20/0.54 ![X0]: (sQ33_spl <=> (~point_neighbourhood(X0,sK17_skl,sK19_skl)|is_eventually_in(sK17_skl,sK18_skl,X0)))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f441,plain,(
% 0.20/0.54 ![X0]: (~point_neighbourhood(X0,sK17_skl,sK19_skl)|is_eventually_in(sK17_skl,sK18_skl,X0)|~sQ33_spl)),
% 0.20/0.54 inference(component_clause,[status(thm)],[f440])).
% 0.20/0.54 fof(f443,plain,(
% 0.20/0.54 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ31_spl|~sQ32_spl|sQ33_spl),
% 0.20/0.54 inference(split_clause,[status(thm)],[f432,f180,f183,f186,f189,f192,f195,f434,f437,f440])).
% 0.20/0.54 fof(f490,plain,(
% 0.20/0.54 ![X0]: (empty_carrier(sK17_skl)|~topological_space(sK17_skl)|~top_str(sK17_skl)|empty_carrier(sK18_skl)|~element(X0,the_carrier(sK17_skl))|is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,X0)|point_neighbourhood(sK3_skl(X0,sK18_skl,sK17_skl),sK17_skl,X0))),
% 0.20/0.54 inference(resolution,[status(thm)],[f74,f146])).
% 0.20/0.54 fof(f499,definition,(
% 0.20/0.54 ![X0]: (sQ46_spl <=> (~element(X0,the_carrier(sK17_skl))|is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,X0)|point_neighbourhood(sK3_skl(X0,sK18_skl,sK17_skl),sK17_skl,X0)))),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f500,plain,(
% 0.20/0.54 ![X0]: (~element(X0,the_carrier(sK17_skl))|is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,X0)|point_neighbourhood(sK3_skl(X0,sK18_skl,sK17_skl),sK17_skl,X0)|~sQ46_spl)),
% 0.20/0.54 inference(component_clause,[status(thm)],[f499])).
% 0.20/0.54 fof(f502,plain,(
% 0.20/0.54 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl|sQ46_spl),
% 0.20/0.54 inference(split_clause,[status(thm)],[f490,f180,f183,f186,f189,f499])).
% 0.20/0.54 fof(f602,plain,(
% 0.20/0.54 $false|sQ31_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f436,f146])).
% 0.20/0.54 fof(f603,plain,(
% 0.20/0.54 sQ31_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f602])).
% 0.20/0.54 fof(f606,plain,(
% 0.20/0.54 $false|sQ32_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f439,f147])).
% 0.20/0.54 fof(f607,plain,(
% 0.20/0.54 sQ32_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f606])).
% 0.20/0.54 fof(f802,definition,(
% 0.20/0.55 sQ104_spl <=> (one_sorted_str(sK17_skl))),
% 0.20/0.55 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.20/0.55 fof(f804,plain,(
% 0.20/0.55 ~one_sorted_str(sK17_skl)|sQ104_spl),
% 0.20/0.55 inference(component_clause,[status(thm)],[f802])).
% 0.20/0.55 fof(f813,plain,(
% 0.20/0.55 $false|sQ104_spl),
% 0.20/0.55 inference(forward_subsumption_resolution,[status(thm)],[f804,f223])).
% 0.20/0.55 fof(f814,plain,(
% 0.20/0.55 sQ104_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f813])).
% 0.20/0.55 fof(f841,plain,(
% 0.20/0.55 is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,sK19_skl)|point_neighbourhood(sK3_skl(sK19_skl,sK18_skl,sK17_skl),sK17_skl,sK19_skl)|~sQ46_spl),
% 0.20/0.55 inference(resolution,[status(thm)],[f500,f147])).
% 0.20/0.55 fof(f849,definition,(
% 0.20/0.55 sQ111_spl <=> (is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,sK19_skl))),
% 0.20/0.55 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.20/0.55 fof(f850,plain,(
% 0.20/0.55 is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,sK19_skl)|~sQ111_spl),
% 0.20/0.55 inference(component_clause,[status(thm)],[f849])).
% 0.20/0.55 fof(f852,definition,(
% 0.20/0.55 sQ112_spl <=> (point_neighbourhood(sK3_skl(sK19_skl,sK18_skl,sK17_skl),sK17_skl,sK19_skl))),
% 0.20/0.55 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.20/0.55 fof(f853,plain,(
% 0.20/0.55 point_neighbourhood(sK3_skl(sK19_skl,sK18_skl,sK17_skl),sK17_skl,sK19_skl)|~sQ112_spl),
% 0.20/0.55 inference(component_clause,[status(thm)],[f852])).
% 0.20/0.55 fof(f855,plain,(
% 0.20/0.55 sQ111_spl|sQ112_spl|~sQ46_spl),
% 0.20/0.55 inference(split_clause,[status(thm)],[f841,f849,f852,f499])).
% 0.20/0.55 fof(f856,plain,(
% 0.20/0.55 $false|~sQ111_spl),
% 0.20/0.55 inference(forward_subsumption_resolution,[status(thm)],[f850,f149])).
% 0.20/0.55 fof(f857,plain,(
% 0.20/0.55 ~sQ111_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f856])).
% 0.20/0.55 fof(f859,plain,(
% 0.20/0.55 is_eventually_in(sK17_skl,sK18_skl,sK3_skl(sK19_skl,sK18_skl,sK17_skl))|~sQ112_spl|~sQ33_spl),
% 0.20/0.55 inference(resolution,[status(thm)],[f853,f441])).
% 0.20/0.55 fof(f1283,plain,(
% 0.20/0.55 empty_carrier(sK17_skl)|~one_sorted_str(sK17_skl)|empty_carrier(sK18_skl)|~transitive_relstr(sK18_skl)|~directed_relstr(sK18_skl)|~net_str(sK18_skl,sK17_skl)|is_often_in(sK17_skl,sK18_skl,sK3_skl(sK19_skl,sK18_skl,sK17_skl))|~sQ112_spl|~sQ33_spl),
% 0.20/0.55 inference(resolution,[status(thm)],[f137,f859])).
% 0.20/0.55 fof(f1285,definition,(
% 0.20/0.55 sQ178_spl <=> (is_often_in(sK17_skl,sK18_skl,sK3_skl(sK19_skl,sK18_skl,sK17_skl)))),
% 0.20/0.55 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.20/0.55 fof(f1286,plain,(
% 0.20/0.55 is_often_in(sK17_skl,sK18_skl,sK3_skl(sK19_skl,sK18_skl,sK17_skl))|~sQ178_spl),
% 0.20/0.55 inference(component_clause,[status(thm)],[f1285])).
% 0.20/0.55 fof(f1288,plain,(
% 0.20/0.55 sQ0_spl|~sQ104_spl|sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ31_spl|sQ178_spl|~sQ112_spl|~sQ33_spl),
% 0.20/0.55 inference(split_clause,[status(thm)],[f1283,f180,f802,f189,f192,f195,f434,f1285,f852,f440])).
% 0.20/0.55 fof(f1293,plain,(
% 0.20/0.55 empty_carrier(sK17_skl)|~topological_space(sK17_skl)|~top_str(sK17_skl)|empty_carrier(sK18_skl)|~net_str(sK18_skl,sK17_skl)|~element(sK19_skl,the_carrier(sK17_skl))|is_a_cluster_point_of_netstr(sK17_skl,sK18_skl,sK19_skl)|~sQ178_spl),
% 0.20/0.55 inference(resolution,[status(thm)],[f1286,f75])).
% 0.20/0.55 fof(f1294,plain,(
% 0.20/0.55 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl|~sQ31_spl|~sQ32_spl|sQ111_spl|~sQ178_spl),
% 0.20/0.55 inference(split_clause,[status(thm)],[f1293,f180,f183,f186,f189,f434,f437,f849,f1285])).
% 0.20/0.55 fof(f1295,plain,(
% 0.20/0.55 $false),
% 0.20/0.55 inference(sat_refutation,[status(thm)],[f233,f235,f237,f239,f241,f243,f443,f502,f603,f607,f814,f855,f857,f1288,f1294])).
% 0.20/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.58 % Elapsed time: 0.143764 seconds
% 0.20/0.58 % CPU time: 0.731468 seconds
% 0.20/0.58 % Total memory used: 92.689 MB
% 0.20/0.58 % Net memory used: 92.201 MB
%------------------------------------------------------------------------------