%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 08:59:10 AM UTC 2026
% Result : Theorem 76.78s 77.09s
% Output : Proof 76.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 132 ( 92 unt; 0 def)
% Number of atoms : 494 ( 22 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 581 ( 219 ~; 223 |; 114 &)
% ( 3 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 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 : 117 ( 0 sgn 75 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d18_yellow_6,axiom,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [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) ) ) ) ) ) ) ),
file('theBenchmark.p',d18_yellow_6) ).
fof(d9_waybel_9,axiom,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [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) ) ) ) ) ),
file('theBenchmark.p',d9_waybel_9) ).
fof(dt_k11_yellow_6,axiom,
! [A,B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> element(lim_points_of_net(A,B),powerset(the_carrier(A))) ),
file('theBenchmark.p',dt_k11_yellow_6) ).
fof(dt_l1_pre_topc,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('theBenchmark.p',dt_l1_pre_topc) ).
fof(t28_yellow_6,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [C] :
( is_eventually_in(A,B,C)
=> is_often_in(A,B,C) ) ) ),
file('theBenchmark.p',t28_yellow_6) ).
fof(t29_waybel_9,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,lim_points_of_net(A,B))
=> is_a_cluster_point_of_netstr(A,B,C) ) ) ) ),
file('theBenchmark.p',t29_waybel_9) ).
fof(f_7_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( C = lim_points_of_net(A,B)
| ? [D] :
( ( ( ~ in(D,C)
& ! [E] :
( is_eventually_in(A,B,E)
| ~ point_neighbourhood(E,A,D) ) )
| ( ? [E] :
( ~ is_eventually_in(A,B,E)
& point_neighbourhood(E,A,D) )
& in(D,C) ) )
& element(D,the_carrier(A)) ) )
& ( ! [D] :
( ( ( in(D,C)
| ? [E] :
( ~ is_eventually_in(A,B,E)
& point_neighbourhood(E,A,D) ) )
& ( ! [E] :
( is_eventually_in(A,B,E)
| ~ point_neighbourhood(E,A,D) )
| ~ in(D,C) ) )
| ~ element(D,the_carrier(A)) )
| C != lim_points_of_net(A,B) ) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[d18_yellow_6]) ).
fof(f_7_2,plain,
! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ( ( U_14 = lim_points_of_net(U_16,U_15)
| ? [U_13] :
( ( ( ~ in(U_13,U_14)
& ! [U_12] :
( is_eventually_in(U_16,U_15,U_12)
| ~ point_neighbourhood(U_12,U_16,U_13) ) )
| ( ? [U_11] :
( ~ is_eventually_in(U_16,U_15,U_11)
& point_neighbourhood(U_11,U_16,U_13) )
& in(U_13,U_14) ) )
& element(U_13,the_carrier(U_16)) ) )
& ( ! [U_10] :
( ( ( in(U_10,U_14)
| ? [U_9] :
( ~ is_eventually_in(U_16,U_15,U_9)
& point_neighbourhood(U_9,U_16,U_10) ) )
& ( ! [U_8] :
( is_eventually_in(U_16,U_15,U_8)
| ~ point_neighbourhood(U_8,U_16,U_10) )
| ~ in(U_10,U_14) ) )
| ~ element(U_10,the_carrier(U_16)) )
| U_14 != lim_points_of_net(U_16,U_15) ) )
| ~ element(U_14,powerset(the_carrier(U_16))) )
| ~ net_str(U_15,U_16)
| ~ directed_relstr(U_15)
| ~ transitive_relstr(U_15)
| empty_carrier(U_15) )
| ~ top_str(U_16)
| ~ topological_space(U_16)
| empty_carrier(U_16) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ( ( U_14 = lim_points_of_net(U_16,U_15)
| ? [U_13] :
( ( ( ~ in(U_13,U_14)
& ! [U_12] :
( is_eventually_in(U_16,U_15,U_12)
| ~ point_neighbourhood(U_12,U_16,U_13) ) )
| ( ? [U_11] :
( ~ is_eventually_in(U_16,U_15,U_11)
& point_neighbourhood(U_11,U_16,U_13) )
& in(U_13,U_14) ) )
& element(U_13,the_carrier(U_16)) ) )
& ( ! [U_10] :
( ( ( in(U_10,U_14)
| ( ~ is_eventually_in(U_16,U_15,sK1(U_16,U_15,U_14,U_10))
& point_neighbourhood(sK1(U_16,U_15,U_14,U_10),U_16,U_10) ) )
& ( ! [U_8] :
( is_eventually_in(U_16,U_15,U_8)
| ~ point_neighbourhood(U_8,U_16,U_10) )
| ~ in(U_10,U_14) ) )
| ~ element(U_10,the_carrier(U_16)) )
| U_14 != lim_points_of_net(U_16,U_15) ) )
| ~ element(U_14,powerset(the_carrier(U_16))) )
| ~ net_str(U_15,U_16)
| ~ directed_relstr(U_15)
| ~ transitive_relstr(U_15)
| empty_carrier(U_15) )
| ~ top_str(U_16)
| ~ topological_space(U_16)
| empty_carrier(U_16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_9,sK1(U_16,U_15,U_14,U_10))],[f_7_2]) ).
fof(f_7_4,plain,
! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ( ( U_14 = lim_points_of_net(U_16,U_15)
| ( ( ( ~ in(sK2(U_16,U_15,U_14),U_14)
& ! [U_12] :
( is_eventually_in(U_16,U_15,U_12)
| ~ point_neighbourhood(U_12,U_16,sK2(U_16,U_15,U_14)) ) )
| ( ? [U_11] :
( ~ is_eventually_in(U_16,U_15,U_11)
& point_neighbourhood(U_11,U_16,sK2(U_16,U_15,U_14)) )
& in(sK2(U_16,U_15,U_14),U_14) ) )
& element(sK2(U_16,U_15,U_14),the_carrier(U_16)) ) )
& ( ! [U_10] :
( ( ( in(U_10,U_14)
| ( ~ is_eventually_in(U_16,U_15,sK1(U_16,U_15,U_14,U_10))
& point_neighbourhood(sK1(U_16,U_15,U_14,U_10),U_16,U_10) ) )
& ( ! [U_8] :
( is_eventually_in(U_16,U_15,U_8)
| ~ point_neighbourhood(U_8,U_16,U_10) )
| ~ in(U_10,U_14) ) )
| ~ element(U_10,the_carrier(U_16)) )
| U_14 != lim_points_of_net(U_16,U_15) ) )
| ~ element(U_14,powerset(the_carrier(U_16))) )
| ~ net_str(U_15,U_16)
| ~ directed_relstr(U_15)
| ~ transitive_relstr(U_15)
| empty_carrier(U_15) )
| ~ top_str(U_16)
| ~ topological_space(U_16)
| empty_carrier(U_16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_13,sK2(U_16,U_15,U_14))],[f_7_3]) ).
fof(f_7_5,plain,
! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ( ( U_14 = lim_points_of_net(U_16,U_15)
| ( ( ( ~ in(sK2(U_16,U_15,U_14),U_14)
& ! [U_12] :
( is_eventually_in(U_16,U_15,U_12)
| ~ point_neighbourhood(U_12,U_16,sK2(U_16,U_15,U_14)) ) )
| ( ~ is_eventually_in(U_16,U_15,sK3(U_16,U_15,U_14))
& point_neighbourhood(sK3(U_16,U_15,U_14),U_16,sK2(U_16,U_15,U_14))
& in(sK2(U_16,U_15,U_14),U_14) ) )
& element(sK2(U_16,U_15,U_14),the_carrier(U_16)) ) )
& ( ! [U_10] :
( ( ( in(U_10,U_14)
| ( ~ is_eventually_in(U_16,U_15,sK1(U_16,U_15,U_14,U_10))
& point_neighbourhood(sK1(U_16,U_15,U_14,U_10),U_16,U_10) ) )
& ( ! [U_8] :
( is_eventually_in(U_16,U_15,U_8)
| ~ point_neighbourhood(U_8,U_16,U_10) )
| ~ in(U_10,U_14) ) )
| ~ element(U_10,the_carrier(U_16)) )
| U_14 != lim_points_of_net(U_16,U_15) ) )
| ~ element(U_14,powerset(the_carrier(U_16))) )
| ~ net_str(U_15,U_16)
| ~ directed_relstr(U_15)
| ~ transitive_relstr(U_15)
| empty_carrier(U_15) )
| ~ top_str(U_16)
| ~ topological_space(U_16)
| empty_carrier(U_16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_11,sK3(U_16,U_15,U_14))],[f_7_4]) ).
cnf(f_7_6,plain,
( is_eventually_in(U_16,U_15,U_8)
| ~ point_neighbourhood(U_8,U_16,U_10)
| ~ in(U_10,U_14)
| ~ element(U_10,the_carrier(U_16))
| U_14 != lim_points_of_net(U_16,U_15)
| ~ element(U_14,powerset(the_carrier(U_16)))
| ~ net_str(U_15,U_16)
| ~ directed_relstr(U_15)
| ~ transitive_relstr(U_15)
| empty_carrier(U_15)
| ~ top_str(U_16)
| ~ topological_space(U_16)
| empty_carrier(U_16) ),
inference(clausify,[status(thm)],[f_7_5]) ).
fof(f_8_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( is_a_cluster_point_of_netstr(A,B,C)
| ? [D] :
( ~ is_often_in(A,B,D)
& point_neighbourhood(D,A,C) ) )
& ( ! [D] :
( is_often_in(A,B,D)
| ~ point_neighbourhood(D,A,C) )
| ~ is_a_cluster_point_of_netstr(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ net_str(B,A)
| empty_carrier(B) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[d9_waybel_9]) ).
fof(f_8_2,plain,
! [U_21] :
( ! [U_20] :
( ! [U_19] :
( ( ( is_a_cluster_point_of_netstr(U_21,U_20,U_19)
| ? [U_18] :
( ~ is_often_in(U_21,U_20,U_18)
& point_neighbourhood(U_18,U_21,U_19) ) )
& ( ! [U_17] :
( is_often_in(U_21,U_20,U_17)
| ~ point_neighbourhood(U_17,U_21,U_19) )
| ~ is_a_cluster_point_of_netstr(U_21,U_20,U_19) ) )
| ~ element(U_19,the_carrier(U_21)) )
| ~ net_str(U_20,U_21)
| empty_carrier(U_20) )
| ~ top_str(U_21)
| ~ topological_space(U_21)
| empty_carrier(U_21) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_21] :
( ! [U_20] :
( ! [U_19] :
( ( ( is_a_cluster_point_of_netstr(U_21,U_20,U_19)
| ( ~ is_often_in(U_21,U_20,sK4(U_21,U_20,U_19))
& point_neighbourhood(sK4(U_21,U_20,U_19),U_21,U_19) ) )
& ( ! [U_17] :
( is_often_in(U_21,U_20,U_17)
| ~ point_neighbourhood(U_17,U_21,U_19) )
| ~ is_a_cluster_point_of_netstr(U_21,U_20,U_19) ) )
| ~ element(U_19,the_carrier(U_21)) )
| ~ net_str(U_20,U_21)
| empty_carrier(U_20) )
| ~ top_str(U_21)
| ~ topological_space(U_21)
| empty_carrier(U_21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_18,sK4(U_21,U_20,U_19))],[f_8_2]) ).
cnf(f_8_5,plain,
( point_neighbourhood(sK4(U_21,U_20,U_19),U_21,U_19)
| is_a_cluster_point_of_netstr(U_21,U_20,U_19)
| ~ element(U_19,the_carrier(U_21))
| ~ net_str(U_20,U_21)
| empty_carrier(U_20)
| ~ top_str(U_21)
| ~ topological_space(U_21)
| empty_carrier(U_21) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( ~ is_often_in(U_21,U_20,sK4(U_21,U_20,U_19))
| is_a_cluster_point_of_netstr(U_21,U_20,U_19)
| ~ element(U_19,the_carrier(U_21))
| ~ net_str(U_20,U_21)
| empty_carrier(U_20)
| ~ top_str(U_21)
| ~ topological_space(U_21)
| empty_carrier(U_21) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [A,B] :
( element(lim_points_of_net(A,B),powerset(the_carrier(A)))
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[dt_k11_yellow_6]) ).
fof(f_9_2,plain,
! [U_23,U_22] :
( element(lim_points_of_net(U_23,U_22),powerset(the_carrier(U_23)))
| ~ net_str(U_22,U_23)
| ~ directed_relstr(U_22)
| ~ transitive_relstr(U_22)
| empty_carrier(U_22)
| ~ top_str(U_23)
| ~ topological_space(U_23)
| empty_carrier(U_23) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( element(lim_points_of_net(U_23,U_22),powerset(the_carrier(U_23)))
| ~ net_str(U_22,U_23)
| ~ directed_relstr(U_22)
| ~ transitive_relstr(U_22)
| empty_carrier(U_22)
| ~ top_str(U_23)
| ~ topological_space(U_23)
| empty_carrier(U_23) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_13_1,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(fof_nnf,[status(thm)],[dt_l1_pre_topc]) ).
fof(f_13_2,plain,
! [U_25] :
( one_sorted_str(U_25)
| ~ top_str(U_25) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
( one_sorted_str(U_25)
| ~ top_str(U_25) ),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_37_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( is_often_in(A,B,C)
| ~ is_eventually_in(A,B,C) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[t28_yellow_6]) ).
fof(f_37_2,plain,
! [U_63] :
( ! [U_62] :
( ! [U_61] :
( is_often_in(U_63,U_62,U_61)
| ~ is_eventually_in(U_63,U_62,U_61) )
| ~ net_str(U_62,U_63)
| ~ directed_relstr(U_62)
| ~ transitive_relstr(U_62)
| empty_carrier(U_62) )
| ~ one_sorted_str(U_63)
| empty_carrier(U_63) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
cnf(f_37_3,plain,
( is_often_in(U_63,U_62,U_61)
| ~ is_eventually_in(U_63,U_62,U_61)
| ~ net_str(U_62,U_63)
| ~ directed_relstr(U_62)
| ~ transitive_relstr(U_62)
| empty_carrier(U_62)
| ~ one_sorted_str(U_63)
| empty_carrier(U_63) ),
inference(clausify,[status(thm)],[f_37_2]) ).
fof(f_38_1,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,lim_points_of_net(A,B))
=> is_a_cluster_point_of_netstr(A,B,C) ) ) ) ),
inference(negate,[status(cth)],[t29_waybel_9]) ).
fof(f_38_2,negated_conjecture,
? [A] :
( ? [B] :
( ? [C] :
( ~ is_a_cluster_point_of_netstr(A,B,C)
& in(C,lim_points_of_net(A,B))
& element(C,the_carrier(A)) )
& net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[f_38_1]) ).
fof(f_38_3,negated_conjecture,
? [U_66] :
( ? [U_65] :
( ? [U_64] :
( ~ is_a_cluster_point_of_netstr(U_66,U_65,U_64)
& in(U_64,lim_points_of_net(U_66,U_65))
& element(U_64,the_carrier(U_66)) )
& net_str(U_65,U_66)
& directed_relstr(U_65)
& transitive_relstr(U_65)
& ~ empty_carrier(U_65) )
& top_str(U_66)
& topological_space(U_66)
& ~ empty_carrier(U_66) ),
inference(variable_rename,[status(thm)],[f_38_2]) ).
fof(f_38_4,negated_conjecture,
( ? [U_65] :
( ? [U_64] :
( ~ is_a_cluster_point_of_netstr(sK18,U_65,U_64)
& in(U_64,lim_points_of_net(sK18,U_65))
& element(U_64,the_carrier(sK18)) )
& net_str(U_65,sK18)
& directed_relstr(U_65)
& transitive_relstr(U_65)
& ~ empty_carrier(U_65) )
& top_str(sK18)
& topological_space(sK18)
& ~ empty_carrier(sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_66,sK18)],[f_38_3]) ).
fof(f_38_5,negated_conjecture,
( ? [U_64] :
( ~ is_a_cluster_point_of_netstr(sK18,sK19,U_64)
& in(U_64,lim_points_of_net(sK18,sK19))
& element(U_64,the_carrier(sK18)) )
& net_str(sK19,sK18)
& directed_relstr(sK19)
& transitive_relstr(sK19)
& ~ empty_carrier(sK19)
& top_str(sK18)
& topological_space(sK18)
& ~ empty_carrier(sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_65,sK19)],[f_38_4]) ).
fof(f_38_6,negated_conjecture,
( ~ is_a_cluster_point_of_netstr(sK18,sK19,sK20)
& in(sK20,lim_points_of_net(sK18,sK19))
& element(sK20,the_carrier(sK18))
& net_str(sK19,sK18)
& directed_relstr(sK19)
& transitive_relstr(sK19)
& ~ empty_carrier(sK19)
& top_str(sK18)
& topological_space(sK18)
& ~ empty_carrier(sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_64,sK20)],[f_38_5]) ).
cnf(f_38_7,negated_conjecture,
~ empty_carrier(sK18),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_8,negated_conjecture,
topological_space(sK18),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_9,negated_conjecture,
top_str(sK18),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_10,negated_conjecture,
~ empty_carrier(sK19),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_11,negated_conjecture,
transitive_relstr(sK19),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_12,negated_conjecture,
directed_relstr(sK19),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_13,negated_conjecture,
net_str(sK19,sK18),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_14,negated_conjecture,
element(sK20,the_carrier(sK18)),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_15,negated_conjecture,
in(sK20,lim_points_of_net(sK18,sK19)),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(f_38_16,negated_conjecture,
~ is_a_cluster_point_of_netstr(sK18,sK19,sK20),
inference(clausify,[status(thm)],[f_38_6]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_6,axiom,
( lim_points_of_net(Eq_x_0,Eq_x_1) = lim_points_of_net(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(t1,plain,
~ empty_carrier(sK18),
inference(start,[status(thm),parent(0:0)],[f_38_7]) ).
cnf(t2,plain,
( ~ one_sorted_str(sK18)
| empty_carrier(sK19)
| ~ transitive_relstr(sK19)
| ~ directed_relstr(sK19)
| ~ net_str(sK19,sK18)
| ~ is_eventually_in(sK18,sK19,sK4(sK18,sK19,sK20))
| is_often_in(sK18,sK19,sK4(sK18,sK19,sK20))
| empty_carrier(sK18) ),
inference(extension,[status(thm),parent(t1:1)],[f_37_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ topological_space(sK18)
| ~ top_str(sK18)
| empty_carrier(sK19)
| ~ net_str(sK19,sK18)
| ~ element(sK20,the_carrier(sK18))
| is_a_cluster_point_of_netstr(sK18,sK19,sK20)
| empty_carrier(sK18)
| ~ is_often_in(sK18,sK19,sK4(sK18,sK19,sK20)) ),
inference(extension,[status(thm),parent(t2:2)],[f_8_6]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
$false,
inference(reduction,[status(thm),parent(t4:2)],[t4:2,t1:1]) ).
cnf(t7,plain,
~ is_a_cluster_point_of_netstr(sK18,sK19,sK20),
inference(extension,[status(thm),parent(t4:3)],[f_38_16]) ).
cnf(t8,plain,
$false,
inference(connection,[status(thm),parent(t7:1)],[t7:1,t4:3]) ).
cnf(t9,plain,
element(sK20,the_carrier(sK18)),
inference(extension,[status(thm),parent(t4:4)],[f_38_14]) ).
cnf(t10,plain,
$false,
inference(connection,[status(thm),parent(t9:1)],[t9:1,t4:4]) ).
cnf(t11,plain,
net_str(sK19,sK18),
inference(extension,[status(thm),parent(t4:5)],[f_38_13]) ).
cnf(t12,plain,
$false,
inference(connection,[status(thm),parent(t11:1)],[t11:1,t4:5]) ).
cnf(t13,plain,
~ empty_carrier(sK19),
inference(extension,[status(thm),parent(t4:6)],[f_38_10]) ).
cnf(t14,plain,
$false,
inference(connection,[status(thm),parent(t13:1)],[t13:1,t4:6]) ).
cnf(t15,plain,
top_str(sK18),
inference(extension,[status(thm),parent(t4:7)],[f_38_9]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t4:7]) ).
cnf(t17,plain,
topological_space(sK18),
inference(extension,[status(thm),parent(t4:8)],[f_38_8]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t4:8]) ).
cnf(t19,plain,
( ~ topological_space(sK18)
| ~ top_str(sK18)
| empty_carrier(sK19)
| ~ transitive_relstr(sK19)
| ~ directed_relstr(sK19)
| ~ net_str(sK19,sK18)
| ~ element(lim_points_of_net(sK18,sK19),powerset(the_carrier(sK18)))
| lim_points_of_net(sK18,sK19) != lim_points_of_net(sK18,sK19)
| ~ element(sK20,the_carrier(sK18))
| ~ in(sK20,lim_points_of_net(sK18,sK19))
| ~ point_neighbourhood(sK4(sK18,sK19,sK20),sK18,sK20)
| empty_carrier(sK18)
| is_eventually_in(sK18,sK19,sK4(sK18,sK19,sK20)) ),
inference(extension,[status(thm),parent(t2:3)],[f_7_6]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t2:3]) ).
cnf(t21,plain,
$false,
inference(reduction,[status(thm),parent(t19:2)],[t19:2,t1:1]) ).
cnf(l11,lemma,
~ empty_carrier(sK18),
inference(lemma,[status(cth),parent(t19:2),below(t2:3)],[t19:2]) ).
cnf(t22,plain,
( ~ topological_space(sK18)
| ~ top_str(sK18)
| empty_carrier(sK19)
| ~ net_str(sK19,sK18)
| ~ element(sK20,the_carrier(sK18))
| is_a_cluster_point_of_netstr(sK18,sK19,sK20)
| empty_carrier(sK18)
| point_neighbourhood(sK4(sK18,sK19,sK20),sK18,sK20) ),
inference(extension,[status(thm),parent(t19:3)],[f_8_5]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t19:3]) ).
cnf(t24,plain,
~ empty_carrier(sK18),
inference(lemma_extension,[status(thm),parent(t22:2)],[l11:1]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
~ is_a_cluster_point_of_netstr(sK18,sK19,sK20),
inference(extension,[status(thm),parent(t22:3)],[f_38_16]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t22:3]) ).
cnf(t28,plain,
element(sK20,the_carrier(sK18)),
inference(extension,[status(thm),parent(t22:4)],[f_38_14]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t22:4]) ).
cnf(t30,plain,
net_str(sK19,sK18),
inference(extension,[status(thm),parent(t22:5)],[f_38_13]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t22:5]) ).
cnf(t32,plain,
~ empty_carrier(sK19),
inference(extension,[status(thm),parent(t22:6)],[f_38_10]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t22:6]) ).
cnf(t34,plain,
top_str(sK18),
inference(extension,[status(thm),parent(t22:7)],[f_38_9]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t22:7]) ).
cnf(t36,plain,
topological_space(sK18),
inference(extension,[status(thm),parent(t22:8)],[f_38_8]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t22:8]) ).
cnf(t38,plain,
in(sK20,lim_points_of_net(sK18,sK19)),
inference(extension,[status(thm),parent(t19:4)],[f_38_15]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t19:4]) ).
cnf(t40,plain,
element(sK20,the_carrier(sK18)),
inference(extension,[status(thm),parent(t19:5)],[f_38_14]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t19:5]) ).
cnf(t42,plain,
( sK19 != sK19
| sK18 != sK18
| lim_points_of_net(sK18,sK19) = lim_points_of_net(sK18,sK19) ),
inference(extension,[status(thm),parent(t19:6)],[equality_6]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t19:6]) ).
cnf(t44,plain,
sK18 = sK18,
inference(extension,[status(thm),parent(t42:2)],[equality_1]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t42:2]) ).
cnf(t46,plain,
sK19 = sK19,
inference(extension,[status(thm),parent(t42:3)],[equality_1]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t42:3]) ).
cnf(t48,plain,
( ~ topological_space(sK18)
| ~ top_str(sK18)
| empty_carrier(sK19)
| ~ transitive_relstr(sK19)
| ~ directed_relstr(sK19)
| ~ net_str(sK19,sK18)
| empty_carrier(sK18)
| element(lim_points_of_net(sK18,sK19),powerset(the_carrier(sK18))) ),
inference(extension,[status(thm),parent(t19:7)],[f_9_3]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t19:7]) ).
cnf(t50,plain,
~ empty_carrier(sK18),
inference(lemma_extension,[status(thm),parent(t48:2)],[l11:1]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
net_str(sK19,sK18),
inference(extension,[status(thm),parent(t48:3)],[f_38_13]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t48:3]) ).
cnf(t54,plain,
directed_relstr(sK19),
inference(extension,[status(thm),parent(t48:4)],[f_38_12]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t48:4]) ).
cnf(t56,plain,
transitive_relstr(sK19),
inference(extension,[status(thm),parent(t48:5)],[f_38_11]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t48:5]) ).
cnf(t58,plain,
~ empty_carrier(sK19),
inference(extension,[status(thm),parent(t48:6)],[f_38_10]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t48:6]) ).
cnf(t60,plain,
top_str(sK18),
inference(extension,[status(thm),parent(t48:7)],[f_38_9]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t48:7]) ).
cnf(t62,plain,
topological_space(sK18),
inference(extension,[status(thm),parent(t48:8)],[f_38_8]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t48:8]) ).
cnf(t64,plain,
net_str(sK19,sK18),
inference(extension,[status(thm),parent(t19:8)],[f_38_13]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t19:8]) ).
cnf(t66,plain,
directed_relstr(sK19),
inference(extension,[status(thm),parent(t19:9)],[f_38_12]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t19:9]) ).
cnf(t68,plain,
transitive_relstr(sK19),
inference(extension,[status(thm),parent(t19:10)],[f_38_11]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t19:10]) ).
cnf(t70,plain,
~ empty_carrier(sK19),
inference(extension,[status(thm),parent(t19:11)],[f_38_10]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t19:11]) ).
cnf(t72,plain,
top_str(sK18),
inference(extension,[status(thm),parent(t19:12)],[f_38_9]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t19:12]) ).
cnf(t74,plain,
topological_space(sK18),
inference(extension,[status(thm),parent(t19:13)],[f_38_8]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t19:13]) ).
cnf(t76,plain,
net_str(sK19,sK18),
inference(extension,[status(thm),parent(t2:4)],[f_38_13]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t2:4]) ).
cnf(t78,plain,
directed_relstr(sK19),
inference(extension,[status(thm),parent(t2:5)],[f_38_12]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t2:5]) ).
cnf(t80,plain,
transitive_relstr(sK19),
inference(extension,[status(thm),parent(t2:6)],[f_38_11]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t2:6]) ).
cnf(t82,plain,
~ empty_carrier(sK19),
inference(extension,[status(thm),parent(t2:7)],[f_38_10]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t2:7]) ).
cnf(t84,plain,
( ~ top_str(sK18)
| one_sorted_str(sK18) ),
inference(extension,[status(thm),parent(t2:8)],[f_13_3]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t2:8]) ).
cnf(t86,plain,
top_str(sK18),
inference(extension,[status(thm),parent(t84:2)],[f_38_9]) ).
cnf(t87,plain,
$false,
inference(connection,[status(thm),parent(t86:1)],[t86:1,t84:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 00:11:21 UTC 2026
% 0.08/0.35 % CPUTime :
% 76.78/77.09 % SZS status Theorem for theBenchmark
% 76.78/77.09 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------