%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:53:07 PM UTC 2026
% Result : Theorem 0.26s 0.48s
% Output : Refutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 17
% Syntax : Number of formulae : 166 ( 22 unt; 8 def)
% Number of atoms : 859 ( 11 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 1139 ( 446 ~; 540 |; 121 &)
% ( 13 <=>; 17 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 9 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 134 ( 0 sgn 122 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34,axiom,
! [X0] :
( one_sorted_str(X0)
=> element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f37,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty(X1)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& net_str(net_of_bool_filter(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow19) ).
fof(f40,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f63,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(cast_as_carrier_subset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_pre_topc) ).
fof(f73,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty(X1)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_yellow19) ).
fof(f76,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty(X1)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& directed_relstr(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_yellow19) ).
fof(f125,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,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(f126,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_yellow19) ).
fof(f127,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<=> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_yellow19) ).
fof(f128,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<=> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f127]) ).
fof(f249,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f252,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(ennf_transformation,[],[f37]) ).
fof(f253,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(flattening,[],[f252]) ).
fof(f255,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f270,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f271,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f270]) ).
fof(f287,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(ennf_transformation,[],[f73]) ).
fof(f288,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(flattening,[],[f287]) ).
fof(f293,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& directed_relstr(net_of_bool_filter(X0,X1,X2)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(ennf_transformation,[],[f76]) ).
fof(f294,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& directed_relstr(net_of_bool_filter(X0,X1,X2)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(flattening,[],[f293]) ).
fof(f339,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,[],[f125]) ).
fof(f340,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,[],[f339]) ).
fof(f341,plain,
! [X0] :
( ! [X1] :
( X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f126]) ).
fof(f342,plain,
! [X0] :
( ! [X1] :
( X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f341]) ).
fof(f343,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<~> is_a_convergence_point_of_set(X0,X1,X2) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(ennf_transformation,[],[f128]) ).
fof(f344,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<~> is_a_convergence_point_of_set(X0,X1,X2) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(flattening,[],[f343]) ).
fof(f409,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) )
& ( 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,[],[f340]) ).
fof(f410,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ~ in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& ( is_a_convergence_point_of_set(X0,X1,X2)
| in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(nnf_transformation,[],[f344]) ).
fof(f411,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ~ in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& ( is_a_convergence_point_of_set(X0,X1,X2)
| in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(flattening,[],[f410]) ).
fof(f412,plain,
( ( ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) )
& ( is_a_convergence_point_of_set(sK46,sK47,sK48)
| in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) )
& element(sK48,the_carrier(sK46))
& ~ empty(sK47)
& filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
& upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
& proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
& element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
& ~ empty_carrier(sK46)
& topological_space(sK46)
& top_str(sK46) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47,sK48]),skolemize(X0,sK46),skolemize(X1,sK47),skolemize(X2,sK48)],[f411]) ).
fof(f486,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f488,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| net_str(net_of_bool_filter(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f253]) ).
fof(f490,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f253]) ).
fof(f494,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f530,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f271]) ).
fof(f560,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| transitive_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f288]) ).
fof(f566,plain,
! [X2,X0,X1] :
( ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| directed_relstr(net_of_bool_filter(X0,X1,X2))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f294]) ).
fof(f773,plain,
! [X2,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(cnf_transformation,[],[f409]) ).
fof(f774,plain,
! [X2,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(cnf_transformation,[],[f409]) ).
fof(f775,plain,
! [X0,X1] :
( ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f342]) ).
fof(f776,plain,
top_str(sK46),
inference(cnf_transformation,[],[f412]) ).
fof(f777,plain,
topological_space(sK46),
inference(cnf_transformation,[],[f412]) ).
fof(f778,plain,
~ empty_carrier(sK46),
inference(cnf_transformation,[],[f412]) ).
fof(f779,plain,
element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))),
inference(cnf_transformation,[],[f412]) ).
fof(f780,plain,
proper_element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))),
inference(cnf_transformation,[],[f412]) ).
fof(f781,plain,
upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46))),
inference(cnf_transformation,[],[f412]) ).
fof(f782,plain,
filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46))),
inference(cnf_transformation,[],[f412]) ).
fof(f783,plain,
~ empty(sK47),
inference(cnf_transformation,[],[f412]) ).
fof(f784,plain,
element(sK48,the_carrier(sK46)),
inference(cnf_transformation,[],[f412]) ).
fof(f785,plain,
( is_a_convergence_point_of_set(sK46,sK47,sK48)
| in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
inference(cnf_transformation,[],[f412]) ).
fof(f786,plain,
( ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
inference(cnf_transformation,[],[f412]) ).
fof(f799,definition,
( spl50_1
<=> in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ),
introduced(definition,[new_symbols(definition,[spl50_1])],[avatar_definition]) ).
fof(f800,plain,
( ~ in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| spl50_1 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f801,plain,
( in(sK48,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ spl50_1 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f803,definition,
( spl50_2
<=> is_a_convergence_point_of_set(sK46,sK47,sK48) ),
introduced(definition,[new_symbols(definition,[spl50_2])],[avatar_definition]) ).
fof(f804,plain,
( ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| spl50_2 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f805,plain,
( is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ spl50_2 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f806,plain,
( spl50_1
| spl50_2 ),
inference(avatar_split_clause,[],[f785,f803,f799]) ).
fof(f807,plain,
( ~ spl50_1
| ~ spl50_2 ),
inference(avatar_split_clause,[],[f786,f803,f799]) ).
fof(f821,plain,
one_sorted_str(sK46),
inference(resolution,[],[f494,f776]) ).
fof(f2074,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(resolution,[],[f490,f779]) ).
fof(f2075,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(forward_subsumption_resolution,[],[f2074,f783]) ).
fof(f2094,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(forward_subsumption_resolution,[],[f2075,f782]) ).
fof(f2108,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(forward_subsumption_resolution,[],[f2094,f781]) ).
fof(f2118,definition,
( spl50_39
<=> empty(cast_as_carrier_subset(sK46)) ),
introduced(definition,[new_symbols(definition,[spl50_39])],[avatar_definition]) ).
fof(f2119,plain,
( ~ empty(cast_as_carrier_subset(sK46))
| spl50_39 ),
inference(avatar_component_clause,[],[f2118]) ).
fof(f2120,plain,
( empty(cast_as_carrier_subset(sK46))
| ~ spl50_39 ),
inference(avatar_component_clause,[],[f2118]) ).
fof(f2122,definition,
( spl50_40
<=> ! [X0] :
( empty_carrier(X0)
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ) ),
introduced(definition,[new_symbols(definition,[spl50_40])],[avatar_definition]) ).
fof(f2123,plain,
( ! [X0] :
( ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl50_40 ),
inference(avatar_component_clause,[],[f2122]) ).
fof(f2124,plain,
( spl50_39
| spl50_40 ),
inference(avatar_split_clause,[],[f2108,f2122,f2118]) ).
fof(f2148,plain,
( empty_carrier(sK46)
| ~ one_sorted_str(sK46)
| ~ spl50_39 ),
inference(resolution,[],[f2120,f530]) ).
fof(f2155,plain,
( ~ one_sorted_str(sK46)
| ~ spl50_39 ),
inference(forward_subsumption_resolution,[],[f2148,f778]) ).
fof(f2171,plain,
( $false
| ~ spl50_39 ),
inference(forward_subsumption_resolution,[],[f2155,f821]) ).
fof(f2172,plain,
~ spl50_39,
inference(avatar_contradiction_clause,[],[f2171]) ).
fof(f2200,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(resolution,[],[f560,f779]) ).
fof(f2201,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(forward_subsumption_resolution,[],[f2200,f783]) ).
fof(f2220,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(forward_subsumption_resolution,[],[f2201,f782]) ).
fof(f2234,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) ),
inference(forward_subsumption_resolution,[],[f2220,f781]) ).
fof(f2244,definition,
( spl50_44
<=> ! [X0] :
( empty_carrier(X0)
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ) ),
introduced(definition,[new_symbols(definition,[spl50_44])],[avatar_definition]) ).
fof(f2245,plain,
( ! [X0] :
( ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| transitive_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl50_44 ),
inference(avatar_component_clause,[],[f2244]) ).
fof(f2246,plain,
( spl50_39
| spl50_44 ),
inference(avatar_split_clause,[],[f2234,f2244,f2118]) ).
fof(f2360,plain,
( ~ empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46)
| ~ one_sorted_str(sK46)
| ~ spl50_40 ),
inference(resolution,[],[f2123,f486]) ).
fof(f2362,plain,
( ~ empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46)
| ~ spl50_40 ),
inference(duplicate_literal_removal,[],[f2360]) ).
fof(f2363,plain,
( ~ empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(sK46)
| ~ spl50_40 ),
inference(forward_subsumption_resolution,[],[f2362,f778]) ).
fof(f2364,plain,
( ~ empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ spl50_40 ),
inference(forward_subsumption_resolution,[],[f2363,f821]) ).
fof(f2367,plain,
( transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46)
| ~ one_sorted_str(sK46)
| ~ spl50_44 ),
inference(resolution,[],[f2245,f486]) ).
fof(f2369,plain,
( transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46)
| ~ spl50_44 ),
inference(duplicate_literal_removal,[],[f2367]) ).
fof(f2370,plain,
( transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(sK46)
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2369,f778]) ).
fof(f2371,plain,
( transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2370,f821]) ).
fof(f2401,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47),X0) ),
inference(resolution,[],[f488,f779]) ).
fof(f2402,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47),X0) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2401,f2119]) ).
fof(f2421,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47),X0) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2402,f783]) ).
fof(f2435,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47),X0) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2421,f782]) ).
fof(f2444,plain,
( ! [X0] :
( net_str(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47),X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty_carrier(X0) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2435,f781]) ).
fof(f2563,plain,
! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(cast_as_carrier_subset(sK46))
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) ),
inference(resolution,[],[f566,f780]) ).
fof(f2568,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2563,f2119]) ).
fof(f2571,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2568,f783]) ).
fof(f2574,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2571,f782]) ).
fof(f2577,plain,
( ! [X0] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46))))) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2574,f781]) ).
fof(f2580,plain,
( ! [X0] :
( ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| directed_relstr(net_of_bool_filter(X0,cast_as_carrier_subset(sK46),sK47)) )
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2577,f779]) ).
fof(f2586,plain,
( ~ one_sorted_str(sK46)
| empty_carrier(sK46)
| directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(sK46)
| spl50_39 ),
inference(resolution,[],[f2580,f486]) ).
fof(f2588,plain,
( ~ one_sorted_str(sK46)
| empty_carrier(sK46)
| directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| spl50_39 ),
inference(duplicate_literal_removal,[],[f2586]) ).
fof(f2589,plain,
( empty_carrier(sK46)
| directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2588,f821]) ).
fof(f2590,plain,
( directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| spl50_39 ),
inference(forward_subsumption_resolution,[],[f2589,f778]) ).
fof(f2601,plain,
( empty(sK47)
| ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46) ),
inference(resolution,[],[f775,f780]) ).
fof(f2607,plain,
( ~ filtered_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46) ),
inference(forward_subsumption_resolution,[],[f2601,f783]) ).
fof(f2610,plain,
( ~ upper_relstr_subset(sK47,boole_POSet(cast_as_carrier_subset(sK46)))
| sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46) ),
inference(forward_subsumption_resolution,[],[f2607,f782]) ).
fof(f2613,plain,
( sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ element(sK47,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK46)))))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46) ),
inference(forward_subsumption_resolution,[],[f2610,f781]) ).
fof(f2616,plain,
( sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| empty_carrier(sK46)
| ~ one_sorted_str(sK46) ),
inference(forward_subsumption_resolution,[],[f2613,f779]) ).
fof(f2618,plain,
( sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ one_sorted_str(sK46) ),
inference(forward_subsumption_resolution,[],[f2616,f778]) ).
fof(f2620,plain,
sK47 = filter_of_net_str(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)),
inference(forward_subsumption_resolution,[],[f2618,f821]) ).
fof(f2631,plain,
! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) ),
inference(superposition,[],[f773,f2620]) ).
fof(f2632,plain,
! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| empty_carrier(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) ),
inference(superposition,[],[f774,f2620]) ).
fof(f2633,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| ~ spl50_40 ),
inference(forward_subsumption_resolution,[],[f2632,f2364]) ).
fof(f2634,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ transitive_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| ~ spl50_40 ),
inference(forward_subsumption_resolution,[],[f2631,f2364]) ).
fof(f2635,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2633,f2371]) ).
fof(f2636,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ directed_relstr(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2634,f2371]) ).
fof(f2637,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2635,f2590]) ).
fof(f2638,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| empty_carrier(sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2636,f2590]) ).
fof(f2639,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2637,f778]) ).
fof(f2640,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| ~ topological_space(sK46)
| ~ top_str(sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2638,f778]) ).
fof(f2641,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| ~ top_str(sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2639,f777]) ).
fof(f2642,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| ~ top_str(sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2640,f777]) ).
fof(f2643,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2641,f776]) ).
fof(f2644,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46) )
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(forward_subsumption_resolution,[],[f2642,f776]) ).
fof(f2646,definition,
( spl50_45
<=> net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46) ),
introduced(definition,[new_symbols(definition,[spl50_45])],[avatar_definition]) ).
fof(f2648,plain,
( ~ net_str(net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47),sK46)
| spl50_45 ),
inference(avatar_component_clause,[],[f2646]) ).
fof(f2650,definition,
( spl50_46
<=> ! [X0] :
( ~ is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ element(X0,the_carrier(sK46))
| in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ) ),
introduced(definition,[new_symbols(definition,[spl50_46])],[avatar_definition]) ).
fof(f2651,plain,
( ! [X0] :
( in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| ~ is_a_convergence_point_of_set(sK46,sK47,X0) )
| ~ spl50_46 ),
inference(avatar_component_clause,[],[f2650]) ).
fof(f2652,plain,
( ~ spl50_45
| spl50_46
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(avatar_split_clause,[],[f2643,f2244,f2122,f2118,f2650,f2646]) ).
fof(f2654,definition,
( spl50_47
<=> ! [X0] :
( is_a_convergence_point_of_set(sK46,sK47,X0)
| ~ element(X0,the_carrier(sK46))
| ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47))) ) ),
introduced(definition,[new_symbols(definition,[spl50_47])],[avatar_definition]) ).
fof(f2655,plain,
( ! [X0] :
( ~ in(X0,lim_points_of_net(sK46,net_of_bool_filter(sK46,cast_as_carrier_subset(sK46),sK47)))
| ~ element(X0,the_carrier(sK46))
| is_a_convergence_point_of_set(sK46,sK47,X0) )
| ~ spl50_47 ),
inference(avatar_component_clause,[],[f2654]) ).
fof(f2656,plain,
( ~ spl50_45
| spl50_47
| spl50_39
| ~ spl50_40
| ~ spl50_44 ),
inference(avatar_split_clause,[],[f2644,f2244,f2122,f2118,f2654,f2646]) ).
fof(f2660,plain,
( ~ one_sorted_str(sK46)
| ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46)))
| empty_carrier(sK46)
| spl50_39
| spl50_45 ),
inference(resolution,[],[f2648,f2444]) ).
fof(f2661,plain,
( ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46)))
| empty_carrier(sK46)
| spl50_39
| spl50_45 ),
inference(forward_subsumption_resolution,[],[f2660,f821]) ).
fof(f2662,plain,
( ~ element(cast_as_carrier_subset(sK46),powerset(the_carrier(sK46)))
| spl50_39
| spl50_45 ),
inference(forward_subsumption_resolution,[],[f2661,f778]) ).
fof(f2666,plain,
( ~ one_sorted_str(sK46)
| spl50_39
| spl50_45 ),
inference(resolution,[],[f2662,f486]) ).
fof(f2668,plain,
( $false
| spl50_39
| spl50_45 ),
inference(forward_subsumption_resolution,[],[f2666,f821]) ).
fof(f2669,plain,
( spl50_39
| spl50_45 ),
inference(avatar_contradiction_clause,[],[f2668]) ).
fof(f2908,plain,
( ~ element(sK48,the_carrier(sK46))
| ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| spl50_1
| ~ spl50_46 ),
inference(resolution,[],[f2651,f800]) ).
fof(f2910,plain,
( ~ is_a_convergence_point_of_set(sK46,sK47,sK48)
| spl50_1
| ~ spl50_46 ),
inference(forward_subsumption_resolution,[],[f2908,f784]) ).
fof(f2932,plain,
( $false
| spl50_1
| ~ spl50_2
| ~ spl50_46 ),
inference(forward_subsumption_resolution,[],[f2910,f805]) ).
fof(f2933,plain,
( spl50_1
| ~ spl50_2
| ~ spl50_46 ),
inference(avatar_contradiction_clause,[],[f2932]) ).
fof(f2944,plain,
( ~ element(sK48,the_carrier(sK46))
| is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ spl50_1
| ~ spl50_47 ),
inference(resolution,[],[f2655,f801]) ).
fof(f2948,plain,
( is_a_convergence_point_of_set(sK46,sK47,sK48)
| ~ spl50_1
| ~ spl50_47 ),
inference(forward_subsumption_resolution,[],[f2944,f784]) ).
fof(f2950,plain,
( $false
| ~ spl50_1
| spl50_2
| ~ spl50_47 ),
inference(forward_subsumption_resolution,[],[f2948,f804]) ).
fof(f2951,plain,
( ~ spl50_1
| spl50_2
| ~ spl50_47 ),
inference(avatar_contradiction_clause,[],[f2950]) ).
cnf(s1,plain,
( spl50_1
| spl50_2 ),
inference(sat_conversion,[],[f806]) ).
cnf(s2,plain,
( ~ spl50_1
| ~ spl50_2 ),
inference(sat_conversion,[],[f807]) ).
cnf(s28,plain,
( spl50_39
| spl50_40 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s32,plain,
~ spl50_39,
inference(sat_conversion,[],[f2172]) ).
cnf(s33,plain,
( spl50_39
| spl50_44 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s34,plain,
( spl50_39
| ~ spl50_40
| ~ spl50_44
| ~ spl50_45
| spl50_46 ),
inference(sat_conversion,[],[f2652]) ).
cnf(s35,plain,
( spl50_39
| ~ spl50_40
| ~ spl50_44
| ~ spl50_45
| spl50_47 ),
inference(sat_conversion,[],[f2656]) ).
cnf(s36,plain,
( spl50_39
| spl50_45 ),
inference(sat_conversion,[],[f2669]) ).
cnf(s57,plain,
( spl50_1
| ~ spl50_2
| ~ spl50_46 ),
inference(sat_conversion,[],[f2933]) ).
cnf(s58,plain,
( ~ spl50_1
| spl50_2
| ~ spl50_47 ),
inference(sat_conversion,[],[f2951]) ).
cnf(s62,plain,
spl50_45,
inference(rat,[],[s36,s32]) ).
cnf(s63,plain,
spl50_44,
inference(rat,[],[s33,s32]) ).
cnf(s64,plain,
spl50_40,
inference(rat,[],[s28,s32]) ).
cnf(s67,plain,
spl50_47,
inference(rat,[],[s35,s63,s62,s32,s64]) ).
cnf(s68,plain,
spl50_46,
inference(rat,[],[s34,s63,s62,s32,s64]) ).
cnf(s83,plain,
spl50_1,
inference(rat,[],[s1,s57,s68]) ).
cnf(s84,plain,
spl50_2,
inference(rat,[],[s58,s67,s83]) ).
cnf(s85,plain,
$false,
inference(rat,[],[s2,s84,s83]) ).
fof(f2961,plain,
$false,
inference(avatar_sat_refutation,[],[s85]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 05:03:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.26/0.48 % (2036618)Will run a generic schedule for satisfiability detection.
% 0.26/0.48 % (2036626)dis+10_1_sil=32000:sp=arity:random_seed=2885824737:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.26/0.48 % (2036624)% WARNING: option uhcvi not known.
% 0.26/0.48 % (2036623)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1491930137_2999 on theBenchmark for (2999ds/0Mi)
% 0.26/0.48 % (2036627)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=294724346:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.26/0.48 % (2036624)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=968773312:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.26/0.48 % (2036625)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3411015000:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.26/0.48 % (2036628)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1327873794:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.26/0.48 % (2036629)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1064648186:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.26/0.48 % TRYING [1]
% 0.26/0.48 % TRYING [2]
% 0.26/0.48 % (2036626) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2036618-2036626"...
% 0.26/0.48 % (2036626)...printing done.
% 0.26/0.48 % (2036626)Refutation found. Thanks to Tanya!
% 0.26/0.48 % SZS status Theorem for theBenchmark
% 0.26/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.26/0.48 % (2036626)------------------------------
% 0.26/0.48 % (2036626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.26/0.48 % (2036626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.26/0.48 % (2036626)CaDiCaL version: 2.1.3
% 0.26/0.48 % (2036626)Termination reason: Refutation
% 0.26/0.48 % (2036626)Time elapsed: 0.033 s
% 0.26/0.48 % (2036626)Peak memory usage: 13 MB
% 0.26/0.48 % (2036626)Instructions burned: 97 (million)
% 0.26/0.48 % (2036618)Success in time 0.063 s
% 0.26/0.48 % Vampire exiting
%------------------------------------------------------------------------------