%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU392+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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 : Tue Sep 29 12:48:41 PM UTC 2026
% Result : Theorem 22.85s 4.95s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 32
% Syntax : Number of formulae : 341 ( 36 unt; 13 def)
% Number of atoms : 1705 ( 76 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 2302 ( 938 ~;1141 |; 151 &)
% ( 35 <=>; 35 =>; 0 <=; 2 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 11 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-3 aty)
% Number of variables : 473 ( 0 sgn 443 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f122,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,powerset(the_carrier(X0)))
=> ( X2 = lim_points_of_net(X0,X1)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X2)
<=> ! [X4] :
( point_neighbourhood(X4,X0,X3)
=> is_eventually_in(X0,X1,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d18_yellow_6) ).
fof(f146,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> neighborhood_system(X0,X1) = a_2_0_yellow19(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_yellow19) ).
fof(f167,axiom,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_yellow_1) ).
fof(f175,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f197,axiom,
! [X0] :
( ( topological_space(X0)
& top_str(X0) )
=> ! [X1,X2] :
( is_a_convergence_point_of_set(X0,X1,X2)
<=> ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( ( open_subset(X3,X0)
& in(X2,X3) )
=> in(X3,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_waybel_7) ).
fof(f235,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_yellow_6) ).
fof(f274,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& net_str(X1,X0) )
=> element(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_yellow19) ).
fof(f324,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f411,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ( ~ empty(filter_of_net_str(X0,X1))
& upper_relstr_subset(filter_of_net_str(X0,X1),boole_POSet(cast_as_carrier_subset(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_yellow19) ).
fof(f470,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& element(X2,the_carrier(X1)) )
=> ( in(X0,a_2_0_yellow19(X1,X2))
<=> ? [X3] :
( point_neighbourhood(X3,X1,X2)
& X0 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_2_0_yellow19) ).
fof(f582,axiom,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f678,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( in(X2,filter_of_net_str(X0,X1))
<=> ( is_eventually_in(X0,X1,X2)
& element(X2,powerset(the_carrier(X0))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_yellow19) ).
fof(f679,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f688,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_yellow19) ).
fof(f689,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f688]) ).
fof(f809,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( in(X2,neighborhood_system(X0,X1))
<=> point_neighbourhood(X2,X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_yellow19) ).
fof(f835,axiom,
! [X0,X1,X2] :
( ( in(X0,X1)
& element(X1,powerset(X2)) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f836,axiom,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_waybel_7) ).
fof(f839,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( ( upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X0)))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> ( is_a_convergence_point_of_set(X0,X2,X1)
<=> subset(neighborhood_system(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_yellow19) ).
fof(f853,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( ( open_subset(X1,X0)
& in(X2,X1) )
=> point_neighbourhood(X1,X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_connsp_2) ).
fof(f1173,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = lim_points_of_net(X0,X1)
<=> ! [X3] :
( ( in(X3,X2)
<=> ! [X4] :
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3) ) )
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f1174,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = lim_points_of_net(X0,X1)
<=> ! [X3] :
( ( in(X3,X2)
<=> ! [X4] :
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3) ) )
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f1173]) ).
fof(f1203,plain,
! [X0] :
( ! [X1] :
( neighborhood_system(X0,X1) = a_2_0_yellow19(X0,X1)
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f146]) ).
fof(f1204,plain,
! [X0] :
( ! [X1] :
( neighborhood_system(X0,X1) = a_2_0_yellow19(X0,X1)
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f1203]) ).
fof(f1238,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f175]) ).
fof(f1259,plain,
! [X0] :
( ! [X1,X2] :
( is_a_convergence_point_of_set(X0,X1,X2)
<=> ! [X3] :
( in(X3,X1)
| ~ open_subset(X3,X0)
| ~ in(X2,X3)
| ~ element(X3,powerset(the_carrier(X0))) ) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f197]) ).
fof(f1260,plain,
! [X0] :
( ! [X1,X2] :
( is_a_convergence_point_of_set(X0,X1,X2)
<=> ! [X3] :
( in(X3,X1)
| ~ open_subset(X3,X0)
| ~ in(X2,X3)
| ~ element(X3,powerset(the_carrier(X0))) ) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f1259]) ).
fof(f1314,plain,
! [X0,X1] :
( element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f235]) ).
fof(f1315,plain,
! [X0,X1] :
( element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1314]) ).
fof(f1347,plain,
! [X0,X1] :
( element(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f274]) ).
fof(f1348,plain,
! [X0,X1] :
( element(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1347]) ).
fof(f1408,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f324]) ).
fof(f1497,plain,
! [X0,X1] :
( ( ~ empty(filter_of_net_str(X0,X1))
& upper_relstr_subset(filter_of_net_str(X0,X1),boole_POSet(cast_as_carrier_subset(X0))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f411]) ).
fof(f1498,plain,
! [X0,X1] :
( ( ~ empty(filter_of_net_str(X0,X1))
& upper_relstr_subset(filter_of_net_str(X0,X1),boole_POSet(cast_as_carrier_subset(X0))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1497]) ).
fof(f1577,plain,
! [X0,X1,X2] :
( ( in(X0,a_2_0_yellow19(X1,X2))
<=> ? [X3] :
( point_neighbourhood(X3,X1,X2)
& X0 = X3 ) )
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(ennf_transformation,[],[f470]) ).
fof(f1578,plain,
! [X0,X1,X2] :
( ( in(X0,a_2_0_yellow19(X1,X2))
<=> ? [X3] :
( point_neighbourhood(X3,X1,X2)
& X0 = X3 ) )
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(flattening,[],[f1577]) ).
fof(f1816,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( in(X2,filter_of_net_str(X0,X1))
<=> ( is_eventually_in(X0,X1,X2)
& element(X2,powerset(the_carrier(X0))) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f678]) ).
fof(f1817,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( in(X2,filter_of_net_str(X0,X1))
<=> ( is_eventually_in(X0,X1,X2)
& element(X2,powerset(the_carrier(X0))) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1816]) ).
fof(f1818,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f679]) ).
fof(f1832,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( in(X2,lim_points_of_net(X0,X1))
<~> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
& element(X2,the_carrier(X0)) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(ennf_transformation,[],[f689]) ).
fof(f1833,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( in(X2,lim_points_of_net(X0,X1))
<~> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
& element(X2,the_carrier(X0)) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(flattening,[],[f1832]) ).
fof(f1993,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( in(X2,neighborhood_system(X0,X1))
<=> point_neighbourhood(X2,X0,X1) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f809]) ).
fof(f1994,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( in(X2,neighborhood_system(X0,X1))
<=> point_neighbourhood(X2,X0,X1) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f1993]) ).
fof(f2031,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(ennf_transformation,[],[f835]) ).
fof(f2032,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(flattening,[],[f2031]) ).
fof(f2035,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_a_convergence_point_of_set(X0,X2,X1)
<=> subset(neighborhood_system(X0,X1),X2) )
| ~ upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f839]) ).
fof(f2036,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_a_convergence_point_of_set(X0,X2,X1)
<=> subset(neighborhood_system(X0,X1),X2) )
| ~ upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f2035]) ).
fof(f2061,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( point_neighbourhood(X1,X0,X2)
| ~ open_subset(X1,X0)
| ~ in(X2,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f853]) ).
fof(f2062,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( point_neighbourhood(X1,X0,X2)
| ~ open_subset(X1,X0)
| ~ in(X2,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f2061]) ).
fof(f2335,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = lim_points_of_net(X0,X1)
| ? [X3] :
( ( ? [X4] :
( ~ is_eventually_in(X0,X1,X4)
& point_neighbourhood(X4,X0,X3) )
| ~ in(X3,X2) )
& ( ! [X4] :
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3) )
| in(X3,X2) )
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( ( ( in(X3,X2)
| ? [X4] :
( ~ is_eventually_in(X0,X1,X4)
& point_neighbourhood(X4,X0,X3) ) )
& ( ! [X4] :
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3) )
| ~ in(X3,X2) ) )
| ~ element(X3,the_carrier(X0)) )
| lim_points_of_net(X0,X1) != X2 ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f1174]) ).
fof(f2336,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = lim_points_of_net(X0,X1)
| ? [X3] :
( ( ? [X4] :
( ~ is_eventually_in(X0,X1,X4)
& point_neighbourhood(X4,X0,X3) )
| ~ in(X3,X2) )
& ( ! [X4] :
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3) )
| in(X3,X2) )
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( ( ( in(X3,X2)
| ? [X4] :
( ~ is_eventually_in(X0,X1,X4)
& point_neighbourhood(X4,X0,X3) ) )
& ( ! [X4] :
( is_eventually_in(X0,X1,X4)
| ~ point_neighbourhood(X4,X0,X3) )
| ~ in(X3,X2) ) )
| ~ element(X3,the_carrier(X0)) )
| lim_points_of_net(X0,X1) != X2 ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f2335]) ).
fof(f2337,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = lim_points_of_net(X0,X1)
| ? [X3] :
( ( ? [X4] :
( ~ is_eventually_in(X0,X1,X4)
& point_neighbourhood(X4,X0,X3) )
| ~ in(X3,X2) )
& ( ! [X5] :
( is_eventually_in(X0,X1,X5)
| ~ point_neighbourhood(X5,X0,X3) )
| in(X3,X2) )
& element(X3,the_carrier(X0)) ) )
& ( ! [X6] :
( ( ( in(X6,X2)
| ? [X7] :
( ~ is_eventually_in(X0,X1,X7)
& point_neighbourhood(X7,X0,X6) ) )
& ( ! [X8] :
( is_eventually_in(X0,X1,X8)
| ~ point_neighbourhood(X8,X0,X6) )
| ~ in(X6,X2) ) )
| ~ element(X6,the_carrier(X0)) )
| lim_points_of_net(X0,X1) != X2 ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(rectify,[],[f2336]) ).
fof(f2338,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = lim_points_of_net(X0,X1)
| ( ( ( ~ is_eventually_in(X0,X1,sK114(X0,X1,X2))
& point_neighbourhood(sK114(X0,X1,X2),X0,sK113(X0,X1,X2)) )
| ~ in(sK113(X0,X1,X2),X2) )
& ( ! [X5] :
( is_eventually_in(X0,X1,X5)
| ~ point_neighbourhood(X5,X0,sK113(X0,X1,X2)) )
| in(sK113(X0,X1,X2),X2) )
& element(sK113(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X6] :
( ( ( in(X6,X2)
| ( ~ is_eventually_in(X0,X1,sK115(X0,X1,X6))
& point_neighbourhood(sK115(X0,X1,X6),X0,X6) ) )
& ( ! [X8] :
( is_eventually_in(X0,X1,X8)
| ~ point_neighbourhood(X8,X0,X6) )
| ~ in(X6,X2) ) )
| ~ element(X6,the_carrier(X0)) )
| lim_points_of_net(X0,X1) != X2 ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK113,sK114,sK115]),skolemize(X3,sK113(X0,X1,X2)),skolemize(X4,sK114(X0,X1,X2)),skolemize(X7,sK115(X0,X1,X6))],[f2337]) ).
fof(f2455,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f1238]) ).
fof(f2456,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f2455]) ).
fof(f2457,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK174(X0,X1),X1)
& in(sK174(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK174]),skolemize(X2,sK174(X0,X1))],[f2456]) ).
fof(f2501,plain,
! [X0] :
( ! [X1,X2] :
( ( is_a_convergence_point_of_set(X0,X1,X2)
| ? [X3] :
( ~ in(X3,X1)
& open_subset(X3,X0)
& in(X2,X3)
& element(X3,powerset(the_carrier(X0))) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ open_subset(X3,X0)
| ~ in(X2,X3)
| ~ element(X3,powerset(the_carrier(X0))) )
| ~ is_a_convergence_point_of_set(X0,X1,X2) ) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f1260]) ).
fof(f2502,plain,
! [X0] :
( ! [X1,X2] :
( ( is_a_convergence_point_of_set(X0,X1,X2)
| ? [X3] :
( ~ in(X3,X1)
& open_subset(X3,X0)
& in(X2,X3)
& element(X3,powerset(the_carrier(X0))) ) )
& ( ! [X4] :
( in(X4,X1)
| ~ open_subset(X4,X0)
| ~ in(X2,X4)
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ is_a_convergence_point_of_set(X0,X1,X2) ) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(rectify,[],[f2501]) ).
fof(f2503,plain,
! [X0] :
( ! [X1,X2] :
( ( is_a_convergence_point_of_set(X0,X1,X2)
| ( ~ in(sK196(X0,X1,X2),X1)
& open_subset(sK196(X0,X1,X2),X0)
& in(X2,sK196(X0,X1,X2))
& element(sK196(X0,X1,X2),powerset(the_carrier(X0))) ) )
& ( ! [X4] :
( in(X4,X1)
| ~ open_subset(X4,X0)
| ~ in(X2,X4)
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ is_a_convergence_point_of_set(X0,X1,X2) ) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK196]),skolemize(X3,sK196(X0,X1,X2))],[f2502]) ).
fof(f2599,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_0_yellow19(X1,X2))
| ! [X3] :
( ~ point_neighbourhood(X3,X1,X2)
| X0 != X3 ) )
& ( ? [X3] :
( point_neighbourhood(X3,X1,X2)
& X0 = X3 )
| ~ in(X0,a_2_0_yellow19(X1,X2)) ) )
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(nnf_transformation,[],[f1578]) ).
fof(f2600,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_0_yellow19(X1,X2))
| ! [X3] :
( ~ point_neighbourhood(X3,X1,X2)
| X0 != X3 ) )
& ( ? [X4] :
( point_neighbourhood(X4,X1,X2)
& X0 = X4 )
| ~ in(X0,a_2_0_yellow19(X1,X2)) ) )
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(rectify,[],[f2599]) ).
fof(f2601,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_0_yellow19(X1,X2))
| ! [X3] :
( ~ point_neighbourhood(X3,X1,X2)
| X0 != X3 ) )
& ( ( point_neighbourhood(sK250(X0,X1,X2),X1,X2)
& sK250(X0,X1,X2) = X0 )
| ~ in(X0,a_2_0_yellow19(X1,X2)) ) )
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK250]),skolemize(X4,sK250(X0,X1,X2))],[f2600]) ).
fof(f2990,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,filter_of_net_str(X0,X1))
| ~ is_eventually_in(X0,X1,X2)
| ~ element(X2,powerset(the_carrier(X0))) )
& ( ( is_eventually_in(X0,X1,X2)
& element(X2,powerset(the_carrier(X0))) )
| ~ in(X2,filter_of_net_str(X0,X1)) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f1817]) ).
fof(f2991,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,filter_of_net_str(X0,X1))
| ~ is_eventually_in(X0,X1,X2)
| ~ element(X2,powerset(the_carrier(X0))) )
& ( ( is_eventually_in(X0,X1,X2)
& element(X2,powerset(the_carrier(X0))) )
| ~ in(X2,filter_of_net_str(X0,X1)) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f2990]) ).
fof(f2997,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| ~ in(X2,lim_points_of_net(X0,X1)) )
& ( is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1)) )
& element(X2,the_carrier(X0)) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(nnf_transformation,[],[f1833]) ).
fof(f2998,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| ~ in(X2,lim_points_of_net(X0,X1)) )
& ( is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1)) )
& element(X2,the_carrier(X0)) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(flattening,[],[f2997]) ).
fof(f2999,plain,
( ( ~ is_a_convergence_point_of_set(sK603,filter_of_net_str(sK603,sK604),sK605)
| ~ in(sK605,lim_points_of_net(sK603,sK604)) )
& ( is_a_convergence_point_of_set(sK603,filter_of_net_str(sK603,sK604),sK605)
| in(sK605,lim_points_of_net(sK603,sK604)) )
& element(sK605,the_carrier(sK603))
& ~ empty_carrier(sK604)
& transitive_relstr(sK604)
& directed_relstr(sK604)
& net_str(sK604,sK603)
& ~ empty_carrier(sK603)
& topological_space(sK603)
& top_str(sK603) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK603,sK604,sK605]),skolemize(X0,sK603),skolemize(X1,sK604),skolemize(X2,sK605)],[f2998]) ).
fof(f3064,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,neighborhood_system(X0,X1))
| ~ point_neighbourhood(X2,X0,X1) )
& ( point_neighbourhood(X2,X0,X1)
| ~ in(X2,neighborhood_system(X0,X1)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f1994]) ).
fof(f3080,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( is_a_convergence_point_of_set(X0,X2,X1)
| ~ subset(neighborhood_system(X0,X1),X2) )
& ( subset(neighborhood_system(X0,X1),X2)
| ~ is_a_convergence_point_of_set(X0,X2,X1) ) )
| ~ upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f2036]) ).
fof(f3548,plain,
! [X2,X0,X1,X8,X6] :
( is_eventually_in(X0,X1,X8)
| ~ point_neighbourhood(X8,X0,X6)
| ~ in(X6,X2)
| ~ element(X6,the_carrier(X0))
| lim_points_of_net(X0,X1) != X2
| ~ element(X2,powerset(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2338]) ).
fof(f3549,plain,
! [X2,X0,X1,X6] :
( in(X6,X2)
| point_neighbourhood(sK115(X0,X1,X6),X0,X6)
| ~ element(X6,the_carrier(X0))
| lim_points_of_net(X0,X1) != X2
| ~ element(X2,powerset(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2338]) ).
fof(f3550,plain,
! [X2,X0,X1,X6] :
( in(X6,X2)
| ~ is_eventually_in(X0,X1,sK115(X0,X1,X6))
| ~ element(X6,the_carrier(X0))
| lim_points_of_net(X0,X1) != X2
| ~ element(X2,powerset(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2338]) ).
fof(f3658,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| neighborhood_system(X0,X1) = a_2_0_yellow19(X0,X1)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f1204]) ).
fof(f3732,plain,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
inference(cnf_transformation,[],[f167]) ).
fof(f3762,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f2457]) ).
fof(f3848,plain,
! [X2,X0,X1] :
( is_a_convergence_point_of_set(X0,X1,X2)
| element(sK196(X0,X1,X2),powerset(the_carrier(X0)))
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2503]) ).
fof(f3849,plain,
! [X2,X0,X1] :
( in(X2,sK196(X0,X1,X2))
| is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2503]) ).
fof(f3850,plain,
! [X2,X0,X1] :
( open_subset(sK196(X0,X1,X2),X0)
| is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2503]) ).
fof(f3851,plain,
! [X2,X0,X1] :
( ~ in(sK196(X0,X1,X2),X1)
| is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2503]) ).
fof(f4005,plain,
! [X0,X1] :
( element(lim_points_of_net(X0,X1),powerset(the_carrier(X0)))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1315]) ).
fof(f4040,plain,
! [X0,X1] :
( element(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1348]) ).
fof(f4097,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1408]) ).
fof(f4337,plain,
! [X0,X1] :
( upper_relstr_subset(filter_of_net_str(X0,X1),boole_POSet(cast_as_carrier_subset(X0)))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1498]) ).
fof(f4559,plain,
! [X2,X0,X1] :
( ~ in(X0,a_2_0_yellow19(X1,X2))
| sK250(X0,X1,X2) = X0
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f2601]) ).
fof(f4560,plain,
! [X2,X0,X1] :
( point_neighbourhood(sK250(X0,X1,X2),X1,X2)
| ~ in(X0,a_2_0_yellow19(X1,X2))
| empty_carrier(X1)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f2601]) ).
fof(f5067,plain,
! [X0] : powerset(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f582]) ).
fof(f5647,plain,
! [X2,X0,X1] :
( ~ in(X2,filter_of_net_str(X0,X1))
| is_eventually_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2991]) ).
fof(f5648,plain,
! [X2,X0,X1] :
( in(X2,filter_of_net_str(X0,X1))
| ~ is_eventually_in(X0,X1,X2)
| ~ element(X2,powerset(the_carrier(X0)))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2991]) ).
fof(f5649,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f1818]) ).
fof(f5667,plain,
top_str(sK603),
inference(cnf_transformation,[],[f2999]) ).
fof(f5668,plain,
topological_space(sK603),
inference(cnf_transformation,[],[f2999]) ).
fof(f5669,plain,
~ empty_carrier(sK603),
inference(cnf_transformation,[],[f2999]) ).
fof(f5670,plain,
net_str(sK604,sK603),
inference(cnf_transformation,[],[f2999]) ).
fof(f5671,plain,
directed_relstr(sK604),
inference(cnf_transformation,[],[f2999]) ).
fof(f5672,plain,
transitive_relstr(sK604),
inference(cnf_transformation,[],[f2999]) ).
fof(f5673,plain,
~ empty_carrier(sK604),
inference(cnf_transformation,[],[f2999]) ).
fof(f5674,plain,
element(sK605,the_carrier(sK603)),
inference(cnf_transformation,[],[f2999]) ).
fof(f5675,plain,
( is_a_convergence_point_of_set(sK603,filter_of_net_str(sK603,sK604),sK605)
| in(sK605,lim_points_of_net(sK603,sK604)) ),
inference(cnf_transformation,[],[f2999]) ).
fof(f5676,plain,
( ~ is_a_convergence_point_of_set(sK603,filter_of_net_str(sK603,sK604),sK605)
| ~ in(sK605,lim_points_of_net(sK603,sK604)) ),
inference(cnf_transformation,[],[f2999]) ).
fof(f5891,plain,
! [X2,X0,X1] :
( in(X2,neighborhood_system(X0,X1))
| ~ point_neighbourhood(X2,X0,X1)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f3064]) ).
fof(f5936,plain,
! [X2,X0,X1] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(cnf_transformation,[],[f2032]) ).
fof(f5937,plain,
! [X0] : powerset(X0) = the_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f836]) ).
fof(f5941,plain,
! [X2,X0,X1] :
( subset(neighborhood_system(X0,X1),X2)
| ~ is_a_convergence_point_of_set(X0,X2,X1)
| ~ upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f3080]) ).
fof(f5979,plain,
! [X2,X0,X1] :
( point_neighbourhood(X1,X0,X2)
| ~ open_subset(X1,X0)
| ~ in(X2,X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,powerset(the_carrier(X0)))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2062]) ).
fof(f6135,plain,
! [X2,X0,X1,X6] :
( in(X6,X2)
| ~ is_eventually_in(X0,X1,sK115(X0,X1,X6))
| ~ element(X6,the_carrier(X0))
| lim_points_of_net(X0,X1) != X2
| ~ element(X2,k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(definition_unfolding,[],[f3550,f5067]) ).
fof(f6136,plain,
! [X2,X0,X1,X6] :
( in(X6,X2)
| point_neighbourhood(sK115(X0,X1,X6),X0,X6)
| ~ element(X6,the_carrier(X0))
| lim_points_of_net(X0,X1) != X2
| ~ element(X2,k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(definition_unfolding,[],[f3549,f5067]) ).
fof(f6137,plain,
! [X2,X0,X1,X8,X6] :
( is_eventually_in(X0,X1,X8)
| ~ point_neighbourhood(X8,X0,X6)
| ~ in(X6,X2)
| ~ element(X6,the_carrier(X0))
| lim_points_of_net(X0,X1) != X2
| ~ element(X2,k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(definition_unfolding,[],[f3548,f5067]) ).
fof(f6242,plain,
! [X2,X0,X1] :
( element(sK196(X0,X1,X2),k1_pcomps_1(the_carrier(X0)))
| is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(definition_unfolding,[],[f3848,f5067]) ).
fof(f6283,plain,
! [X0,X1] :
( element(lim_points_of_net(X0,X1),k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(definition_unfolding,[],[f4005,f5067]) ).
fof(f6292,plain,
! [X0,X1] :
( element(filter_of_net_str(X0,X1),k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(definition_unfolding,[],[f4040,f5067,f3732]) ).
fof(f6408,plain,
! [X0,X1] :
( upper_relstr_subset(filter_of_net_str(X0,X1),poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(definition_unfolding,[],[f4337,f3732]) ).
fof(f6853,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(the_carrier(X0)))
| ~ is_eventually_in(X0,X1,X2)
| in(X2,filter_of_net_str(X0,X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(definition_unfolding,[],[f5648,f5067]) ).
fof(f6948,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(definition_unfolding,[],[f5936,f5067]) ).
fof(f6949,plain,
! [X0] : k1_pcomps_1(X0) = the_carrier(poset_of_lattice(boole_lattice(X0))),
inference(definition_unfolding,[],[f5937,f5067,f3732]) ).
fof(f6954,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| ~ is_a_convergence_point_of_set(X0,X2,X1)
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| subset(neighborhood_system(X0,X1),X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(definition_unfolding,[],[f5941,f3732,f5067,f3732]) ).
fof(f6964,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ open_subset(X1,X0)
| ~ in(X2,X1)
| ~ element(X2,the_carrier(X0))
| point_neighbourhood(X1,X0,X2)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(definition_unfolding,[],[f5979,f5067]) ).
fof(f7032,plain,
! [X0,X1,X6] :
( in(X6,lim_points_of_net(X0,X1))
| ~ is_eventually_in(X0,X1,sK115(X0,X1,X6))
| ~ element(X6,the_carrier(X0))
| ~ element(lim_points_of_net(X0,X1),k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(equality_resolution,[],[f6135]) ).
fof(f7033,plain,
! [X0,X1,X6] :
( in(X6,lim_points_of_net(X0,X1))
| point_neighbourhood(sK115(X0,X1,X6),X0,X6)
| ~ element(X6,the_carrier(X0))
| ~ element(lim_points_of_net(X0,X1),k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(equality_resolution,[],[f6136]) ).
fof(f7034,plain,
! [X0,X1,X8,X6] :
( is_eventually_in(X0,X1,X8)
| ~ point_neighbourhood(X8,X0,X6)
| ~ in(X6,lim_points_of_net(X0,X1))
| ~ element(X6,the_carrier(X0))
| ~ element(lim_points_of_net(X0,X1),k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(equality_resolution,[],[f6137]) ).
fof(f7296,definition,
sF644 = filter_of_net_str(sK603,sK604),
introduced(definition,[new_symbols(definition,[sF644])],[function_definition]) ).
fof(f7297,plain,
filter_of_net_str(sK603,sK604) = sF644,
inference(reorient_equations,[],[f7296]) ).
fof(f7298,definition,
sF645 = lim_points_of_net(sK603,sK604),
introduced(definition,[new_symbols(definition,[sF645])],[function_definition]) ).
fof(f7299,plain,
lim_points_of_net(sK603,sK604) = sF645,
inference(reorient_equations,[],[f7298]) ).
fof(f7300,plain,
( ~ is_a_convergence_point_of_set(sK603,sF644,sK605)
| ~ in(sK605,sF645) ),
inference(definition_folding,[],[f5676,f7299,f7297]) ).
fof(f7301,plain,
( is_a_convergence_point_of_set(sK603,sF644,sK605)
| in(sK605,sF645) ),
inference(definition_folding,[],[f5675,f7299,f7297]) ).
fof(f7302,definition,
sF646 = the_carrier(sK603),
introduced(definition,[new_symbols(definition,[sF646])],[function_definition]) ).
fof(f7303,plain,
the_carrier(sK603) = sF646,
inference(reorient_equations,[],[f7302]) ).
fof(f7304,plain,
element(sK605,sF646),
inference(definition_folding,[],[f5674,f7303]) ).
fof(f7357,definition,
( spl647_5
<=> in(sK605,sF645) ),
introduced(definition,[new_symbols(definition,[spl647_5])],[avatar_definition]) ).
fof(f7358,plain,
( ~ in(sK605,sF645)
| spl647_5 ),
inference(avatar_component_clause,[],[f7357]) ).
fof(f7359,plain,
( in(sK605,sF645)
| ~ spl647_5 ),
inference(avatar_component_clause,[],[f7357]) ).
fof(f7361,definition,
( spl647_6
<=> is_a_convergence_point_of_set(sK603,sF644,sK605) ),
introduced(definition,[new_symbols(definition,[spl647_6])],[avatar_definition]) ).
fof(f7362,plain,
( ~ is_a_convergence_point_of_set(sK603,sF644,sK605)
| spl647_6 ),
inference(avatar_component_clause,[],[f7361]) ).
fof(f7363,plain,
( is_a_convergence_point_of_set(sK603,sF644,sK605)
| ~ spl647_6 ),
inference(avatar_component_clause,[],[f7361]) ).
fof(f7364,plain,
( spl647_5
| spl647_6 ),
inference(avatar_split_clause,[],[f7301,f7361,f7357]) ).
fof(f7365,plain,
( ~ spl647_5
| ~ spl647_6 ),
inference(avatar_split_clause,[],[f7300,f7361,f7357]) ).
fof(f7640,plain,
! [X0,X1] :
( element(filter_of_net_str(X0,X1),k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(forward_demodulation,[],[f6292,f6949]) ).
fof(f7672,plain,
! [X0,X1,X8,X6] :
( is_eventually_in(X0,X1,X8)
| ~ point_neighbourhood(X8,X0,X6)
| ~ in(X6,lim_points_of_net(X0,X1))
| ~ element(lim_points_of_net(X0,X1),k1_pcomps_1(the_carrier(X0)))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(forward_subsumption_resolution,[],[f7034,f6948]) ).
fof(f7673,plain,
! [X0,X1,X6] :
( point_neighbourhood(sK115(X0,X1,X6),X0,X6)
| in(X6,lim_points_of_net(X0,X1))
| ~ element(X6,the_carrier(X0))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(forward_subsumption_resolution,[],[f7033,f6283]) ).
fof(f7674,plain,
! [X0,X1,X6] :
( ~ is_eventually_in(X0,X1,sK115(X0,X1,X6))
| in(X6,lim_points_of_net(X0,X1))
| ~ element(X6,the_carrier(X0))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(forward_subsumption_resolution,[],[f7032,f6283]) ).
fof(f7706,plain,
! [X0,X1,X8,X6] :
( ~ in(X6,lim_points_of_net(X0,X1))
| ~ point_neighbourhood(X8,X0,X6)
| is_eventually_in(X0,X1,X8)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(forward_subsumption_resolution,[],[f7672,f6283]) ).
fof(f7715,definition,
( spl647_61
<=> one_sorted_str(sK603) ),
introduced(definition,[new_symbols(definition,[spl647_61])],[avatar_definition]) ).
fof(f7716,plain,
( one_sorted_str(sK603)
| ~ spl647_61 ),
inference(avatar_component_clause,[],[f7715]) ).
fof(f7717,plain,
( ~ one_sorted_str(sK603)
| spl647_61 ),
inference(avatar_component_clause,[],[f7715]) ).
fof(f7723,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(superposition,[],[f7706,f7299]) ).
fof(f7724,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7723,f5673]) ).
fof(f7725,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7724,f5672]) ).
fof(f7726,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7725,f5671]) ).
fof(f7727,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7726,f5670]) ).
fof(f7728,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7727,f5669]) ).
fof(f7729,plain,
! [X0,X1] :
( ~ in(X0,sF645)
| ~ point_neighbourhood(X1,sK603,X0)
| is_eventually_in(sK603,sK604,X1)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7728,f5668]) ).
fof(f7730,plain,
! [X0,X1] :
( ~ point_neighbourhood(X1,sK603,X0)
| ~ in(X0,sF645)
| is_eventually_in(sK603,sK604,X1) ),
inference(forward_subsumption_resolution,[],[f7729,f5667]) ).
fof(f7731,plain,
( upper_relstr_subset(sF644,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK603))))
| empty_carrier(sK603)
| ~ one_sorted_str(sK603)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603) ),
inference(superposition,[],[f6408,f7297]) ).
fof(f7732,plain,
! [X0] :
( ~ in(X0,sF644)
| is_eventually_in(sK603,sK604,X0)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ one_sorted_str(sK603) ),
inference(superposition,[],[f5647,f7297]) ).
fof(f7753,plain,
( element(sF644,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK603))))
| empty_carrier(sK603)
| ~ one_sorted_str(sK603)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603) ),
inference(superposition,[],[f7640,f7297]) ).
fof(f7755,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603) ),
inference(superposition,[],[f6283,f7299]) ).
fof(f7770,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| ~ topological_space(sK603)
| ~ top_str(sK603)
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7755,f5669]) ).
fof(f7771,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| ~ top_str(sK603)
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7770,f5668]) ).
fof(f7772,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7771,f5667]) ).
fof(f7773,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7772,f5673]) ).
fof(f7774,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7773,f5672]) ).
fof(f7775,plain,
( element(sF645,k1_pcomps_1(the_carrier(sK603)))
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7774,f5671]) ).
fof(f7776,plain,
element(sF645,k1_pcomps_1(the_carrier(sK603))),
inference(forward_subsumption_resolution,[],[f7775,f5670]) ).
fof(f7777,plain,
element(sF645,k1_pcomps_1(sF646)),
inference(forward_demodulation,[],[f7776,f7303]) ).
fof(f7778,plain,
one_sorted_str(sK603),
inference(resolution,[],[f4097,f5667]) ).
fof(f7779,plain,
( $false
| spl647_61 ),
inference(forward_subsumption_resolution,[],[f7778,f7717]) ).
fof(f7780,plain,
spl647_61,
inference(avatar_contradiction_clause,[],[f7779]) ).
fof(f7781,plain,
( upper_relstr_subset(sF644,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK603))))
| ~ one_sorted_str(sK603)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7731,f5669]) ).
fof(f7782,plain,
! [X0] :
( ~ in(X0,sF644)
| is_eventually_in(sK603,sK604,X0)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ one_sorted_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7732,f5673]) ).
fof(f7785,plain,
( element(sF644,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK603))))
| ~ one_sorted_str(sK603)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603) ),
inference(forward_subsumption_resolution,[],[f7753,f5669]) ).
fof(f7786,plain,
( upper_relstr_subset(sF644,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK603))))
| empty_carrier(sK604)
| ~ net_str(sK604,sK603)
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7781,f7716]) ).
fof(f7787,plain,
! [X0] :
( ~ in(X0,sF644)
| is_eventually_in(sK603,sK604,X0)
| empty_carrier(sK603)
| ~ one_sorted_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7782,f5670]) ).
fof(f7790,plain,
( element(sF644,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK603))))
| empty_carrier(sK604)
| ~ net_str(sK604,sK603)
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7785,f7716]) ).
fof(f7791,plain,
( upper_relstr_subset(sF644,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK603))))
| ~ net_str(sK604,sK603)
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7786,f5673]) ).
fof(f7792,plain,
! [X0] :
( ~ in(X0,sF644)
| is_eventually_in(sK603,sK604,X0)
| ~ one_sorted_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7787,f5669]) ).
fof(f7795,plain,
( element(sF644,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK603))))
| ~ net_str(sK604,sK603)
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7790,f5673]) ).
fof(f7796,plain,
( upper_relstr_subset(sF644,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK603))))
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7791,f5670]) ).
fof(f7797,plain,
( ! [X0] :
( is_eventually_in(sK603,sK604,X0)
| ~ in(X0,sF644) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7792,f7716]) ).
fof(f7800,plain,
( element(sF644,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK603))))
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7795,f5670]) ).
fof(f7803,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(resolution,[],[f7797,f7674]) ).
fof(f7804,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7803,f5673]) ).
fof(f7805,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7804,f5672]) ).
fof(f7806,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7805,f5671]) ).
fof(f7807,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7806,f5670]) ).
fof(f7808,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7807,f5669]) ).
fof(f7809,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603))
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7808,f5668]) ).
fof(f7810,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,lim_points_of_net(sK603,sK604))
| ~ element(X0,the_carrier(sK603)) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f7809,f5667]) ).
fof(f7811,plain,
( ! [X0] :
( in(X0,sF645)
| ~ in(sK115(sK603,sK604,X0),sF644)
| ~ element(X0,the_carrier(sK603)) )
| ~ spl647_61 ),
inference(forward_demodulation,[],[f7810,f7299]) ).
fof(f7812,plain,
( ! [X0] :
( ~ in(sK115(sK603,sK604,X0),sF644)
| in(X0,sF645)
| ~ element(X0,sF646) )
| ~ spl647_61 ),
inference(forward_demodulation,[],[f7811,f7303]) ).
fof(f7856,plain,
! [X0] :
( ~ element(X0,sF646)
| neighborhood_system(sK603,X0) = a_2_0_yellow19(sK603,X0)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(superposition,[],[f3658,f7303]) ).
fof(f7857,plain,
! [X0] :
( ~ element(X0,sF646)
| neighborhood_system(sK603,X0) = a_2_0_yellow19(sK603,X0)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7856,f5669]) ).
fof(f7858,plain,
! [X0] :
( ~ element(X0,sF646)
| neighborhood_system(sK603,X0) = a_2_0_yellow19(sK603,X0)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7857,f5668]) ).
fof(f7859,plain,
! [X0] :
( ~ element(X0,sF646)
| neighborhood_system(sK603,X0) = a_2_0_yellow19(sK603,X0) ),
inference(forward_subsumption_resolution,[],[f7858,f5667]) ).
fof(f7860,plain,
neighborhood_system(sK603,sK605) = a_2_0_yellow19(sK603,sK605),
inference(resolution,[],[f7859,f7304]) ).
fof(f7874,plain,
! [X0] :
( ~ in(X0,neighborhood_system(sK603,sK605))
| sK250(X0,sK603,sK605) = X0
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ element(sK605,the_carrier(sK603)) ),
inference(superposition,[],[f4559,f7860]) ).
fof(f7875,plain,
! [X0] :
( ~ in(X0,neighborhood_system(sK603,sK605))
| sK250(X0,sK603,sK605) = X0
| ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ element(sK605,the_carrier(sK603)) ),
inference(forward_subsumption_resolution,[],[f7874,f5669]) ).
fof(f7876,plain,
! [X0] :
( ~ in(X0,neighborhood_system(sK603,sK605))
| sK250(X0,sK603,sK605) = X0
| ~ top_str(sK603)
| ~ element(sK605,the_carrier(sK603)) ),
inference(forward_subsumption_resolution,[],[f7875,f5668]) ).
fof(f7877,plain,
! [X0] :
( ~ in(X0,neighborhood_system(sK603,sK605))
| sK250(X0,sK603,sK605) = X0
| ~ element(sK605,the_carrier(sK603)) ),
inference(forward_subsumption_resolution,[],[f7876,f5667]) ).
fof(f7878,plain,
! [X0] :
( ~ element(sK605,sF646)
| ~ in(X0,neighborhood_system(sK603,sK605))
| sK250(X0,sK603,sK605) = X0 ),
inference(forward_demodulation,[],[f7877,f7303]) ).
fof(f7879,plain,
! [X0] :
( ~ in(X0,neighborhood_system(sK603,sK605))
| sK250(X0,sK603,sK605) = X0 ),
inference(forward_subsumption_resolution,[],[f7878,f7304]) ).
fof(f7880,plain,
! [X0] :
( sK250(X0,sK603,sK605) = X0
| ~ point_neighbourhood(X0,sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(resolution,[],[f7879,f5891]) ).
fof(f7881,plain,
! [X0] :
( sK250(X0,sK603,sK605) = X0
| ~ point_neighbourhood(X0,sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7880,f5669]) ).
fof(f7882,plain,
! [X0] :
( sK250(X0,sK603,sK605) = X0
| ~ point_neighbourhood(X0,sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f7881,f5668]) ).
fof(f7883,plain,
! [X0] :
( sK250(X0,sK603,sK605) = X0
| ~ point_neighbourhood(X0,sK603,sK605)
| ~ element(sK605,the_carrier(sK603)) ),
inference(forward_subsumption_resolution,[],[f7882,f5667]) ).
fof(f7884,plain,
! [X0] :
( ~ element(sK605,sF646)
| sK250(X0,sK603,sK605) = X0
| ~ point_neighbourhood(X0,sK603,sK605) ),
inference(forward_demodulation,[],[f7883,f7303]) ).
fof(f7885,plain,
! [X0] :
( ~ point_neighbourhood(X0,sK603,sK605)
| sK250(X0,sK603,sK605) = X0 ),
inference(forward_subsumption_resolution,[],[f7884,f7304]) ).
fof(f7899,plain,
( the_carrier(sK603) = cast_as_carrier_subset(sK603)
| ~ spl647_61 ),
inference(resolution,[],[f5649,f7716]) ).
fof(f7900,plain,
( sF646 = cast_as_carrier_subset(sK603)
| ~ spl647_61 ),
inference(forward_demodulation,[],[f7899,f7303]) ).
fof(f7901,plain,
( upper_relstr_subset(sF644,poset_of_lattice(boole_lattice(sF646)))
| ~ spl647_61 ),
inference(superposition,[],[f7796,f7900]) ).
fof(f7903,plain,
( element(sF644,k1_pcomps_1(k1_pcomps_1(sF646)))
| ~ spl647_61 ),
inference(superposition,[],[f7800,f7900]) ).
fof(f7987,plain,
! [X2,X3,X0,X1] :
( is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ open_subset(sK196(X0,X1,X2),X0)
| ~ in(X3,sK196(X0,X1,X2))
| ~ element(X3,the_carrier(X0))
| point_neighbourhood(sK196(X0,X1,X2),X0,X3)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(resolution,[],[f6242,f6964]) ).
fof(f7988,plain,
! [X2,X3,X0,X1] :
( is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ is_eventually_in(X0,X3,sK196(X0,X1,X2))
| in(sK196(X0,X1,X2),filter_of_net_str(X0,X3))
| empty_carrier(X3)
| ~ net_str(X3,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f6242,f6853]) ).
fof(f7993,plain,
! [X2,X3,X0,X1] :
( is_a_convergence_point_of_set(X0,X1,X2)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ open_subset(sK196(X0,X1,X2),X0)
| ~ in(X3,sK196(X0,X1,X2))
| ~ element(X3,the_carrier(X0))
| point_neighbourhood(sK196(X0,X1,X2),X0,X3)
| empty_carrier(X0) ),
inference(duplicate_literal_removal,[],[f7987]) ).
fof(f7997,plain,
! [X2,X3,X0,X1] :
( in(sK196(X0,X1,X2),filter_of_net_str(X0,X3))
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ is_eventually_in(X0,X3,sK196(X0,X1,X2))
| is_a_convergence_point_of_set(X0,X1,X2)
| empty_carrier(X3)
| ~ net_str(X3,X0)
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[],[f7988,f4097]) ).
fof(f7998,plain,
! [X2,X3,X0,X1] :
( point_neighbourhood(sK196(X0,X1,X2),X0,X3)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ in(X3,sK196(X0,X1,X2))
| ~ element(X3,the_carrier(X0))
| is_a_convergence_point_of_set(X0,X1,X2)
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[],[f7993,f3850]) ).
fof(f8030,plain,
! [X0,X1] :
( ~ in(X0,a_2_0_yellow19(sK603,X1))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ element(X1,the_carrier(sK603))
| ~ in(X1,sF645)
| is_eventually_in(sK603,sK604,sK250(X0,sK603,X1)) ),
inference(resolution,[],[f4560,f7730]) ).
fof(f8036,plain,
! [X0,X1] :
( ~ in(X0,a_2_0_yellow19(sK603,X1))
| ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ element(X1,the_carrier(sK603))
| ~ in(X1,sF645)
| is_eventually_in(sK603,sK604,sK250(X0,sK603,X1)) ),
inference(forward_subsumption_resolution,[],[f8030,f5669]) ).
fof(f8038,plain,
! [X0,X1] :
( ~ in(X0,a_2_0_yellow19(sK603,X1))
| ~ top_str(sK603)
| ~ element(X1,the_carrier(sK603))
| ~ in(X1,sF645)
| is_eventually_in(sK603,sK604,sK250(X0,sK603,X1)) ),
inference(forward_subsumption_resolution,[],[f8036,f5668]) ).
fof(f8040,plain,
! [X0,X1] :
( ~ in(X0,a_2_0_yellow19(sK603,X1))
| ~ element(X1,the_carrier(sK603))
| ~ in(X1,sF645)
| is_eventually_in(sK603,sK604,sK250(X0,sK603,X1)) ),
inference(forward_subsumption_resolution,[],[f8038,f5667]) ).
fof(f8042,plain,
! [X0,X1] :
( is_eventually_in(sK603,sK604,sK250(X0,sK603,X1))
| ~ in(X0,a_2_0_yellow19(sK603,X1))
| ~ in(X1,sF645)
| ~ element(X1,sF646) ),
inference(forward_demodulation,[],[f8040,f7303]) ).
fof(f8075,plain,
! [X0,X1] :
( in(sK196(sK603,X0,X1),sF644)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ is_eventually_in(sK603,sK604,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603) ),
inference(superposition,[],[f7997,f7297]) ).
fof(f8079,plain,
! [X0,X1] :
( in(sK196(sK603,X0,X1),sF644)
| ~ top_str(sK603)
| ~ is_eventually_in(sK603,sK604,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603) ),
inference(forward_subsumption_resolution,[],[f8075,f5668]) ).
fof(f8080,plain,
! [X0,X1] :
( in(sK196(sK603,X0,X1),sF644)
| ~ is_eventually_in(sK603,sK604,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603) ),
inference(forward_subsumption_resolution,[],[f8079,f5667]) ).
fof(f8081,plain,
! [X0,X1] :
( in(sK196(sK603,X0,X1),sF644)
| ~ is_eventually_in(sK603,sK604,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603) ),
inference(forward_subsumption_resolution,[],[f8080,f5673]) ).
fof(f8082,plain,
! [X0,X1] :
( in(sK196(sK603,X0,X1),sF644)
| ~ is_eventually_in(sK603,sK604,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK603) ),
inference(forward_subsumption_resolution,[],[f8081,f5670]) ).
fof(f8083,plain,
! [X0,X1] :
( ~ is_eventually_in(sK603,sK604,sK196(sK603,X0,X1))
| in(sK196(sK603,X0,X1),sF644)
| is_a_convergence_point_of_set(sK603,X0,X1) ),
inference(forward_subsumption_resolution,[],[f8082,f5669]) ).
fof(f8099,plain,
! [X2,X3,X0,X1] :
( ~ in(X0,sK196(X1,X2,X3))
| element(X0,the_carrier(X1))
| is_a_convergence_point_of_set(X1,X2,X3)
| ~ topological_space(X1)
| ~ top_str(X1) ),
inference(resolution,[],[f6948,f6242]) ).
fof(f8103,plain,
! [X0] :
( ~ in(X0,sF645)
| element(X0,sF646) ),
inference(resolution,[],[f6948,f7777]) ).
fof(f8405,plain,
! [X0,X1] :
( ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ in(sK605,sK196(sK603,X0,X1))
| ~ element(sK605,the_carrier(sK603))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK603)
| sK196(sK603,X0,X1) = sK250(sK196(sK603,X0,X1),sK603,sK605) ),
inference(resolution,[],[f7998,f7885]) ).
fof(f8409,plain,
! [X0,X1] :
( ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ in(sK605,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK603)
| sK196(sK603,X0,X1) = sK250(sK196(sK603,X0,X1),sK603,sK605) ),
inference(forward_subsumption_resolution,[],[f8405,f8099]) ).
fof(f8411,plain,
! [X0,X1] :
( ~ top_str(sK603)
| ~ in(sK605,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK603)
| sK196(sK603,X0,X1) = sK250(sK196(sK603,X0,X1),sK603,sK605) ),
inference(forward_subsumption_resolution,[],[f8409,f5668]) ).
fof(f8413,plain,
! [X0,X1] :
( ~ in(sK605,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| empty_carrier(sK603)
| sK196(sK603,X0,X1) = sK250(sK196(sK603,X0,X1),sK603,sK605) ),
inference(forward_subsumption_resolution,[],[f8411,f5667]) ).
fof(f8415,plain,
! [X0,X1] :
( ~ in(sK605,sK196(sK603,X0,X1))
| is_a_convergence_point_of_set(sK603,X0,X1)
| sK196(sK603,X0,X1) = sK250(sK196(sK603,X0,X1),sK603,sK605) ),
inference(forward_subsumption_resolution,[],[f8413,f5669]) ).
fof(f8423,plain,
! [X0] :
( is_a_convergence_point_of_set(sK603,X0,sK605)
| sK196(sK603,X0,sK605) = sK250(sK196(sK603,X0,sK605),sK603,sK605)
| is_a_convergence_point_of_set(sK603,X0,sK605)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(resolution,[],[f8415,f3849]) ).
fof(f8424,plain,
! [X0] :
( is_a_convergence_point_of_set(sK603,X0,sK605)
| sK196(sK603,X0,sK605) = sK250(sK196(sK603,X0,sK605),sK603,sK605)
| ~ topological_space(sK603)
| ~ top_str(sK603) ),
inference(duplicate_literal_removal,[],[f8423]) ).
fof(f8425,plain,
! [X0] :
( is_a_convergence_point_of_set(sK603,X0,sK605)
| sK196(sK603,X0,sK605) = sK250(sK196(sK603,X0,sK605),sK603,sK605)
| ~ top_str(sK603) ),
inference(forward_subsumption_resolution,[],[f8424,f5668]) ).
fof(f8426,plain,
! [X0] :
( is_a_convergence_point_of_set(sK603,X0,sK605)
| sK196(sK603,X0,sK605) = sK250(sK196(sK603,X0,sK605),sK603,sK605) ),
inference(forward_subsumption_resolution,[],[f8425,f5667]) ).
fof(f8427,plain,
( sK196(sK603,sF644,sK605) = sK250(sK196(sK603,sF644,sK605),sK603,sK605)
| spl647_6 ),
inference(resolution,[],[f8426,f7362]) ).
fof(f8430,plain,
( is_eventually_in(sK603,sK604,sK196(sK603,sF644,sK605))
| ~ in(sK196(sK603,sF644,sK605),a_2_0_yellow19(sK603,sK605))
| ~ in(sK605,sF645)
| ~ element(sK605,sF646)
| spl647_6 ),
inference(superposition,[],[f8042,f8427]) ).
fof(f8433,plain,
( is_eventually_in(sK603,sK604,sK196(sK603,sF644,sK605))
| ~ in(sK196(sK603,sF644,sK605),a_2_0_yellow19(sK603,sK605))
| ~ in(sK605,sF645)
| spl647_6 ),
inference(forward_subsumption_resolution,[],[f8430,f8103]) ).
fof(f8436,plain,
( is_eventually_in(sK603,sK604,sK196(sK603,sF644,sK605))
| ~ in(sK196(sK603,sF644,sK605),a_2_0_yellow19(sK603,sK605))
| ~ spl647_5
| spl647_6 ),
inference(forward_subsumption_resolution,[],[f8433,f7359]) ).
fof(f8439,plain,
( ~ in(sK196(sK603,sF644,sK605),neighborhood_system(sK603,sK605))
| is_eventually_in(sK603,sK604,sK196(sK603,sF644,sK605))
| ~ spl647_5
| spl647_6 ),
inference(forward_demodulation,[],[f8436,f7860]) ).
fof(f8443,definition,
( spl647_75
<=> is_eventually_in(sK603,sK604,sK196(sK603,sF644,sK605)) ),
introduced(definition,[new_symbols(definition,[spl647_75])],[avatar_definition]) ).
fof(f8445,plain,
( is_eventually_in(sK603,sK604,sK196(sK603,sF644,sK605))
| ~ spl647_75 ),
inference(avatar_component_clause,[],[f8443]) ).
fof(f8447,definition,
( spl647_76
<=> in(sK196(sK603,sF644,sK605),neighborhood_system(sK603,sK605)) ),
introduced(definition,[new_symbols(definition,[spl647_76])],[avatar_definition]) ).
fof(f8449,plain,
( ~ in(sK196(sK603,sF644,sK605),neighborhood_system(sK603,sK605))
| spl647_76 ),
inference(avatar_component_clause,[],[f8447]) ).
fof(f8450,plain,
( spl647_75
| ~ spl647_76
| ~ spl647_5
| spl647_6 ),
inference(avatar_split_clause,[],[f8439,f7361,f7357,f8447,f8443]) ).
fof(f8459,definition,
( spl647_78
<=> point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605) ),
introduced(definition,[new_symbols(definition,[spl647_78])],[avatar_definition]) ).
fof(f8460,plain,
( ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| spl647_78 ),
inference(avatar_component_clause,[],[f8459]) ).
fof(f8464,plain,
( ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_76 ),
inference(resolution,[],[f8449,f5891]) ).
fof(f8465,plain,
( ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_76 ),
inference(forward_subsumption_resolution,[],[f8464,f5669]) ).
fof(f8467,plain,
( ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| ~ top_str(sK603)
| spl647_76 ),
inference(forward_subsumption_resolution,[],[f8465,f5668]) ).
fof(f8469,plain,
( ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| spl647_76 ),
inference(forward_subsumption_resolution,[],[f8467,f5667]) ).
fof(f8471,plain,
( ~ element(sK605,sF646)
| ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| spl647_76 ),
inference(forward_demodulation,[],[f8469,f7303]) ).
fof(f8472,plain,
( ~ point_neighbourhood(sK196(sK603,sF644,sK605),sK603,sK605)
| spl647_76 ),
inference(forward_subsumption_resolution,[],[f8471,f7304]) ).
fof(f8473,plain,
( ~ spl647_78
| spl647_76 ),
inference(avatar_split_clause,[],[f8472,f8447,f8459]) ).
fof(f8475,plain,
( ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ in(sK605,sK196(sK603,sF644,sK605))
| ~ element(sK605,the_carrier(sK603))
| is_a_convergence_point_of_set(sK603,sF644,sK605)
| empty_carrier(sK603)
| spl647_78 ),
inference(resolution,[],[f8460,f7998]) ).
fof(f8476,plain,
( ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ element(sK605,the_carrier(sK603))
| is_a_convergence_point_of_set(sK603,sF644,sK605)
| empty_carrier(sK603)
| spl647_78 ),
inference(forward_subsumption_resolution,[],[f8475,f3849]) ).
fof(f8478,definition,
( spl647_79
<=> in(sK196(sK603,sF644,sK605),sF644) ),
introduced(definition,[new_symbols(definition,[spl647_79])],[avatar_definition]) ).
fof(f8479,plain,
( in(sK196(sK603,sF644,sK605),sF644)
| ~ spl647_79 ),
inference(avatar_component_clause,[],[f8478]) ).
fof(f8490,plain,
( ~ top_str(sK603)
| ~ element(sK605,the_carrier(sK603))
| is_a_convergence_point_of_set(sK603,sF644,sK605)
| empty_carrier(sK603)
| spl647_78 ),
inference(forward_subsumption_resolution,[],[f8476,f5668]) ).
fof(f8491,plain,
( ~ element(sK605,the_carrier(sK603))
| is_a_convergence_point_of_set(sK603,sF644,sK605)
| empty_carrier(sK603)
| spl647_78 ),
inference(forward_subsumption_resolution,[],[f8490,f5667]) ).
fof(f8492,plain,
( ~ element(sK605,the_carrier(sK603))
| empty_carrier(sK603)
| spl647_6
| spl647_78 ),
inference(forward_subsumption_resolution,[],[f8491,f7362]) ).
fof(f8493,plain,
( ~ element(sK605,the_carrier(sK603))
| spl647_6
| spl647_78 ),
inference(forward_subsumption_resolution,[],[f8492,f5669]) ).
fof(f8494,plain,
( ~ element(sK605,sF646)
| spl647_6
| spl647_78 ),
inference(forward_demodulation,[],[f8493,f7303]) ).
fof(f8495,plain,
( $false
| spl647_6
| spl647_78 ),
inference(forward_subsumption_resolution,[],[f8494,f7304]) ).
fof(f8496,plain,
( spl647_6
| spl647_78 ),
inference(avatar_contradiction_clause,[],[f8495]) ).
fof(f8515,definition,
( spl647_82
<=> point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605) ),
introduced(definition,[new_symbols(definition,[spl647_82])],[avatar_definition]) ).
fof(f8516,plain,
( ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| spl647_82 ),
inference(avatar_component_clause,[],[f8515]) ).
fof(f8519,definition,
( spl647_83
<=> in(sK115(sK603,sK604,sK605),neighborhood_system(sK603,sK605)) ),
introduced(definition,[new_symbols(definition,[spl647_83])],[avatar_definition]) ).
fof(f8520,plain,
( in(sK115(sK603,sK604,sK605),neighborhood_system(sK603,sK605))
| ~ spl647_83 ),
inference(avatar_component_clause,[],[f8519]) ).
fof(f8521,plain,
( ~ in(sK115(sK603,sK604,sK605),neighborhood_system(sK603,sK605))
| spl647_83 ),
inference(avatar_component_clause,[],[f8519]) ).
fof(f8523,plain,
( ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_83 ),
inference(resolution,[],[f8521,f5891]) ).
fof(f8524,plain,
( ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_83 ),
inference(forward_subsumption_resolution,[],[f8523,f5669]) ).
fof(f8525,plain,
( ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| ~ top_str(sK603)
| spl647_83 ),
inference(forward_subsumption_resolution,[],[f8524,f5668]) ).
fof(f8526,plain,
( ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| ~ element(sK605,the_carrier(sK603))
| spl647_83 ),
inference(forward_subsumption_resolution,[],[f8525,f5667]) ).
fof(f8527,plain,
( ~ element(sK605,sF646)
| ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| spl647_83 ),
inference(forward_demodulation,[],[f8526,f7303]) ).
fof(f8528,plain,
( ~ point_neighbourhood(sK115(sK603,sK604,sK605),sK603,sK605)
| spl647_83 ),
inference(forward_subsumption_resolution,[],[f8527,f7304]) ).
fof(f8529,plain,
( ~ spl647_82
| spl647_83 ),
inference(avatar_split_clause,[],[f8528,f8519,f8515]) ).
fof(f8530,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| empty_carrier(sK604)
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_82 ),
inference(resolution,[],[f8516,f7673]) ).
fof(f8533,definition,
( spl647_84
<=> in(sK115(sK603,sK604,sK605),sF644) ),
introduced(definition,[new_symbols(definition,[spl647_84])],[avatar_definition]) ).
fof(f8534,plain,
( in(sK115(sK603,sK604,sK605),sF644)
| ~ spl647_84 ),
inference(avatar_component_clause,[],[f8533]) ).
fof(f8535,plain,
( ~ in(sK115(sK603,sK604,sK605),sF644)
| spl647_84 ),
inference(avatar_component_clause,[],[f8533]) ).
fof(f8545,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| ~ transitive_relstr(sK604)
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8530,f5673]) ).
fof(f8546,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| ~ directed_relstr(sK604)
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8545,f5672]) ).
fof(f8547,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| ~ net_str(sK604,sK603)
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8546,f5671]) ).
fof(f8548,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8547,f5670]) ).
fof(f8549,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8548,f5669]) ).
fof(f8550,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| ~ top_str(sK603)
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8549,f5668]) ).
fof(f8551,plain,
( in(sK605,lim_points_of_net(sK603,sK604))
| ~ element(sK605,the_carrier(sK603))
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8550,f5667]) ).
fof(f8552,plain,
( in(sK605,sF645)
| ~ element(sK605,the_carrier(sK603))
| spl647_82 ),
inference(forward_demodulation,[],[f8551,f7299]) ).
fof(f8553,plain,
( ~ element(sK605,the_carrier(sK603))
| spl647_5
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8552,f7358]) ).
fof(f8554,plain,
( ~ element(sK605,sF646)
| spl647_5
| spl647_82 ),
inference(forward_demodulation,[],[f8553,f7303]) ).
fof(f8555,plain,
( $false
| spl647_5
| spl647_82 ),
inference(forward_subsumption_resolution,[],[f8554,f7304]) ).
fof(f8556,plain,
( spl647_5
| spl647_82 ),
inference(avatar_contradiction_clause,[],[f8555]) ).
fof(f8563,plain,
( in(sK196(sK603,sF644,sK605),sF644)
| is_a_convergence_point_of_set(sK603,sF644,sK605)
| ~ spl647_75 ),
inference(resolution,[],[f8445,f8083]) ).
fof(f8571,plain,
( in(sK196(sK603,sF644,sK605),sF644)
| spl647_6
| ~ spl647_75 ),
inference(forward_subsumption_resolution,[],[f8563,f7362]) ).
fof(f8572,plain,
( spl647_79
| spl647_6
| ~ spl647_75 ),
inference(avatar_split_clause,[],[f8571,f8443,f7361,f8478]) ).
fof(f8573,plain,
( is_a_convergence_point_of_set(sK603,sF644,sK605)
| ~ topological_space(sK603)
| ~ top_str(sK603)
| ~ spl647_79 ),
inference(resolution,[],[f8479,f3851]) ).
fof(f8578,plain,
( ~ topological_space(sK603)
| ~ top_str(sK603)
| spl647_6
| ~ spl647_79 ),
inference(forward_subsumption_resolution,[],[f8573,f7362]) ).
fof(f8579,plain,
( ~ top_str(sK603)
| spl647_6
| ~ spl647_79 ),
inference(forward_subsumption_resolution,[],[f8578,f5668]) ).
fof(f8580,plain,
( $false
| spl647_6
| ~ spl647_79 ),
inference(forward_subsumption_resolution,[],[f8579,f5667]) ).
fof(f8581,plain,
( spl647_6
| ~ spl647_79 ),
inference(avatar_contradiction_clause,[],[f8580]) ).
fof(f10829,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(sF646)))))
| ~ is_a_convergence_point_of_set(sK603,X0,X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF646)))
| subset(neighborhood_system(sK603,X1),X0)
| ~ element(X1,the_carrier(sK603))
| empty_carrier(sK603)
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(superposition,[],[f6954,f7900]) ).
fof(f10830,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(sF646)))))
| ~ is_a_convergence_point_of_set(sK603,X0,X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF646)))
| subset(neighborhood_system(sK603,X1),X0)
| ~ element(X1,the_carrier(sK603))
| ~ topological_space(sK603)
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f10829,f5669]) ).
fof(f10835,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(sF646)))))
| ~ is_a_convergence_point_of_set(sK603,X0,X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF646)))
| subset(neighborhood_system(sK603,X1),X0)
| ~ element(X1,the_carrier(sK603))
| ~ top_str(sK603) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f10830,f5668]) ).
fof(f10837,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(sF646)))))
| ~ is_a_convergence_point_of_set(sK603,X0,X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF646)))
| subset(neighborhood_system(sK603,X1),X0)
| ~ element(X1,the_carrier(sK603)) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f10835,f5667]) ).
fof(f10839,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF646)))
| ~ is_a_convergence_point_of_set(sK603,X0,X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF646)))
| subset(neighborhood_system(sK603,X1),X0)
| ~ element(X1,the_carrier(sK603)) )
| ~ spl647_61 ),
inference(forward_demodulation,[],[f10837,f6949]) ).
fof(f10840,plain,
( ! [X0,X1] :
( ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF646)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF646)))
| ~ is_a_convergence_point_of_set(sK603,X0,X1)
| ~ element(X1,sF646)
| subset(neighborhood_system(sK603,X1),X0) )
| ~ spl647_61 ),
inference(forward_demodulation,[],[f10839,f7303]) ).
fof(f10841,plain,
( ! [X0] :
( ~ element(sF644,k1_pcomps_1(k1_pcomps_1(sF646)))
| ~ is_a_convergence_point_of_set(sK603,sF644,X0)
| ~ element(X0,sF646)
| subset(neighborhood_system(sK603,X0),sF644) )
| ~ spl647_61 ),
inference(resolution,[],[f10840,f7901]) ).
fof(f10846,plain,
( ! [X0] :
( subset(neighborhood_system(sK603,X0),sF644)
| ~ element(X0,sF646)
| ~ is_a_convergence_point_of_set(sK603,sF644,X0) )
| ~ spl647_61 ),
inference(forward_subsumption_resolution,[],[f10841,f7903]) ).
fof(f10849,plain,
( ! [X0,X1] :
( ~ in(X1,neighborhood_system(sK603,X0))
| ~ is_a_convergence_point_of_set(sK603,sF644,X0)
| ~ element(X0,sF646)
| in(X1,sF644) )
| ~ spl647_61 ),
inference(resolution,[],[f10846,f3762]) ).
fof(f10884,plain,
( ~ is_a_convergence_point_of_set(sK603,sF644,sK605)
| ~ element(sK605,sF646)
| in(sK115(sK603,sK604,sK605),sF644)
| ~ spl647_61
| ~ spl647_83 ),
inference(resolution,[],[f10849,f8520]) ).
fof(f10890,plain,
( ~ element(sK605,sF646)
| in(sK115(sK603,sK604,sK605),sF644)
| ~ spl647_6
| ~ spl647_61
| ~ spl647_83 ),
inference(forward_subsumption_resolution,[],[f10884,f7363]) ).
fof(f10893,plain,
( in(sK115(sK603,sK604,sK605),sF644)
| ~ spl647_6
| ~ spl647_61
| ~ spl647_83 ),
inference(forward_subsumption_resolution,[],[f10890,f7304]) ).
fof(f10897,plain,
( $false
| ~ spl647_6
| ~ spl647_61
| ~ spl647_83
| spl647_84 ),
inference(forward_subsumption_resolution,[],[f10893,f8535]) ).
fof(f10898,plain,
( ~ spl647_6
| ~ spl647_61
| ~ spl647_83
| spl647_84 ),
inference(avatar_contradiction_clause,[],[f10897]) ).
fof(f10909,plain,
( in(sK605,sF645)
| ~ element(sK605,sF646)
| ~ spl647_61
| ~ spl647_84 ),
inference(resolution,[],[f8534,f7812]) ).
fof(f10920,plain,
( ~ element(sK605,sF646)
| spl647_5
| ~ spl647_61
| ~ spl647_84 ),
inference(forward_subsumption_resolution,[],[f10909,f7358]) ).
fof(f10921,plain,
( $false
| spl647_5
| ~ spl647_61
| ~ spl647_84 ),
inference(forward_subsumption_resolution,[],[f10920,f7304]) ).
fof(f10922,plain,
( spl647_5
| ~ spl647_61
| ~ spl647_84 ),
inference(avatar_contradiction_clause,[],[f10921]) ).
cnf(s3,plain,
( spl647_5
| spl647_6 ),
inference(sat_conversion,[],[f7364]) ).
cnf(s4,plain,
( ~ spl647_5
| ~ spl647_6 ),
inference(sat_conversion,[],[f7365]) ).
cnf(s53,plain,
spl647_61,
inference(sat_conversion,[],[f7780]) ).
cnf(s60,plain,
( ~ spl647_5
| spl647_6
| spl647_75
| ~ spl647_76 ),
inference(sat_conversion,[],[f8450]) ).
cnf(s63,plain,
( spl647_76
| ~ spl647_78 ),
inference(sat_conversion,[],[f8473]) ).
cnf(s65,plain,
( spl647_6
| spl647_78 ),
inference(sat_conversion,[],[f8496]) ).
cnf(s67,plain,
( ~ spl647_82
| spl647_83 ),
inference(sat_conversion,[],[f8529]) ).
cnf(s69,plain,
( spl647_5
| spl647_82 ),
inference(sat_conversion,[],[f8556]) ).
cnf(s71,plain,
( spl647_6
| ~ spl647_75
| spl647_79 ),
inference(sat_conversion,[],[f8572]) ).
cnf(s72,plain,
( spl647_6
| ~ spl647_79 ),
inference(sat_conversion,[],[f8581]) ).
cnf(s119,plain,
( ~ spl647_6
| ~ spl647_61
| ~ spl647_83
| spl647_84 ),
inference(sat_conversion,[],[f10898]) ).
cnf(s121,plain,
( spl647_5
| ~ spl647_61
| ~ spl647_84 ),
inference(sat_conversion,[],[f10922]) ).
cnf(s124,plain,
spl647_5,
inference(rat,[],[s119,s67,s3,s69,s121,s53]) ).
cnf(s125,plain,
~ spl647_6,
inference(rat,[],[s4,s124]) ).
cnf(s126,plain,
~ spl647_79,
inference(rat,[],[s72,s125]) ).
cnf(s127,plain,
~ spl647_75,
inference(rat,[],[s71,s126,s125]) ).
cnf(s128,plain,
spl647_78,
inference(rat,[],[s65,s125]) ).
cnf(s129,plain,
~ spl647_76,
inference(rat,[],[s60,s125,s124,s127]) ).
cnf(s130,plain,
$false,
inference(rat,[],[s63,s128,s129]) ).
fof(f10923,plain,
$false,
inference(avatar_sat_refutation,[],[s130]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU392+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n018.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 28 05:06:54 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.48 Running first-order theorem proving
% 0.15/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.52/4.49 % (3002905)Detected formulas, will run a generic FOF schedule.
% 23.52/4.49 % (3002914)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2567946956:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 23.52/4.49 % (3002917)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3887805611:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 23.52/4.49 % (3002912)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2591706119:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 23.52/4.49 % (3002916)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3765842309:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 23.52/4.49 % (3002915)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4055486006:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 23.52/4.49 % (3002913)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2194128890:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 23.52/4.49 % (3002918)dis-21_1_sil=8000:lcm=predicate:random_seed=39881392:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 23.52/4.49 % (3002917)Instruction limit reached!
% 23.52/4.49 % (3002917)------------------------------
% 23.52/4.49 % (3002917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.52/4.49 % (3002917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.52/4.49 % (3002917)CaDiCaL version: 2.1.3
% 23.52/4.49 % (3002917)Termination reason: Instruction limit
% 23.52/4.49 % (3002917)Termination phase: Saturation
% 23.52/4.49 % (3002917)Time elapsed: 0.137 s
% 23.52/4.49 % (3002917)Peak memory usage: 92 MB
% 23.52/4.49 % (3002917)Instructions burned: 139 (million)
% 23.52/4.49 % (3002915)Instruction limit reached!
% 23.52/4.49 % (3002915)------------------------------
% 23.52/4.49 % (3002915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.52/4.49 % (3002915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.52/4.49 % (3002915)CaDiCaL version: 2.1.3
% 23.52/4.49 % (3002915)Termination reason: Instruction limit
% 23.52/4.49 % (3002915)Termination phase: Blocked clause elimination
% 23.52/4.49 % (3002915)Time elapsed: 0.105 s
% 23.52/4.49 % (3002915)Peak memory usage: 90 MB
% 23.52/4.49 % (3002915)Instructions burned: 110 (million)
% 23.52/4.49 % (3002916)Instruction limit reached!
% 23.52/4.49 % (3002916)------------------------------
% 23.52/4.49 % (3002916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.52/4.49 % (3002916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.52/4.49 % (3002916)CaDiCaL version: 2.1.3
% 23.52/4.49 % (3002916)Termination reason: Instruction limit
% 23.52/4.49 % (3002916)Termination phase: Saturation
% 23.52/4.49 % (3002916)Time elapsed: 0.119 s
% 23.52/4.49 % (3002916)Peak memory usage: 92 MB
% 23.52/4.49 % (3002916)Instructions burned: 119 (million)
% 23.52/4.49 % (3002918)Instruction limit reached!
% 23.52/4.49 % (3002918)------------------------------
% 23.52/4.49 % (3002918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.52/4.49 % (3002918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.52/4.49 % (3002918)CaDiCaL version: 2.1.3
% 23.52/4.49 % (3002918)Termination reason: Instruction limit
% 23.52/4.49 % (3002918)Termination phase: Saturation
% 23.52/4.49 % (3002918)Time elapsed: 0.117 s
% 23.52/4.49 % (3002918)Peak memory usage: 92 MB
% 23.52/4.49 % (3002918)Instructions burned: 130 (million)
% 23.52/4.49 % (3002926)lrs+10_1_sil=8000:sp=occurrence:random_seed=3040869536:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 23.52/4.49 % (3002927)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1429080149:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 23.52/4.49 % (3002929)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1298608848:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 23.52/4.49 % (3002928)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3847996432:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 23.52/4.49 % (3002926)Instruction limit reached!
% 22.85/4.95 % (3002926)------------------------------
% 22.85/4.95 % (3002926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002926)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002926)Termination reason: Instruction limit
% 22.85/4.95 % (3002926)Termination phase: Saturation
% 22.85/4.95 % (3002926)Time elapsed: 0.245 s
% 22.85/4.95 % (3002926)Peak memory usage: 95 MB
% 22.85/4.95 % (3002926)Instructions burned: 285 (million)
% 22.85/4.95 % (3002927)Instruction limit reached!
% 22.85/4.95 % (3002927)------------------------------
% 22.85/4.95 % (3002927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002927)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002927)Termination reason: Instruction limit
% 22.85/4.95 % (3002927)Termination phase: Saturation
% 22.85/4.95 % (3002927)Time elapsed: 0.127 s
% 22.85/4.95 % (3002927)Peak memory usage: 92 MB
% 22.85/4.95 % (3002927)Instructions burned: 157 (million)
% 22.85/4.95 % (3002929)Instruction limit reached!
% 22.85/4.95 % (3002929)------------------------------
% 22.85/4.95 % (3002929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002929)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002929)Termination reason: Instruction limit
% 22.85/4.95 % (3002929)Termination phase: Saturation
% 22.85/4.95 % (3002929)Time elapsed: 0.244 s
% 22.85/4.95 % (3002929)Peak memory usage: 94 MB
% 22.85/4.95 % (3002929)Instructions burned: 248 (million)
% 22.85/4.95 % (3002934)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=618530335:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 22.85/4.95 % (3002935)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1362621092:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 22.85/4.95 % (3002928)Instruction limit reached!
% 22.85/4.95 % (3002928)------------------------------
% 22.85/4.95 % (3002928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002928)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002928)Termination reason: Instruction limit
% 22.85/4.95 % (3002928)Termination phase: Saturation
% 22.85/4.95 % (3002928)Time elapsed: 0.335 s
% 22.85/4.95 % (3002928)Peak memory usage: 96 MB
% 22.85/4.95 % (3002928)Instructions burned: 326 (million)
% 22.85/4.95 % (3002936)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4031787892:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 22.85/4.95 % (3002939)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1793583717:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 22.85/4.95 % (3002936)Instruction limit reached!
% 22.85/4.95 % (3002936)------------------------------
% 22.85/4.95 % (3002936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002936)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002936)Termination reason: Instruction limit
% 22.85/4.95 % (3002936)Termination phase: Saturation
% 22.85/4.95 % (3002936)Time elapsed: 0.109 s
% 22.85/4.95 % (3002936)Peak memory usage: 92 MB
% 22.85/4.95 % (3002936)Instructions burned: 113 (million)
% 22.85/4.95 % (3002934)Instruction limit reached!
% 22.85/4.95 % (3002934)------------------------------
% 22.85/4.95 % (3002934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002934)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002934)Termination reason: Instruction limit
% 22.85/4.95 % (3002934)Termination phase: Saturation
% 22.85/4.95 % (3002934)Time elapsed: 0.291 s
% 22.85/4.95 % (3002934)Peak memory usage: 94 MB
% 22.85/4.95 % (3002934)Instructions burned: 294 (million)
% 22.85/4.95 % (3002939)Instruction limit reached!
% 22.85/4.95 % (3002939)------------------------------
% 22.85/4.95 % (3002939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002939)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002939)Termination reason: Instruction limit
% 22.85/4.95 % (3002939)Termination phase: Blocked clause elimination
% 22.85/4.95 % (3002939)Time elapsed: 0.121 s
% 22.85/4.95 % (3002939)Peak memory usage: 91 MB
% 22.85/4.95 % (3002939)Instructions burned: 127 (million)
% 22.85/4.95 % (3002942)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3018451201:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 22.85/4.95 % (3002943)lrs+10_1_sil=8000:sp=occurrence:random_seed=3044092731:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 22.85/4.95 % (3002944)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1296584729:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 22.85/4.95 % (3002942)Instruction limit reached!
% 22.85/4.95 % (3002942)------------------------------
% 22.85/4.95 % (3002942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002942)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002942)Termination reason: Instruction limit
% 22.85/4.95 % (3002942)Termination phase: Saturation
% 22.85/4.95 % (3002942)Time elapsed: 0.117 s
% 22.85/4.95 % (3002942)Peak memory usage: 90 MB
% 22.85/4.95 % (3002942)Instructions burned: 115 (million)
% 22.85/4.95 % (3002948)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=230051635:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 22.85/4.95 % (3002944)Instruction limit reached!
% 22.85/4.95 % (3002944)------------------------------
% 22.85/4.95 % (3002944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002944)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002944)Termination reason: Instruction limit
% 22.85/4.95 % (3002944)Termination phase: Saturation
% 22.85/4.95 % (3002944)Time elapsed: 0.415 s
% 22.85/4.95 % (3002944)Peak memory usage: 96 MB
% 22.85/4.95 % (3002944)Instructions burned: 437 (million)
% 22.85/4.95 % (3002950)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4146701941:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 22.85/4.95 % (3002950)Instruction limit reached!
% 22.85/4.95 % (3002950)------------------------------
% 22.85/4.95 % (3002950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002950)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002950)Termination reason: Instruction limit
% 22.85/4.95 % (3002950)Termination phase: Property scanning
% 22.85/4.95 % (3002950)Time elapsed: 0.094 s
% 22.85/4.95 % (3002950)Peak memory usage: 90 MB
% 22.85/4.95 % (3002950)Instructions burned: 134 (million)
% 22.85/4.95 % (3002943)Instruction limit reached!
% 22.85/4.95 % (3002943)------------------------------
% 22.85/4.95 % (3002943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002943)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002943)Termination reason: Instruction limit
% 22.85/4.95 % (3002943)Termination phase: Saturation
% 22.85/4.95 % (3002943)Time elapsed: 0.914 s
% 22.85/4.95 % (3002943)Peak memory usage: 106 MB
% 22.85/4.95 % (3002943)Instructions burned: 907 (million)
% 22.85/4.95 % (3002952)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3851774834:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 22.85/4.95 % (3002953)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2652704036:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 22.85/4.95 % (3002952)Instruction limit reached!
% 22.85/4.95 % (3002952)------------------------------
% 22.85/4.95 % (3002952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002952)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002952)Termination reason: Instruction limit
% 22.85/4.95 % (3002952)Termination phase: Saturation
% 22.85/4.95 % (3002952)Time elapsed: 0.531 s
% 22.85/4.95 % (3002952)Peak memory usage: 100 MB
% 22.85/4.95 % (3002952)Instructions burned: 592 (million)
% 22.85/4.95 % (3002912)First to succeed.
% 22.85/4.95 % (3002912)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3002905"
% 22.85/4.95 % (3002958)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3126703169:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/125Mi)
% 22.85/4.95 % (3002935)Instruction limit reached!
% 22.85/4.95 % (3002935)------------------------------
% 22.85/4.95 % (3002935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002935)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002935)Termination reason: Instruction limit
% 22.85/4.95 % (3002935)Termination phase: Saturation
% 22.85/4.95 % (3002935)Time elapsed: 2.399 s
% 22.85/4.95 % (3002935)Peak memory usage: 164 MB
% 22.85/4.95 % (3002935)Instructions burned: 2350 (million)
% 22.85/4.95 % (3002958)Instruction limit reached!
% 22.85/4.95 % (3002958)------------------------------
% 22.85/4.95 % (3002958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/4.95 % (3002958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/4.95 % (3002958)CaDiCaL version: 2.1.3
% 22.85/4.95 % (3002958)Termination reason: Instruction limit
% 22.85/4.95 % (3002958)Termination phase: Saturation
% 22.85/4.95 % (3002958)Time elapsed: 0.113 s
% 22.85/4.95 % (3002958)Peak memory usage: 92 MB
% 22.85/4.95 % (3002958)Instructions burned: 125 (million)
% 22.85/4.95 % (3002913)Also succeeded, but the first one will report.
% 22.85/4.95 % (3002961)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=568932281:i=134:gtgl=5:slsql=off:gtg=exists_sym_2965 on theBenchmark for (2965ds/134Mi)
% 22.85/4.95 % (3002962)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=89105439:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/141Mi)
% 22.85/4.95 % (3002912)Refutation found. Thanks to Tanya!
% 22.85/4.95 % SZS status Theorem for theBenchmark
% 22.85/4.95 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/5.20 % (3002912)------------------------------
% 0.22/5.20 % (3002912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.22/5.20 % (3002912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/5.20 % (3002912)CaDiCaL version: 2.1.3
% 0.22/5.20 % (3002912)Termination reason: Refutation
% 0.22/5.20 % (3002912)Time elapsed: 2.896 s
% 0.22/5.20 % (3002912)Peak memory usage: 171 MB
% 0.22/5.20 % (3002912)Instructions burned: 2771 (million)
% 0.22/5.20 % (3002912)------------------------------
% 0.22/5.20 % (3002912)------------------------------
% 0.22/5.20 % (3002905)Success in time 3.892 s
% 0.22/5.20 % Vampire exiting
%------------------------------------------------------------------------------