%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU386+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 04:29:29 EST 2010
% Result : Theorem 1.00s
% Output : Solution 1.00s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP31676/SEU386+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP31676/SEU386+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP31676/SEU386+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 31772
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.018 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(5, axiom,![X1]:![X2]:(((((((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))&~(empty_carrier(X2)))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>element(lim_points_of_net(X1,X2),powerset(the_carrier(X1)))),file('/tmp/SRASS.s.p', dt_k11_yellow_6)).
% fof(7, axiom,![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((~(empty_carrier(X2))&net_str(X2,X1))=>![X3]:(element(X3,the_carrier(X1))=>(is_a_cluster_point_of_netstr(X1,X2,X3)<=>![X4]:(point_neighbourhood(X4,X1,X3)=>is_often_in(X1,X2,X4)))))),file('/tmp/SRASS.s.p', d9_waybel_9)).
% fof(8, axiom,![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(element(X3,powerset(the_carrier(X1)))=>(X3=lim_points_of_net(X1,X2)<=>![X4]:(element(X4,the_carrier(X1))=>(in(X4,X3)<=>![X5]:(point_neighbourhood(X5,X1,X4)=>is_eventually_in(X1,X2,X5)))))))),file('/tmp/SRASS.s.p', d18_yellow_6)).
% fof(11, axiom,![X1]:![X2]:![X3]:((in(X1,X2)&element(X2,powerset(X3)))=>element(X1,X3)),file('/tmp/SRASS.s.p', t4_subset)).
% fof(12, axiom,![X1]:((~(empty_carrier(X1))&one_sorted_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(is_eventually_in(X1,X2,X3)=>is_often_in(X1,X2,X3)))),file('/tmp/SRASS.s.p', t28_yellow_6)).
% fof(17, axiom,![X1]:(top_str(X1)=>one_sorted_str(X1)),file('/tmp/SRASS.s.p', dt_l1_pre_topc)).
% fof(45, conjecture,![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(element(X3,the_carrier(X1))=>(in(X3,lim_points_of_net(X1,X2))=>is_a_cluster_point_of_netstr(X1,X2,X3))))),file('/tmp/SRASS.s.p', t29_waybel_9)).
% fof(46, negated_conjecture,~(![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(element(X3,the_carrier(X1))=>(in(X3,lim_points_of_net(X1,X2))=>is_a_cluster_point_of_netstr(X1,X2,X3)))))),inference(assume_negation,[status(cth)],[45])).
% fof(48, plain,![X1]:![X2]:(((((((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))&~(empty_carrier(X2)))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>element(lim_points_of_net(X1,X2),powerset(the_carrier(X1)))),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(50, plain,![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((~(empty_carrier(X2))&net_str(X2,X1))=>![X3]:(element(X3,the_carrier(X1))=>(is_a_cluster_point_of_netstr(X1,X2,X3)<=>![X4]:(point_neighbourhood(X4,X1,X3)=>is_often_in(X1,X2,X4)))))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(51, plain,![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(element(X3,powerset(the_carrier(X1)))=>(X3=lim_points_of_net(X1,X2)<=>![X4]:(element(X4,the_carrier(X1))=>(in(X4,X3)<=>![X5]:(point_neighbourhood(X5,X1,X4)=>is_eventually_in(X1,X2,X5)))))))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(53, plain,![X1]:((~(empty_carrier(X1))&one_sorted_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(is_eventually_in(X1,X2,X3)=>is_often_in(X1,X2,X3)))),inference(fof_simplification,[status(thm)],[12,theory(equality)])).
% fof(62, negated_conjecture,~(![X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))=>![X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))=>![X3]:(element(X3,the_carrier(X1))=>(in(X3,lim_points_of_net(X1,X2))=>is_a_cluster_point_of_netstr(X1,X2,X3)))))),inference(fof_simplification,[status(thm)],[46,theory(equality)])).
% fof(75, plain,![X1]:![X2]:(((((((empty_carrier(X1)|~(topological_space(X1)))|~(top_str(X1)))|empty_carrier(X2))|~(transitive_relstr(X2)))|~(directed_relstr(X2)))|~(net_str(X2,X1)))|element(lim_points_of_net(X1,X2),powerset(the_carrier(X1)))),inference(fof_nnf,[status(thm)],[48])).
% fof(76, plain,![X3]:![X4]:(((((((empty_carrier(X3)|~(topological_space(X3)))|~(top_str(X3)))|empty_carrier(X4))|~(transitive_relstr(X4)))|~(directed_relstr(X4)))|~(net_str(X4,X3)))|element(lim_points_of_net(X3,X4),powerset(the_carrier(X3)))),inference(variable_rename,[status(thm)],[75])).
% cnf(77,plain,(element(lim_points_of_net(X1,X2),powerset(the_carrier(X1)))|empty_carrier(X2)|empty_carrier(X1)|~net_str(X2,X1)|~directed_relstr(X2)|~transitive_relstr(X2)|~top_str(X1)|~topological_space(X1)),inference(split_conjunct,[status(thm)],[76])).
% fof(82, plain,![X1]:(((empty_carrier(X1)|~(topological_space(X1)))|~(top_str(X1)))|![X2]:((empty_carrier(X2)|~(net_str(X2,X1)))|![X3]:(~(element(X3,the_carrier(X1)))|((~(is_a_cluster_point_of_netstr(X1,X2,X3))|![X4]:(~(point_neighbourhood(X4,X1,X3))|is_often_in(X1,X2,X4)))&(?[X4]:(point_neighbourhood(X4,X1,X3)&~(is_often_in(X1,X2,X4)))|is_a_cluster_point_of_netstr(X1,X2,X3)))))),inference(fof_nnf,[status(thm)],[50])).
% fof(83, plain,![X5]:(((empty_carrier(X5)|~(topological_space(X5)))|~(top_str(X5)))|![X6]:((empty_carrier(X6)|~(net_str(X6,X5)))|![X7]:(~(element(X7,the_carrier(X5)))|((~(is_a_cluster_point_of_netstr(X5,X6,X7))|![X8]:(~(point_neighbourhood(X8,X5,X7))|is_often_in(X5,X6,X8)))&(?[X9]:(point_neighbourhood(X9,X5,X7)&~(is_often_in(X5,X6,X9)))|is_a_cluster_point_of_netstr(X5,X6,X7)))))),inference(variable_rename,[status(thm)],[82])).
% fof(84, plain,![X5]:(((empty_carrier(X5)|~(topological_space(X5)))|~(top_str(X5)))|![X6]:((empty_carrier(X6)|~(net_str(X6,X5)))|![X7]:(~(element(X7,the_carrier(X5)))|((~(is_a_cluster_point_of_netstr(X5,X6,X7))|![X8]:(~(point_neighbourhood(X8,X5,X7))|is_often_in(X5,X6,X8)))&((point_neighbourhood(esk4_3(X5,X6,X7),X5,X7)&~(is_often_in(X5,X6,esk4_3(X5,X6,X7))))|is_a_cluster_point_of_netstr(X5,X6,X7)))))),inference(skolemize,[status(esa)],[83])).
% fof(85, plain,![X5]:![X6]:![X7]:![X8]:((((((~(point_neighbourhood(X8,X5,X7))|is_often_in(X5,X6,X8))|~(is_a_cluster_point_of_netstr(X5,X6,X7)))&((point_neighbourhood(esk4_3(X5,X6,X7),X5,X7)&~(is_often_in(X5,X6,esk4_3(X5,X6,X7))))|is_a_cluster_point_of_netstr(X5,X6,X7)))|~(element(X7,the_carrier(X5))))|(empty_carrier(X6)|~(net_str(X6,X5))))|((empty_carrier(X5)|~(topological_space(X5)))|~(top_str(X5)))),inference(shift_quantors,[status(thm)],[84])).
% fof(86, plain,![X5]:![X6]:![X7]:![X8]:((((((~(point_neighbourhood(X8,X5,X7))|is_often_in(X5,X6,X8))|~(is_a_cluster_point_of_netstr(X5,X6,X7)))|~(element(X7,the_carrier(X5))))|(empty_carrier(X6)|~(net_str(X6,X5))))|((empty_carrier(X5)|~(topological_space(X5)))|~(top_str(X5))))&(((((point_neighbourhood(esk4_3(X5,X6,X7),X5,X7)|is_a_cluster_point_of_netstr(X5,X6,X7))|~(element(X7,the_carrier(X5))))|(empty_carrier(X6)|~(net_str(X6,X5))))|((empty_carrier(X5)|~(topological_space(X5)))|~(top_str(X5))))&((((~(is_often_in(X5,X6,esk4_3(X5,X6,X7)))|is_a_cluster_point_of_netstr(X5,X6,X7))|~(element(X7,the_carrier(X5))))|(empty_carrier(X6)|~(net_str(X6,X5))))|((empty_carrier(X5)|~(topological_space(X5)))|~(top_str(X5)))))),inference(distribute,[status(thm)],[85])).
% cnf(87,plain,(empty_carrier(X1)|empty_carrier(X2)|is_a_cluster_point_of_netstr(X1,X2,X3)|~top_str(X1)|~topological_space(X1)|~net_str(X2,X1)|~element(X3,the_carrier(X1))|~is_often_in(X1,X2,esk4_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[86])).
% cnf(88,plain,(empty_carrier(X1)|empty_carrier(X2)|is_a_cluster_point_of_netstr(X1,X2,X3)|point_neighbourhood(esk4_3(X1,X2,X3),X1,X3)|~top_str(X1)|~topological_space(X1)|~net_str(X2,X1)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[86])).
% fof(90, plain,![X1]:(((empty_carrier(X1)|~(topological_space(X1)))|~(top_str(X1)))|![X2]:((((empty_carrier(X2)|~(transitive_relstr(X2)))|~(directed_relstr(X2)))|~(net_str(X2,X1)))|![X3]:(~(element(X3,powerset(the_carrier(X1))))|((~(X3=lim_points_of_net(X1,X2))|![X4]:(~(element(X4,the_carrier(X1)))|((~(in(X4,X3))|![X5]:(~(point_neighbourhood(X5,X1,X4))|is_eventually_in(X1,X2,X5)))&(?[X5]:(point_neighbourhood(X5,X1,X4)&~(is_eventually_in(X1,X2,X5)))|in(X4,X3)))))&(?[X4]:(element(X4,the_carrier(X1))&((~(in(X4,X3))|?[X5]:(point_neighbourhood(X5,X1,X4)&~(is_eventually_in(X1,X2,X5))))&(in(X4,X3)|![X5]:(~(point_neighbourhood(X5,X1,X4))|is_eventually_in(X1,X2,X5)))))|X3=lim_points_of_net(X1,X2)))))),inference(fof_nnf,[status(thm)],[51])).
% fof(91, plain,![X6]:(((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6)))|![X7]:((((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6)))|![X8]:(~(element(X8,powerset(the_carrier(X6))))|((~(X8=lim_points_of_net(X6,X7))|![X9]:(~(element(X9,the_carrier(X6)))|((~(in(X9,X8))|![X10]:(~(point_neighbourhood(X10,X6,X9))|is_eventually_in(X6,X7,X10)))&(?[X11]:(point_neighbourhood(X11,X6,X9)&~(is_eventually_in(X6,X7,X11)))|in(X9,X8)))))&(?[X12]:(element(X12,the_carrier(X6))&((~(in(X12,X8))|?[X13]:(point_neighbourhood(X13,X6,X12)&~(is_eventually_in(X6,X7,X13))))&(in(X12,X8)|![X14]:(~(point_neighbourhood(X14,X6,X12))|is_eventually_in(X6,X7,X14)))))|X8=lim_points_of_net(X6,X7)))))),inference(variable_rename,[status(thm)],[90])).
% fof(92, plain,![X6]:(((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6)))|![X7]:((((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6)))|![X8]:(~(element(X8,powerset(the_carrier(X6))))|((~(X8=lim_points_of_net(X6,X7))|![X9]:(~(element(X9,the_carrier(X6)))|((~(in(X9,X8))|![X10]:(~(point_neighbourhood(X10,X6,X9))|is_eventually_in(X6,X7,X10)))&((point_neighbourhood(esk5_4(X6,X7,X8,X9),X6,X9)&~(is_eventually_in(X6,X7,esk5_4(X6,X7,X8,X9))))|in(X9,X8)))))&((element(esk6_3(X6,X7,X8),the_carrier(X6))&((~(in(esk6_3(X6,X7,X8),X8))|(point_neighbourhood(esk7_3(X6,X7,X8),X6,esk6_3(X6,X7,X8))&~(is_eventually_in(X6,X7,esk7_3(X6,X7,X8)))))&(in(esk6_3(X6,X7,X8),X8)|![X14]:(~(point_neighbourhood(X14,X6,esk6_3(X6,X7,X8)))|is_eventually_in(X6,X7,X14)))))|X8=lim_points_of_net(X6,X7)))))),inference(skolemize,[status(esa)],[91])).
% fof(93, plain,![X6]:![X7]:![X8]:![X9]:![X10]:![X14]:(((((((((~(point_neighbourhood(X14,X6,esk6_3(X6,X7,X8)))|is_eventually_in(X6,X7,X14))|in(esk6_3(X6,X7,X8),X8))&(~(in(esk6_3(X6,X7,X8),X8))|(point_neighbourhood(esk7_3(X6,X7,X8),X6,esk6_3(X6,X7,X8))&~(is_eventually_in(X6,X7,esk7_3(X6,X7,X8))))))&element(esk6_3(X6,X7,X8),the_carrier(X6)))|X8=lim_points_of_net(X6,X7))&(((((~(point_neighbourhood(X10,X6,X9))|is_eventually_in(X6,X7,X10))|~(in(X9,X8)))&((point_neighbourhood(esk5_4(X6,X7,X8,X9),X6,X9)&~(is_eventually_in(X6,X7,esk5_4(X6,X7,X8,X9))))|in(X9,X8)))|~(element(X9,the_carrier(X6))))|~(X8=lim_points_of_net(X6,X7))))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6)))),inference(shift_quantors,[status(thm)],[92])).
% fof(94, plain,![X6]:![X7]:![X8]:![X9]:![X10]:![X14]:(((((((((~(point_neighbourhood(X14,X6,esk6_3(X6,X7,X8)))|is_eventually_in(X6,X7,X14))|in(esk6_3(X6,X7,X8),X8))|X8=lim_points_of_net(X6,X7))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6))))&((((((point_neighbourhood(esk7_3(X6,X7,X8),X6,esk6_3(X6,X7,X8))|~(in(esk6_3(X6,X7,X8),X8)))|X8=lim_points_of_net(X6,X7))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6))))&(((((~(is_eventually_in(X6,X7,esk7_3(X6,X7,X8)))|~(in(esk6_3(X6,X7,X8),X8)))|X8=lim_points_of_net(X6,X7))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6))))))&((((element(esk6_3(X6,X7,X8),the_carrier(X6))|X8=lim_points_of_net(X6,X7))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6)))))&((((((((~(point_neighbourhood(X10,X6,X9))|is_eventually_in(X6,X7,X10))|~(in(X9,X8)))|~(element(X9,the_carrier(X6))))|~(X8=lim_points_of_net(X6,X7)))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6))))&(((((((point_neighbourhood(esk5_4(X6,X7,X8,X9),X6,X9)|in(X9,X8))|~(element(X9,the_carrier(X6))))|~(X8=lim_points_of_net(X6,X7)))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6))))&((((((~(is_eventually_in(X6,X7,esk5_4(X6,X7,X8,X9)))|in(X9,X8))|~(element(X9,the_carrier(X6))))|~(X8=lim_points_of_net(X6,X7)))|~(element(X8,powerset(the_carrier(X6)))))|(((empty_carrier(X7)|~(transitive_relstr(X7)))|~(directed_relstr(X7)))|~(net_str(X7,X6))))|((empty_carrier(X6)|~(topological_space(X6)))|~(top_str(X6))))))),inference(distribute,[status(thm)],[93])).
% cnf(97,plain,(empty_carrier(X1)|empty_carrier(X2)|is_eventually_in(X1,X2,X5)|~top_str(X1)|~topological_space(X1)|~net_str(X2,X1)|~directed_relstr(X2)|~transitive_relstr(X2)|~element(X3,powerset(the_carrier(X1)))|X3!=lim_points_of_net(X1,X2)|~element(X4,the_carrier(X1))|~in(X4,X3)|~point_neighbourhood(X5,X1,X4)),inference(split_conjunct,[status(thm)],[94])).
% fof(109, plain,![X1]:![X2]:![X3]:((~(in(X1,X2))|~(element(X2,powerset(X3))))|element(X1,X3)),inference(fof_nnf,[status(thm)],[11])).
% fof(110, plain,![X4]:![X5]:![X6]:((~(in(X4,X5))|~(element(X5,powerset(X6))))|element(X4,X6)),inference(variable_rename,[status(thm)],[109])).
% cnf(111,plain,(element(X1,X2)|~element(X3,powerset(X2))|~in(X1,X3)),inference(split_conjunct,[status(thm)],[110])).
% fof(112, plain,![X1]:((empty_carrier(X1)|~(one_sorted_str(X1)))|![X2]:((((empty_carrier(X2)|~(transitive_relstr(X2)))|~(directed_relstr(X2)))|~(net_str(X2,X1)))|![X3]:(~(is_eventually_in(X1,X2,X3))|is_often_in(X1,X2,X3)))),inference(fof_nnf,[status(thm)],[53])).
% fof(113, plain,![X4]:((empty_carrier(X4)|~(one_sorted_str(X4)))|![X5]:((((empty_carrier(X5)|~(transitive_relstr(X5)))|~(directed_relstr(X5)))|~(net_str(X5,X4)))|![X6]:(~(is_eventually_in(X4,X5,X6))|is_often_in(X4,X5,X6)))),inference(variable_rename,[status(thm)],[112])).
% fof(114, plain,![X4]:![X5]:![X6]:(((~(is_eventually_in(X4,X5,X6))|is_often_in(X4,X5,X6))|(((empty_carrier(X5)|~(transitive_relstr(X5)))|~(directed_relstr(X5)))|~(net_str(X5,X4))))|(empty_carrier(X4)|~(one_sorted_str(X4)))),inference(shift_quantors,[status(thm)],[113])).
% cnf(115,plain,(empty_carrier(X1)|empty_carrier(X2)|is_often_in(X1,X2,X3)|~one_sorted_str(X1)|~net_str(X2,X1)|~directed_relstr(X2)|~transitive_relstr(X2)|~is_eventually_in(X1,X2,X3)),inference(split_conjunct,[status(thm)],[114])).
% fof(129, plain,![X1]:(~(top_str(X1))|one_sorted_str(X1)),inference(fof_nnf,[status(thm)],[17])).
% fof(130, plain,![X2]:(~(top_str(X2))|one_sorted_str(X2)),inference(variable_rename,[status(thm)],[129])).
% cnf(131,plain,(one_sorted_str(X1)|~top_str(X1)),inference(split_conjunct,[status(thm)],[130])).
% fof(220, negated_conjecture,?[X1]:(((~(empty_carrier(X1))&topological_space(X1))&top_str(X1))&?[X2]:((((~(empty_carrier(X2))&transitive_relstr(X2))&directed_relstr(X2))&net_str(X2,X1))&?[X3]:(element(X3,the_carrier(X1))&(in(X3,lim_points_of_net(X1,X2))&~(is_a_cluster_point_of_netstr(X1,X2,X3)))))),inference(fof_nnf,[status(thm)],[62])).
% fof(221, negated_conjecture,?[X4]:(((~(empty_carrier(X4))&topological_space(X4))&top_str(X4))&?[X5]:((((~(empty_carrier(X5))&transitive_relstr(X5))&directed_relstr(X5))&net_str(X5,X4))&?[X6]:(element(X6,the_carrier(X4))&(in(X6,lim_points_of_net(X4,X5))&~(is_a_cluster_point_of_netstr(X4,X5,X6)))))),inference(variable_rename,[status(thm)],[220])).
% fof(222, negated_conjecture,(((~(empty_carrier(esk18_0))&topological_space(esk18_0))&top_str(esk18_0))&((((~(empty_carrier(esk19_0))&transitive_relstr(esk19_0))&directed_relstr(esk19_0))&net_str(esk19_0,esk18_0))&(element(esk20_0,the_carrier(esk18_0))&(in(esk20_0,lim_points_of_net(esk18_0,esk19_0))&~(is_a_cluster_point_of_netstr(esk18_0,esk19_0,esk20_0)))))),inference(skolemize,[status(esa)],[221])).
% cnf(223,negated_conjecture,(~is_a_cluster_point_of_netstr(esk18_0,esk19_0,esk20_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(224,negated_conjecture,(in(esk20_0,lim_points_of_net(esk18_0,esk19_0))),inference(split_conjunct,[status(thm)],[222])).
% cnf(225,negated_conjecture,(element(esk20_0,the_carrier(esk18_0))),inference(split_conjunct,[status(thm)],[222])).
% cnf(226,negated_conjecture,(net_str(esk19_0,esk18_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(227,negated_conjecture,(directed_relstr(esk19_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(228,negated_conjecture,(transitive_relstr(esk19_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(229,negated_conjecture,(~empty_carrier(esk19_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(230,negated_conjecture,(top_str(esk18_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(231,negated_conjecture,(topological_space(esk18_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(232,negated_conjecture,(~empty_carrier(esk18_0)),inference(split_conjunct,[status(thm)],[222])).
% cnf(233,plain,(is_eventually_in(X1,X2,X5)|empty_carrier(X2)|empty_carrier(X1)|lim_points_of_net(X1,X2)!=X3|~point_neighbourhood(X5,X1,X4)|~net_str(X2,X1)|~directed_relstr(X2)|~transitive_relstr(X2)|~topological_space(X1)|~element(X3,powerset(the_carrier(X1)))|~top_str(X1)|~in(X4,X3)),inference(csr,[status(thm)],[97,111])).
% cnf(273,plain,(is_a_cluster_point_of_netstr(X1,X2,X3)|empty_carrier(X2)|empty_carrier(X1)|~net_str(X2,X1)|~topological_space(X1)|~element(X3,the_carrier(X1))|~top_str(X1)|~one_sorted_str(X1)|~is_eventually_in(X1,X2,esk4_3(X1,X2,X3))|~directed_relstr(X2)|~transitive_relstr(X2)),inference(spm,[status(thm)],[87,115,theory(equality)])).
% cnf(279,plain,(is_eventually_in(X1,X2,X3)|empty_carrier(X2)|empty_carrier(X1)|empty_carrier(X4)|lim_points_of_net(X1,X2)!=lim_points_of_net(X1,X4)|~point_neighbourhood(X3,X1,X5)|~net_str(X2,X1)|~directed_relstr(X2)|~transitive_relstr(X2)|~topological_space(X1)|~top_str(X1)|~in(X5,lim_points_of_net(X1,X4))|~net_str(X4,X1)|~directed_relstr(X4)|~transitive_relstr(X4)),inference(spm,[status(thm)],[233,77,theory(equality)])).
% cnf(420,plain,(is_a_cluster_point_of_netstr(X1,X2,X3)|empty_carrier(X2)|empty_carrier(X1)|~is_eventually_in(X1,X2,esk4_3(X1,X2,X3))|~net_str(X2,X1)|~directed_relstr(X2)|~transitive_relstr(X2)|~topological_space(X1)|~element(X3,the_carrier(X1))|~top_str(X1)),inference(csr,[status(thm)],[273,131])).
% cnf(630,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|~net_str(esk19_0,esk18_0)|~directed_relstr(X1)|~directed_relstr(esk19_0)|~transitive_relstr(X1)|~transitive_relstr(esk19_0)|~topological_space(esk18_0)|~top_str(esk18_0)),inference(spm,[status(thm)],[279,224,theory(equality)])).
% cnf(632,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|$false|~directed_relstr(X1)|~directed_relstr(esk19_0)|~transitive_relstr(X1)|~transitive_relstr(esk19_0)|~topological_space(esk18_0)|~top_str(esk18_0)),inference(rw,[status(thm)],[630,226,theory(equality)])).
% cnf(633,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|$false|~directed_relstr(X1)|$false|~transitive_relstr(X1)|~transitive_relstr(esk19_0)|~topological_space(esk18_0)|~top_str(esk18_0)),inference(rw,[status(thm)],[632,227,theory(equality)])).
% cnf(634,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|$false|~directed_relstr(X1)|$false|~transitive_relstr(X1)|$false|~topological_space(esk18_0)|~top_str(esk18_0)),inference(rw,[status(thm)],[633,228,theory(equality)])).
% cnf(635,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|$false|~directed_relstr(X1)|$false|~transitive_relstr(X1)|$false|$false|~top_str(esk18_0)),inference(rw,[status(thm)],[634,231,theory(equality)])).
% cnf(636,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|$false|~directed_relstr(X1)|$false|~transitive_relstr(X1)|$false|$false|$false),inference(rw,[status(thm)],[635,230,theory(equality)])).
% cnf(637,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk19_0)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)),inference(cn,[status(thm)],[636,theory(equality)])).
% cnf(638,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(esk18_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)),inference(sr,[status(thm)],[637,229,theory(equality)])).
% cnf(639,negated_conjecture,(is_eventually_in(esk18_0,X1,X2)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(X2,esk18_0,esk20_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)),inference(sr,[status(thm)],[638,232,theory(equality)])).
% cnf(643,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,X2)|empty_carrier(esk18_0)|empty_carrier(X1)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|~topological_space(esk18_0)|~element(X2,the_carrier(esk18_0))|~top_str(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(esk4_3(esk18_0,X1,X2),esk18_0,esk20_0)),inference(spm,[status(thm)],[420,639,theory(equality)])).
% cnf(649,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,X2)|empty_carrier(esk18_0)|empty_carrier(X1)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|$false|~element(X2,the_carrier(esk18_0))|~top_str(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(esk4_3(esk18_0,X1,X2),esk18_0,esk20_0)),inference(rw,[status(thm)],[643,231,theory(equality)])).
% cnf(650,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,X2)|empty_carrier(esk18_0)|empty_carrier(X1)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|$false|~element(X2,the_carrier(esk18_0))|$false|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(esk4_3(esk18_0,X1,X2),esk18_0,esk20_0)),inference(rw,[status(thm)],[649,230,theory(equality)])).
% cnf(651,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,X2)|empty_carrier(esk18_0)|empty_carrier(X1)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|~element(X2,the_carrier(esk18_0))|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(esk4_3(esk18_0,X1,X2),esk18_0,esk20_0)),inference(cn,[status(thm)],[650,theory(equality)])).
% cnf(652,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,X2)|empty_carrier(X1)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|~element(X2,the_carrier(esk18_0))|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~point_neighbourhood(esk4_3(esk18_0,X1,X2),esk18_0,esk20_0)),inference(sr,[status(thm)],[651,232,theory(equality)])).
% cnf(705,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,esk20_0)|empty_carrier(X1)|empty_carrier(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|~element(esk20_0,the_carrier(esk18_0))|~topological_space(esk18_0)|~top_str(esk18_0)),inference(spm,[status(thm)],[652,88,theory(equality)])).
% cnf(706,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,esk20_0)|empty_carrier(X1)|empty_carrier(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|$false|~topological_space(esk18_0)|~top_str(esk18_0)),inference(rw,[status(thm)],[705,225,theory(equality)])).
% cnf(707,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,esk20_0)|empty_carrier(X1)|empty_carrier(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|$false|$false|~top_str(esk18_0)),inference(rw,[status(thm)],[706,231,theory(equality)])).
% cnf(708,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,esk20_0)|empty_carrier(X1)|empty_carrier(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)|$false|$false|$false),inference(rw,[status(thm)],[707,230,theory(equality)])).
% cnf(709,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,esk20_0)|empty_carrier(X1)|empty_carrier(esk18_0)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)),inference(cn,[status(thm)],[708,theory(equality)])).
% cnf(710,negated_conjecture,(is_a_cluster_point_of_netstr(esk18_0,X1,esk20_0)|empty_carrier(X1)|lim_points_of_net(esk18_0,X1)!=lim_points_of_net(esk18_0,esk19_0)|~net_str(X1,esk18_0)|~directed_relstr(X1)|~transitive_relstr(X1)),inference(sr,[status(thm)],[709,232,theory(equality)])).
% cnf(714,negated_conjecture,(empty_carrier(esk19_0)|~net_str(esk19_0,esk18_0)|~directed_relstr(esk19_0)|~transitive_relstr(esk19_0)),inference(spm,[status(thm)],[223,710,theory(equality)])).
% cnf(720,negated_conjecture,(empty_carrier(esk19_0)|$false|~directed_relstr(esk19_0)|~transitive_relstr(esk19_0)),inference(rw,[status(thm)],[714,226,theory(equality)])).
% cnf(721,negated_conjecture,(empty_carrier(esk19_0)|$false|$false|~transitive_relstr(esk19_0)),inference(rw,[status(thm)],[720,227,theory(equality)])).
% cnf(722,negated_conjecture,(empty_carrier(esk19_0)|$false|$false|$false),inference(rw,[status(thm)],[721,228,theory(equality)])).
% cnf(723,negated_conjecture,(empty_carrier(esk19_0)),inference(cn,[status(thm)],[722,theory(equality)])).
% cnf(724,negated_conjecture,($false),inference(sr,[status(thm)],[723,229,theory(equality)])).
% cnf(725,negated_conjecture,($false),724,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 298
% # ...of these trivial : 1
% # ...subsumed : 33
% # ...remaining for further processing: 264
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 3
% # Backward-rewritten : 4
% # Generated clauses : 295
% # ...of the previous two non-trivial : 280
% # Contextual simplify-reflections : 63
% # Paramodulations : 292
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 187
% # Positive orientable unit clauses: 24
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 13
% # Non-unit-clauses : 150
% # Current number of unprocessed clauses: 114
% # ...number of literals in the above : 760
% # Clause-clause subsumption calls (NU) : 1429
% # Rec. Clause-clause subsumption calls : 1182
% # Unit Clause-clause subsumption calls : 66
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 14
% # Indexed BW rewrite successes : 3
% # Backwards rewriting index: 194 leaves, 1.83+/-2.020 terms/leaf
% # Paramod-from index: 64 leaves, 1.41+/-1.455 terms/leaf
% # Paramod-into index: 175 leaves, 1.74+/-2.028 terms/leaf
% # -------------------------------------------------
% # User time : 0.047 s
% # System time : 0.006 s
% # Total time : 0.053 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.14 CPU 0.22 WC
% FINAL PrfWatch: 0.14 CPU 0.22 WC
% SZS output end Solution for /tmp/SystemOnTPTP31676/SEU386+1.tptp
%
%------------------------------------------------------------------------------