%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:20:24 PM UTC 2026
% Result : Theorem 0.23s 10.55s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 9
% Syntax : Number of formulae : 113 ( 16 unt; 0 def)
% Number of atoms : 629 ( 10 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 831 ( 315 ~; 401 |; 93 &)
% ( 4 <=>; 17 =>; 0 <=; 1 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 92 ( 86 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34,axiom,
! [A] :
( one_sorted_str(A)
=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B,C] :
( ( element(C,powerset(the_carrier(boole_POSet(B))))
& upper_relstr_subset(C,boole_POSet(B))
& filtered_subset(C,boole_POSet(B))
& ~ empty(C)
& element(B,powerset(the_carrier(A)))
& ~ empty(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> ( net_str(net_of_bool_filter(A,B,C),A)
& strict_net_str(net_of_bool_filter(A,B,C),A)
& ~ empty_carrier(net_of_bool_filter(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(cast_as_carrier_subset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B,C] :
( ( element(C,powerset(the_carrier(boole_POSet(B))))
& upper_relstr_subset(C,boole_POSet(B))
& filtered_subset(C,boole_POSet(B))
& ~ empty(C)
& element(B,powerset(the_carrier(A)))
& ~ empty(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> ( strict_net_str(net_of_bool_filter(A,B,C),A)
& transitive_relstr(net_of_bool_filter(A,B,C))
& reflexive_relstr(net_of_bool_filter(A,B,C))
& ~ empty_carrier(net_of_bool_filter(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [A,B,C] :
( ( element(C,powerset(the_carrier(boole_POSet(B))))
& proper_element(C,powerset(the_carrier(boole_POSet(B))))
& upper_relstr_subset(C,boole_POSet(B))
& filtered_subset(C,boole_POSet(B))
& ~ empty(C)
& element(B,powerset(the_carrier(A)))
& ~ empty(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> ( directed_relstr(net_of_bool_filter(A,B,C))
& strict_net_str(net_of_bool_filter(A,B,C),A)
& transitive_relstr(net_of_bool_filter(A,B,C))
& reflexive_relstr(net_of_bool_filter(A,B,C))
& ~ empty_carrier(net_of_bool_filter(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,lim_points_of_net(A,B))
<=> is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
=> B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))
<=> is_a_convergence_point_of_set(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))
<=> is_a_convergence_point_of_set(A,B,C) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f127]) ).
fof(f248,plain,
! [A] :
( element(cast_as_carrier_subset(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f249,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f252,plain,
! [A,B,C] :
( ( net_str(net_of_bool_filter(A,B,C),A)
& strict_net_str(net_of_bool_filter(A,B,C),A)
& ~ empty_carrier(net_of_bool_filter(A,B,C)) )
| ~ element(C,powerset(the_carrier(boole_POSet(B))))
| ~ upper_relstr_subset(C,boole_POSet(B))
| ~ filtered_subset(C,boole_POSet(B))
| empty(C)
| ~ element(B,powerset(the_carrier(A)))
| empty(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f253,plain,
! [X0,X1,X2] :
( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f255,plain,
! [X0,X1,X2] :
( net_str(net_of_bool_filter(X0,X1,X2),X0)
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f261,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f262,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f324,plain,
! [A] :
( ~ empty(cast_as_carrier_subset(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f325,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f369,plain,
! [A,B,C] :
( ( strict_net_str(net_of_bool_filter(A,B,C),A)
& transitive_relstr(net_of_bool_filter(A,B,C))
& reflexive_relstr(net_of_bool_filter(A,B,C))
& ~ empty_carrier(net_of_bool_filter(A,B,C)) )
| ~ element(C,powerset(the_carrier(boole_POSet(B))))
| ~ upper_relstr_subset(C,boole_POSet(B))
| ~ filtered_subset(C,boole_POSet(B))
| empty(C)
| ~ element(B,powerset(the_carrier(A)))
| empty(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f372,plain,
! [X0,X1,X2] :
( transitive_relstr(net_of_bool_filter(X0,X1,X2))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f379,plain,
! [A,B,C] :
( ( directed_relstr(net_of_bool_filter(A,B,C))
& strict_net_str(net_of_bool_filter(A,B,C),A)
& transitive_relstr(net_of_bool_filter(A,B,C))
& reflexive_relstr(net_of_bool_filter(A,B,C))
& ~ empty_carrier(net_of_bool_filter(A,B,C)) )
| ~ element(C,powerset(the_carrier(boole_POSet(B))))
| ~ proper_element(C,powerset(the_carrier(boole_POSet(B))))
| ~ upper_relstr_subset(C,boole_POSet(B))
| ~ filtered_subset(C,boole_POSet(B))
| empty(C)
| ~ element(B,powerset(the_carrier(A)))
| empty(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f384,plain,
! [X0,X1,X2] :
( directed_relstr(net_of_bool_filter(X0,X1,X2))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| empty(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f691,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( in(C,lim_points_of_net(A,B))
<=> is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C) )
| ~ element(C,the_carrier(A)) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f125]) ).
fof(f692,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C)
| in(C,lim_points_of_net(A,B)) )
& ( is_a_convergence_point_of_set(A,filter_of_net_str(A,B),C)
| ~ in(C,lim_points_of_net(A,B)) ) )
| ~ element(C,the_carrier(A)) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f691]) ).
fof(f693,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))
| ~ element(X2,the_carrier(X0))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f692]) ).
fof(f694,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))
| ~ element(X2,the_carrier(X0))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f692]) ).
fof(f695,plain,
! [A] :
( ! [B] :
( B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B))
| ~ element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
| ~ proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
| ~ upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
| ~ filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
| empty(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f126]) ).
fof(f696,plain,
! [X0,X1] :
( X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f695]) ).
fof(f697,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)))
<~> is_a_convergence_point_of_set(A,B,C) )
& element(C,the_carrier(A)) )
& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f128]) ).
fof(f698,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ is_a_convergence_point_of_set(A,B,C)
| ~ in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B))) )
& ( is_a_convergence_point_of_set(A,B,C)
| in(C,lim_points_of_net(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B))) )
& element(C,the_carrier(A)) )
& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& ~ empty(B) )
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f697]) ).
fof(f699,plain,
( ( ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))) )
& ( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))) )
& element(sK47_skl,the_carrier(sK45_skl))
& element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
& proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
& upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
& filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
& ~ empty(sK46_skl)
& top_str(sK45_skl)
& topological_space(sK45_skl)
& ~ empty_carrier(sK45_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl,sK46_skl,sK47_skl]),skolemize(A,sK45_skl),skolemize(B,sK46_skl),skolemize(C,sK47_skl)],[f698]) ).
fof(f700,plain,
~ empty_carrier(sK45_skl),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f701,plain,
topological_space(sK45_skl),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f702,plain,
top_str(sK45_skl),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f703,plain,
~ empty(sK46_skl),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f704,plain,
filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f705,plain,
upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f706,plain,
proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f707,plain,
element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl))))),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f708,plain,
element(sK47_skl,the_carrier(sK45_skl)),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f709,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))) ),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f710,plain,
( ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))) ),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f739,plain,
one_sorted_str(sK45_skl),
inference(resolution,[status(thm)],[f262,f702]) ).
fof(f740,plain,
element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl))),
inference(resolution,[status(thm)],[f249,f739]) ).
fof(f774,plain,
! [X0] :
( ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl)
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(resolution,[status(thm)],[f253,f707]) ).
fof(f775,plain,
! [X0] :
( ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f774,f703]) ).
fof(f779,plain,
! [X0] :
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0),sK45_skl)
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(resolution,[status(thm)],[f255,f740]) ).
fof(f783,plain,
! [X0] :
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0),sK45_skl)
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f779,f700]) ).
fof(f870,plain,
! [X0] :
( ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(X0)))
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f775,f704]) ).
fof(f889,plain,
! [X0] :
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(resolution,[status(thm)],[f372,f740]) ).
fof(f893,plain,
! [X0] :
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f889,f700]) ).
fof(f942,plain,
! [X0] :
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f893,f739]) ).
fof(f943,plain,
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f942,f707]) ).
fof(f944,plain,
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f943,f703]) ).
fof(f950,plain,
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f704]) ).
fof(f951,plain,
( transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f950,f705]) ).
fof(f952,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)),sK47_skl)
| ~ element(sK47_skl,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl)
| ~ topological_space(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(resolution,[status(thm)],[f693,f709]) ).
fof(f953,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)),sK47_skl)
| ~ element(sK47_skl,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl)
| ~ topological_space(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f952,f700]) ).
fof(f979,plain,
! [X0] :
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0),sK45_skl)
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f783,f739]) ).
fof(f980,plain,
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f979,f707]) ).
fof(f981,plain,
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f980,f703]) ).
fof(f982,plain,
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f981,f704]) ).
fof(f983,plain,
( net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f982,f705]) ).
fof(f993,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| is_a_convergence_point_of_set(sK45_skl,filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)),sK47_skl)
| ~ element(sK47_skl,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f953,f701]) ).
fof(f1002,plain,
! [X0] :
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(resolution,[status(thm)],[f384,f740]) ).
fof(f1006,plain,
! [X0] :
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1002,f700]) ).
fof(f1007,plain,
( sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl)
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(resolution,[status(thm)],[f696,f707]) ).
fof(f1008,plain,
( sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl)
| ~ one_sorted_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1007,f700]) ).
fof(f1009,plain,
( sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1008,f739]) ).
fof(f1010,plain,
( sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl) ),
inference(resolution,[status(thm)],[f1009,f706]) ).
fof(f1011,plain,
( sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f703]) ).
fof(f1012,plain,
( sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1011,f704]) ).
fof(f1013,plain,
sK46_skl = filter_of_net_str(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)),
inference(resolution,[status(thm)],[f1012,f705]) ).
fof(f1015,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ element(sK47_skl,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl) ),
inference(backward_demodulation,[status(thm)],[f1013,f993]) ).
fof(f1018,plain,
! [X0] :
( ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl)
| ~ topological_space(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(paramodulation,[status(thm)],[f1013,f694]) ).
fof(f1019,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ element(sK47_skl,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1015]) ).
fof(f1020,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ element(sK47_skl,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1019,f702]) ).
fof(f1021,plain,
! [X0] :
( ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl)
| ~ topological_space(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1018,f700]) ).
fof(f1023,plain,
( is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1020,f708]) ).
fof(f1024,plain,
( empty(cast_as_carrier_subset(sK45_skl))
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(resolution,[status(thm)],[f1023,f983]) ).
fof(f1025,plain,
( empty(cast_as_carrier_subset(sK45_skl))
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1024,f951]) ).
fof(f1081,plain,
! [X0] :
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),X0))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(X0)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1006,f739]) ).
fof(f1082,plain,
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(sK46_skl)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f1081,f707]) ).
fof(f1083,plain,
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ filtered_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1082,f703]) ).
fof(f1084,plain,
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ proper_element(sK46_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK45_skl)))))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1083,f704]) ).
fof(f1085,plain,
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f1084,f706]) ).
fof(f1086,plain,
( directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1085,f705]) ).
fof(f1087,plain,
( empty(cast_as_carrier_subset(sK45_skl))
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1025,f1086]) ).
fof(f1088,plain,
! [X0] :
( ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| ~ net_str(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl),sK45_skl)
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1021,f701]) ).
fof(f1089,plain,
! [X0] :
( empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ top_str(sK45_skl) ),
inference(resolution,[status(thm)],[f1088,f983]) ).
fof(f1090,plain,
! [X0] :
( empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| ~ transitive_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1089,f702]) ).
fof(f1147,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl)
| empty(cast_as_carrier_subset(sK45_skl))
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl) ),
inference(resolution,[status(thm)],[f1087,f870]) ).
fof(f1148,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl)
| empty(cast_as_carrier_subset(sK45_skl))
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1147]) ).
fof(f1149,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl)
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1148,f325]) ).
fof(f1150,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| ~ one_sorted_str(sK45_skl)
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1149,f700]) ).
fof(f1151,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ one_sorted_str(sK45_skl)
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl) ),
inference(resolution,[status(thm)],[f1150,f740]) ).
fof(f1152,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1151,f739]) ).
fof(f1153,plain,
~ in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))),
inference(backward_subsumption_resolution,[status(thm)],[f710,f1154]) ).
fof(f1154,plain,
is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1152,f705]) ).
fof(f1218,plain,
! [X0] :
( empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| ~ directed_relstr(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1090,f951]) ).
fof(f1219,plain,
! [X0] :
( empty(cast_as_carrier_subset(sK45_skl))
| empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(resolution,[status(thm)],[f1218,f1086]) ).
fof(f1220,plain,
! [X0] :
( empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,X0)
| in(X0,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| ~ element(X0,the_carrier(sK45_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1219]) ).
fof(f1221,plain,
( empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| in(sK47_skl,lim_points_of_net(sK45_skl,net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(resolution,[status(thm)],[f1220,f708]) ).
fof(f1222,plain,
( empty(cast_as_carrier_subset(sK45_skl))
| ~ is_a_convergence_point_of_set(sK45_skl,sK46_skl,sK47_skl)
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1221,f1153]) ).
fof(f1223,plain,
( empty(cast_as_carrier_subset(sK45_skl))
| empty_carrier(net_of_bool_filter(sK45_skl,cast_as_carrier_subset(sK45_skl),sK46_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1222,f1154]) ).
fof(f1224,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| empty(cast_as_carrier_subset(sK45_skl))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(resolution,[status(thm)],[f1223,f870]) ).
fof(f1225,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl)
| empty(cast_as_carrier_subset(sK45_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1224]) ).
fof(f1226,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| ~ one_sorted_str(sK45_skl)
| empty_carrier(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1225,f325]) ).
fof(f1290,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ element(cast_as_carrier_subset(sK45_skl),powerset(the_carrier(sK45_skl)))
| ~ one_sorted_str(sK45_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1226,f700]) ).
fof(f1291,plain,
( ~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl)))
| ~ one_sorted_str(sK45_skl) ),
inference(resolution,[status(thm)],[f1290,f740]) ).
fof(f1292,plain,
~ upper_relstr_subset(sK46_skl,boole_POSet(cast_as_carrier_subset(sK45_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1291,f739]) ).
fof(f1293,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1292,f705]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/10.46 % Computer : n002.cluster.edu
% 0.18/10.46 % Model : x86_64 x86_64
% 0.18/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.46 % Memory : 8046.5625MB
% 0.18/10.46 % OS : Linux 6.8.0-71-generic
% 0.18/10.46 % CPULimit : 300
% 0.18/10.46 % WCLimit : 300
% 0.18/10.46 % DateTime : Mon Sep 21 06:22:14 UTC 2026
% 0.18/10.46 % CPUTime :
% 0.18/10.49 % Drodi V4.1.1
% 0.23/10.55 % Refutation found
% 0.23/10.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/10.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/10.58 % Elapsed time: 0.098739 seconds
% 0.23/10.58 % CPU time: 0.426856 seconds
% 0.23/10.58 % Total memory used: 83.636 MB
% 0.23/10.58 % Net memory used: 83.423 MB
%------------------------------------------------------------------------------