%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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 : Fri Sep 25 02:51:55 PM UTC 2026
% Result : Theorem 13.05s 2.26s
% Output : Proof 13.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 6
% Syntax : Number of formulae : 77 ( 13 unt; 0 def)
% Number of atoms : 476 ( 11 equ)
% Maximal formula atoms : 24 ( 6 avg)
% Number of connectives : 602 ( 203 ~; 310 |; 64 &)
% ( 3 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 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 : 120 ( 0 sgn 52 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_yellow_6) ).
fof(f8_nnf,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(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,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(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c20,plain,
( element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f37,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_waybel_9) ).
fof(f37_neg,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(negated_conjecture,[status(cth)],[f37]) ).
fof(f37_nnf,plain,
? [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(nnf_transformation,[status(thm)],[f37_neg]) ).
fof(f37_sk,plain,
( ~ is_a_cluster_point_of_netstr(sk17,sk18,sk19)
& in(sk19,lim_points_of_net(sk17,sk18))
& element(sk19,the_carrier(sk17))
& net_str(sk18,sk17)
& directed_relstr(sk18)
& transitive_relstr(sk18)
& ~ empty_carrier(sk18)
& top_str(sk17)
& topological_space(sk17)
& ~ empty_carrier(sk17) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17,sk18,sk19])],[f37_nnf]) ).
cnf(c60,plain,
topological_space(sk17),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p173,plain,
( element(lim_points_of_net(sk17,X0),powerset(the_carrier(sk17)))
| ~ net_str(X0,sk17)
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| ~ top_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c20,c60]) ).
cnf(c61,plain,
top_str(sk17),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p175,plain,
( element(lim_points_of_net(sk17,X0),powerset(the_carrier(sk17)))
| ~ net_str(X0,sk17)
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p173,c61]) ).
cnf(c63,plain,
transitive_relstr(sk18),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p177,plain,
( element(lim_points_of_net(sk17,sk18),powerset(the_carrier(sk17)))
| ~ net_str(sk18,sk17)
| ~ directed_relstr(sk18)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p175,c63]) ).
cnf(c64,plain,
directed_relstr(sk18),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p179,plain,
( element(lim_points_of_net(sk17,sk18),powerset(the_carrier(sk17)))
| ~ net_str(sk18,sk17)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p177,c64]) ).
cnf(c65,plain,
net_str(sk18,sk17),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p180,plain,
( element(lim_points_of_net(sk17,sk18),powerset(the_carrier(sk17)))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p179,c65]) ).
fof(f6,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',d18_yellow_6) ).
fof(f6_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( ( ( ! [E] :
( is_eventually_in(A,B,E)
| ~ point_neighbourhood(E,A,D) )
& ~ in(D,C) )
| ( ? [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) )
& ( ! [D] :
( ( ( ? [E] :
( ~ is_eventually_in(A,B,E)
& point_neighbourhood(E,A,D) )
| in(D,C) )
& ( ! [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(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C,D,E] :
( ( ( ( ( ( ( is_eventually_in(A,B,E)
| ~ point_neighbourhood(E,A,sk1(A,B,C)) )
& ~ in(sk1(A,B,C),C) )
| ( ~ is_eventually_in(A,B,sk2(A,B,C))
& point_neighbourhood(sk2(A,B,C),A,sk1(A,B,C))
& in(sk1(A,B,C),C) ) )
& element(sk1(A,B,C),the_carrier(A)) )
| C = lim_points_of_net(A,B) )
& ( ( ( ( ~ is_eventually_in(A,B,sk0(A,B,C,D))
& point_neighbourhood(sk0(A,B,C,D),A,D) )
| in(D,C) )
& ( 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(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f6_nnf]) ).
cnf(c7,plain,
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0))
| X2 != lim_points_of_net(X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p88,plain,
( is_eventually_in(sk17,X0,X3)
| ~ point_neighbourhood(X3,sk17,X2)
| ~ in(X2,X1)
| ~ element(X2,the_carrier(sk17))
| X1 != lim_points_of_net(sk17,X0)
| ~ element(X1,powerset(the_carrier(sk17)))
| ~ net_str(X0,sk17)
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| ~ top_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c7,c60]) ).
cnf(p91,plain,
( is_eventually_in(sk17,X0,X3)
| ~ point_neighbourhood(X3,sk17,X2)
| ~ in(X2,X1)
| ~ element(X2,the_carrier(sk17))
| X1 != lim_points_of_net(sk17,X0)
| ~ element(X1,powerset(the_carrier(sk17)))
| ~ net_str(X0,sk17)
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p88,c61]) ).
cnf(p99,plain,
( is_eventually_in(sk17,sk18,X2)
| ~ point_neighbourhood(X2,sk17,X1)
| ~ in(X1,X0)
| ~ element(X1,the_carrier(sk17))
| X0 != lim_points_of_net(sk17,sk18)
| ~ element(X0,powerset(the_carrier(sk17)))
| ~ net_str(sk18,sk17)
| ~ directed_relstr(sk18)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p91,c63]) ).
cnf(p101,plain,
( is_eventually_in(sk17,sk18,X2)
| ~ point_neighbourhood(X2,sk17,X1)
| ~ in(X1,X0)
| ~ element(X1,the_carrier(sk17))
| X0 != lim_points_of_net(sk17,sk18)
| ~ element(X0,powerset(the_carrier(sk17)))
| ~ net_str(sk18,sk17)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p99,c64]) ).
cnf(p103,plain,
( is_eventually_in(sk17,sk18,X2)
| ~ point_neighbourhood(X2,sk17,X1)
| ~ in(X1,X0)
| ~ element(X1,the_carrier(sk17))
| X0 != lim_points_of_net(sk17,sk18)
| ~ element(X0,powerset(the_carrier(sk17)))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p101,c65]) ).
cnf(p104,plain,
( is_eventually_in(sk17,sk18,X1)
| ~ point_neighbourhood(X1,sk17,X0)
| ~ in(X0,lim_points_of_net(sk17,sk18))
| ~ element(X0,the_carrier(sk17))
| ~ element(lim_points_of_net(sk17,sk18),powerset(the_carrier(sk17)))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(equality_resolution,[status(thm)],[p103]) ).
cnf(p182,plain,
( is_eventually_in(sk17,sk18,X1)
| ~ point_neighbourhood(X1,sk17,X0)
| ~ in(X0,lim_points_of_net(sk17,sk18))
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk18)
| empty_carrier(sk17)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p180,p104]) ).
cnf(p530,plain,
( is_eventually_in(sk17,sk18,X1)
| ~ point_neighbourhood(X1,sk17,X0)
| ~ in(X0,lim_points_of_net(sk17,sk18))
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk18)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p182]) ).
cnf(p690,plain,
( is_eventually_in(sk17,sk18,X1)
| ~ point_neighbourhood(X1,sk17,X0)
| ~ in(X0,lim_points_of_net(sk17,sk18))
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p530]) ).
cnf(c66,plain,
element(sk19,the_carrier(sk17)),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p691,plain,
( is_eventually_in(sk17,sk18,X0)
| ~ point_neighbourhood(X0,sk17,sk19)
| ~ in(sk19,lim_points_of_net(sk17,sk18))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p690,c66]) ).
cnf(c67,plain,
in(sk19,lim_points_of_net(sk17,sk18)),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p700,plain,
( is_eventually_in(sk17,sk18,X0)
| ~ point_neighbourhood(X0,sk17,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p691,c67]) ).
fof(f7,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_waybel_9) ).
fof(f7_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ is_often_in(A,B,D)
& point_neighbourhood(D,A,C) )
| is_a_cluster_point_of_netstr(A,B,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(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C,D] :
( ( ( ( ~ is_often_in(A,B,sk3(A,B,C))
& point_neighbourhood(sk3(A,B,C),A,C) )
| is_a_cluster_point_of_netstr(A,B,C) )
& ( 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(skolemisation,[status(esa),new_symbols(skolem,[sk3])],[f7_nnf]) ).
cnf(c18,plain,
( point_neighbourhood(sk3(X0,X1,X2),X0,X2)
| is_a_cluster_point_of_netstr(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p162,plain,
( point_neighbourhood(sk3(sk17,X0,X1),sk17,X1)
| is_a_cluster_point_of_netstr(sk17,X0,X1)
| ~ element(X1,the_carrier(sk17))
| ~ net_str(X0,sk17)
| empty_carrier(X0)
| ~ top_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c18,c60]) ).
cnf(p164,plain,
( point_neighbourhood(sk3(sk17,X0,X1),sk17,X1)
| is_a_cluster_point_of_netstr(sk17,X0,X1)
| ~ element(X1,the_carrier(sk17))
| ~ net_str(X0,sk17)
| empty_carrier(X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p162,c61]) ).
cnf(p168,plain,
( point_neighbourhood(sk3(sk17,sk18,X0),sk17,X0)
| is_a_cluster_point_of_netstr(sk17,sk18,X0)
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p164,c65]) ).
cnf(p169,plain,
( point_neighbourhood(sk3(sk17,sk18,sk19),sk17,sk19)
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p168,c66]) ).
cnf(p701,plain,
( is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17)
| is_eventually_in(sk17,sk18,sk3(sk17,sk18,sk19))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p700,p169]) ).
cnf(p711,plain,
( is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| is_eventually_in(sk17,sk18,sk3(sk17,sk18,sk19))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p701]) ).
cnf(p714,plain,
( is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| is_eventually_in(sk17,sk18,sk3(sk17,sk18,sk19))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p711]) ).
fof(f36,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_yellow_6) ).
fof(f36_nnf,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(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,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(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c58,plain,
( is_often_in(X0,X1,X2)
| ~ is_eventually_in(X0,X1,X2)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
fof(f12,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f12_nnf,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c24,plain,
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p189,plain,
one_sorted_str(sk17),
inference(resolution,[status(thm)],[c24,c61]) ).
cnf(p319,plain,
( is_often_in(sk17,X0,X1)
| ~ is_eventually_in(sk17,X0,X1)
| ~ net_str(X0,sk17)
| ~ directed_relstr(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c58,p189]) ).
cnf(p567,plain,
( is_often_in(sk17,sk18,X0)
| ~ is_eventually_in(sk17,sk18,X0)
| ~ net_str(sk18,sk17)
| ~ directed_relstr(sk18)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p319,c63]) ).
cnf(p568,plain,
( is_often_in(sk17,sk18,X0)
| ~ is_eventually_in(sk17,sk18,X0)
| ~ net_str(sk18,sk17)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p567,c64]) ).
cnf(p569,plain,
( is_often_in(sk17,sk18,X0)
| ~ is_eventually_in(sk17,sk18,X0)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p568,c65]) ).
cnf(p715,plain,
( is_often_in(sk17,sk18,sk3(sk17,sk18,sk19))
| empty_carrier(sk18)
| empty_carrier(sk17)
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p714,p569]) ).
cnf(p716,plain,
( is_often_in(sk17,sk18,sk3(sk17,sk18,sk19))
| empty_carrier(sk18)
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p715]) ).
cnf(p718,plain,
( is_often_in(sk17,sk18,sk3(sk17,sk18,sk19))
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p716]) ).
cnf(c19,plain,
( ~ is_often_in(X0,X1,sk3(X0,X1,X2))
| is_a_cluster_point_of_netstr(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p167,plain,
( ~ is_often_in(sk17,X0,sk3(sk17,X0,X1))
| is_a_cluster_point_of_netstr(sk17,X0,X1)
| ~ element(X1,the_carrier(sk17))
| ~ net_str(X0,sk17)
| empty_carrier(X0)
| ~ top_str(sk17)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[c19,c60]) ).
cnf(p171,plain,
( ~ is_often_in(sk17,X0,sk3(sk17,X0,X1))
| is_a_cluster_point_of_netstr(sk17,X0,X1)
| ~ element(X1,the_carrier(sk17))
| ~ net_str(X0,sk17)
| empty_carrier(X0)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p167,c61]) ).
cnf(p190,plain,
( ~ is_often_in(sk17,sk18,sk3(sk17,sk18,X0))
| is_a_cluster_point_of_netstr(sk17,sk18,X0)
| ~ element(X0,the_carrier(sk17))
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p171,c65]) ).
cnf(p191,plain,
( ~ is_often_in(sk17,sk18,sk3(sk17,sk18,sk19))
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p190,c66]) ).
cnf(p720,plain,
( is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17)
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p718,p191]) ).
cnf(p723,plain,
( empty_carrier(sk18)
| empty_carrier(sk17)
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p720]) ).
cnf(p724,plain,
( empty_carrier(sk18)
| is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p723]) ).
cnf(p726,plain,
( is_a_cluster_point_of_netstr(sk17,sk18,sk19)
| empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(factoring,[status(thm)],[p724]) ).
cnf(c68,plain,
~ is_a_cluster_point_of_netstr(sk17,sk18,sk19),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p728,plain,
( empty_carrier(sk18)
| empty_carrier(sk17) ),
inference(resolution,[status(thm)],[p726,c68]) ).
cnf(c62,plain,
~ empty_carrier(sk18),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p729,plain,
empty_carrier(sk17),
inference(resolution,[status(thm)],[p728,c62]) ).
cnf(c59,plain,
~ empty_carrier(sk17),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p730,plain,
$false,
inference(resolution,[status(thm)],[p729,c59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 13:56:28 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 13.05/2.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.05/2.26 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------