%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU386+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Sun Dec 26 08:12:20 EST 2010
% Result : Theorem 0.51s
% Output : CNFRefutation 0.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 7
% Syntax : Number of formulae : 83 ( 13 unt; 0 def)
% Number of atoms : 779 ( 40 equ)
% Maximal formula atoms : 81 ( 9 avg)
% Number of connectives : 1113 ( 417 ~; 531 |; 119 &)
% ( 6 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-4 aty)
% Number of variables : 196 ( 0 sgn 112 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(8,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/tmpCH5TIr/sel_SEU386+1.p_1',t29_waybel_9) ).
fof(12,axiom,
! [X1,X2,X3] :
( ( in(X1,X2)
& element(X2,powerset(X3)) )
=> element(X1,X3) ),
file('/tmp/tmpCH5TIr/sel_SEU386+1.p_1',t4_subset) ).
fof(18,axiom,
! [X1] :
( top_str(X1)
=> one_sorted_str(X1) ),
file('/tmp/tmpCH5TIr/sel_SEU386+1.p_1',dt_l1_pre_topc) ).
fof(20,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/tmpCH5TIr/sel_SEU386+1.p_1',d18_yellow_6) ).
fof(25,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/tmpCH5TIr/sel_SEU386+1.p_1',t28_yellow_6) ).
fof(33,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/tmpCH5TIr/sel_SEU386+1.p_1',d9_waybel_9) ).
fof(34,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/tmpCH5TIr/sel_SEU386+1.p_1',dt_k11_yellow_6) ).
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)],[8]) ).
fof(49,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(53,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)],[20,theory(equality)]) ).
fof(55,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)],[25,theory(equality)]) ).
fof(57,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)],[33,theory(equality)]) ).
fof(58,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)],[34,theory(equality)]) ).
fof(84,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)],[49]) ).
fof(85,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)],[84]) ).
fof(86,negated_conjecture,
( ~ empty_carrier(esk3_0)
& topological_space(esk3_0)
& top_str(esk3_0)
& ~ empty_carrier(esk4_0)
& transitive_relstr(esk4_0)
& directed_relstr(esk4_0)
& net_str(esk4_0,esk3_0)
& element(esk5_0,the_carrier(esk3_0))
& in(esk5_0,lim_points_of_net(esk3_0,esk4_0))
& ~ is_a_cluster_point_of_netstr(esk3_0,esk4_0,esk5_0) ),
inference(skolemize,[status(esa)],[85]) ).
cnf(87,negated_conjecture,
~ is_a_cluster_point_of_netstr(esk3_0,esk4_0,esk5_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(88,negated_conjecture,
in(esk5_0,lim_points_of_net(esk3_0,esk4_0)),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(89,negated_conjecture,
element(esk5_0,the_carrier(esk3_0)),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(90,negated_conjecture,
net_str(esk4_0,esk3_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(91,negated_conjecture,
directed_relstr(esk4_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(92,negated_conjecture,
transitive_relstr(esk4_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(93,negated_conjecture,
~ empty_carrier(esk4_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(94,negated_conjecture,
top_str(esk3_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(95,negated_conjecture,
topological_space(esk3_0),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(96,negated_conjecture,
~ empty_carrier(esk3_0),
inference(split_conjunct,[status(thm)],[86]) ).
fof(106,plain,
! [X1,X2,X3] :
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| element(X1,X3) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(107,plain,
! [X4,X5,X6] :
( ~ in(X4,X5)
| ~ element(X5,powerset(X6))
| element(X4,X6) ),
inference(variable_rename,[status(thm)],[106]) ).
cnf(108,plain,
( element(X1,X2)
| ~ element(X3,powerset(X2))
| ~ in(X1,X3) ),
inference(split_conjunct,[status(thm)],[107]) ).
fof(127,plain,
! [X1] :
( ~ top_str(X1)
| one_sorted_str(X1) ),
inference(fof_nnf,[status(thm)],[18]) ).
fof(128,plain,
! [X2] :
( ~ top_str(X2)
| one_sorted_str(X2) ),
inference(variable_rename,[status(thm)],[127]) ).
cnf(129,plain,
( one_sorted_str(X1)
| ~ top_str(X1) ),
inference(split_conjunct,[status(thm)],[128]) ).
fof(134,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)],[53]) ).
fof(135,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)],[134]) ).
fof(136,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(esk9_4(X6,X7,X8,X9),X6,X9)
& ~ is_eventually_in(X6,X7,esk9_4(X6,X7,X8,X9)) )
| in(X9,X8) ) ) ) )
& ( ( element(esk10_3(X6,X7,X8),the_carrier(X6))
& ( ~ in(esk10_3(X6,X7,X8),X8)
| ( point_neighbourhood(esk11_3(X6,X7,X8),X6,esk10_3(X6,X7,X8))
& ~ is_eventually_in(X6,X7,esk11_3(X6,X7,X8)) ) )
& ( in(esk10_3(X6,X7,X8),X8)
| ! [X14] :
( ~ point_neighbourhood(X14,X6,esk10_3(X6,X7,X8))
| is_eventually_in(X6,X7,X14) ) ) )
| X8 = lim_points_of_net(X6,X7) ) ) ) ) ),
inference(skolemize,[status(esa)],[135]) ).
fof(137,plain,
! [X6,X7,X8,X9,X10,X14] :
( ( ( ( ( ~ point_neighbourhood(X14,X6,esk10_3(X6,X7,X8))
| is_eventually_in(X6,X7,X14)
| in(esk10_3(X6,X7,X8),X8) )
& ( ~ in(esk10_3(X6,X7,X8),X8)
| ( point_neighbourhood(esk11_3(X6,X7,X8),X6,esk10_3(X6,X7,X8))
& ~ is_eventually_in(X6,X7,esk11_3(X6,X7,X8)) ) )
& element(esk10_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(esk9_4(X6,X7,X8,X9),X6,X9)
& ~ is_eventually_in(X6,X7,esk9_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)],[136]) ).
fof(138,plain,
! [X6,X7,X8,X9,X10,X14] :
( ( ~ point_neighbourhood(X14,X6,esk10_3(X6,X7,X8))
| is_eventually_in(X6,X7,X14)
| in(esk10_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(esk11_3(X6,X7,X8),X6,esk10_3(X6,X7,X8))
| ~ in(esk10_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,esk11_3(X6,X7,X8))
| ~ in(esk10_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(esk10_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(esk9_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,esk9_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)],[137]) ).
cnf(141,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)],[138]) ).
fof(157,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)],[55]) ).
fof(158,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)],[157]) ).
fof(159,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)],[158]) ).
cnf(160,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)],[159]) ).
fof(186,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)],[57]) ).
fof(187,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)],[186]) ).
fof(188,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(esk15_3(X5,X6,X7),X5,X7)
& ~ is_often_in(X5,X6,esk15_3(X5,X6,X7)) )
| is_a_cluster_point_of_netstr(X5,X6,X7) ) ) ) ) ),
inference(skolemize,[status(esa)],[187]) ).
fof(189,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(esk15_3(X5,X6,X7),X5,X7)
& ~ is_often_in(X5,X6,esk15_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)],[188]) ).
fof(190,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(esk15_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,esk15_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)],[189]) ).
cnf(191,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,esk15_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[190]) ).
cnf(192,plain,
( empty_carrier(X1)
| empty_carrier(X2)
| is_a_cluster_point_of_netstr(X1,X2,X3)
| point_neighbourhood(esk15_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)],[190]) ).
fof(194,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)],[58]) ).
fof(195,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)],[194]) ).
cnf(196,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)],[195]) ).
cnf(273,plain,
( is_a_cluster_point_of_netstr(X1,X2,X3)
| empty_carrier(X1)
| empty_carrier(X2)
| ~ net_str(X2,X1)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X3,the_carrier(X1))
| ~ is_eventually_in(X1,X2,esk15_3(X1,X2,X3))
| ~ one_sorted_str(X1)
| ~ directed_relstr(X2)
| ~ transitive_relstr(X2) ),
inference(spm,[status(thm)],[191,160,theory(equality)]) ).
cnf(278,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)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ in(X4,X3)
| ~ element(X3,powerset(the_carrier(X1))) ),
inference(csr,[status(thm)],[141,108]) ).
cnf(283,plain,
( is_eventually_in(X1,X2,X3)
| empty_carrier(X1)
| empty_carrier(X2)
| 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)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ in(X5,lim_points_of_net(X1,X4))
| ~ net_str(X4,X1)
| ~ directed_relstr(X4)
| ~ transitive_relstr(X4) ),
inference(spm,[status(thm)],[278,196,theory(equality)]) ).
cnf(461,plain,
( is_a_cluster_point_of_netstr(X1,X2,X3)
| empty_carrier(X1)
| empty_carrier(X2)
| ~ is_eventually_in(X1,X2,esk15_3(X1,X2,X3))
| ~ net_str(X2,X1)
| ~ directed_relstr(X2)
| ~ transitive_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X3,the_carrier(X1)) ),
inference(csr,[status(thm)],[273,129]) ).
cnf(781,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| ~ net_str(esk4_0,esk3_0)
| ~ directed_relstr(X1)
| ~ directed_relstr(esk4_0)
| ~ transitive_relstr(X1)
| ~ transitive_relstr(esk4_0)
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0) ),
inference(spm,[status(thm)],[283,88,theory(equality)]) ).
cnf(783,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| $false
| ~ directed_relstr(X1)
| ~ directed_relstr(esk4_0)
| ~ transitive_relstr(X1)
| ~ transitive_relstr(esk4_0)
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0) ),
inference(rw,[status(thm)],[781,90,theory(equality)]) ).
cnf(784,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| $false
| ~ directed_relstr(X1)
| $false
| ~ transitive_relstr(X1)
| ~ transitive_relstr(esk4_0)
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0) ),
inference(rw,[status(thm)],[783,91,theory(equality)]) ).
cnf(785,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| $false
| ~ directed_relstr(X1)
| $false
| ~ transitive_relstr(X1)
| $false
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0) ),
inference(rw,[status(thm)],[784,92,theory(equality)]) ).
cnf(786,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| $false
| ~ directed_relstr(X1)
| $false
| ~ transitive_relstr(X1)
| $false
| $false
| ~ topological_space(esk3_0) ),
inference(rw,[status(thm)],[785,94,theory(equality)]) ).
cnf(787,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| $false
| ~ directed_relstr(X1)
| $false
| ~ transitive_relstr(X1)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[786,95,theory(equality)]) ).
cnf(788,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(esk4_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1) ),
inference(cn,[status(thm)],[787,theory(equality)]) ).
cnf(789,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1) ),
inference(sr,[status(thm)],[788,93,theory(equality)]) ).
cnf(790,negated_conjecture,
( is_eventually_in(esk3_0,X1,X2)
| empty_carrier(X1)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(X2,esk3_0,esk5_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1) ),
inference(sr,[status(thm)],[789,96,theory(equality)]) ).
cnf(794,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,X2)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0)
| ~ element(X2,the_carrier(esk3_0))
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(esk15_3(esk3_0,X1,X2),esk3_0,esk5_0) ),
inference(spm,[status(thm)],[461,790,theory(equality)]) ).
cnf(803,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,X2)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| $false
| ~ topological_space(esk3_0)
| ~ element(X2,the_carrier(esk3_0))
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(esk15_3(esk3_0,X1,X2),esk3_0,esk5_0) ),
inference(rw,[status(thm)],[794,94,theory(equality)]) ).
cnf(804,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,X2)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| $false
| $false
| ~ element(X2,the_carrier(esk3_0))
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(esk15_3(esk3_0,X1,X2),esk3_0,esk5_0) ),
inference(rw,[status(thm)],[803,95,theory(equality)]) ).
cnf(805,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,X2)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ element(X2,the_carrier(esk3_0))
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(esk15_3(esk3_0,X1,X2),esk3_0,esk5_0) ),
inference(cn,[status(thm)],[804,theory(equality)]) ).
cnf(806,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ element(X2,the_carrier(esk3_0))
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ point_neighbourhood(esk15_3(esk3_0,X1,X2),esk3_0,esk5_0) ),
inference(sr,[status(thm)],[805,96,theory(equality)]) ).
cnf(4077,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,esk5_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| ~ element(esk5_0,the_carrier(esk3_0))
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0) ),
inference(spm,[status(thm)],[806,192,theory(equality)]) ).
cnf(4078,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,esk5_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| $false
| ~ top_str(esk3_0)
| ~ topological_space(esk3_0) ),
inference(rw,[status(thm)],[4077,89,theory(equality)]) ).
cnf(4079,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,esk5_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| $false
| $false
| ~ topological_space(esk3_0) ),
inference(rw,[status(thm)],[4078,94,theory(equality)]) ).
cnf(4080,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,esk5_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[4079,95,theory(equality)]) ).
cnf(4081,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,esk5_0)
| empty_carrier(X1)
| empty_carrier(esk3_0)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1) ),
inference(cn,[status(thm)],[4080,theory(equality)]) ).
cnf(4082,negated_conjecture,
( is_a_cluster_point_of_netstr(esk3_0,X1,esk5_0)
| empty_carrier(X1)
| lim_points_of_net(esk3_0,X1) != lim_points_of_net(esk3_0,esk4_0)
| ~ net_str(X1,esk3_0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1) ),
inference(sr,[status(thm)],[4081,96,theory(equality)]) ).
cnf(4083,negated_conjecture,
( empty_carrier(esk4_0)
| ~ net_str(esk4_0,esk3_0)
| ~ directed_relstr(esk4_0)
| ~ transitive_relstr(esk4_0) ),
inference(spm,[status(thm)],[87,4082,theory(equality)]) ).
cnf(4084,negated_conjecture,
( empty_carrier(esk4_0)
| $false
| ~ directed_relstr(esk4_0)
| ~ transitive_relstr(esk4_0) ),
inference(rw,[status(thm)],[4083,90,theory(equality)]) ).
cnf(4085,negated_conjecture,
( empty_carrier(esk4_0)
| $false
| $false
| ~ transitive_relstr(esk4_0) ),
inference(rw,[status(thm)],[4084,91,theory(equality)]) ).
cnf(4086,negated_conjecture,
( empty_carrier(esk4_0)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[4085,92,theory(equality)]) ).
cnf(4087,negated_conjecture,
empty_carrier(esk4_0),
inference(cn,[status(thm)],[4086,theory(equality)]) ).
cnf(4088,negated_conjecture,
$false,
inference(sr,[status(thm)],[4087,93,theory(equality)]) ).
cnf(4089,negated_conjecture,
$false,
4088,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% /home/graph/tptp/Systems/SInE---0.4/Source/sine.py:10: DeprecationWarning: the sets module is deprecated
% from sets import Set
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU386+1.p
% --creating new selector for []
% -running prover on /tmp/tmpCH5TIr/sel_SEU386+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU386+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU386+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU386+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------