%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU395+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:57:20 PM UTC 2026
% Result : Theorem 18.90s 4.37s
% Output : CNFRefutation 18.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of formulae : 173 ( 46 unt; 0 def)
% Number of atoms : 926 ( 29 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 1245 ( 492 ~; 598 |; 128 &)
% ( 5 <=>; 20 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 233 ( 0 sgn 221 !; 12 ?; 90 :)
% Comments :
%------------------------------------------------------------------------------
fof(f167,axiom,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_yellow_1) ).
fof(f236,axiom,
! [X0,X1] :
( ( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1)
& top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_yellow_6) ).
fof(f268,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(f286,axiom,
! [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) )
=> ( net_str(net_of_bool_filter(X0,X1,X2),X0)
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow19) ).
fof(f326,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f408,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ~ empty(cast_as_carrier_subset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_pre_topc) ).
fof(f451,axiom,
! [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) )
=> ( strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_yellow19) ).
fof(f458,axiom,
! [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) )
=> ( directed_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_yellow19) ).
fof(f591,axiom,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f689,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f698,axiom,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( net_str(X1,X0)
& directed_relstr(X1)
& transitive_relstr(X1)
& ~ empty_carrier(X1) )
=> ! [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(f711,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(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) )
=> 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(f730,conjecture,
! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(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) )
=> ! [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(f731,negated_conjecture,
~ ! [X0] :
( ( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(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) )
=> ! [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)],[f730]) ).
fof(f848,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X2))
& in(X0,X1) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f849,axiom,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_waybel_7) ).
fof(f1330,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f236]) ).
fof(f1331,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(flattening,[],[f1330]) ).
fof(f1359,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f268]) ).
fof(f1373,plain,
! [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)
| ( net_str(net_of_bool_filter(X0,X1,X2),X0)
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f286]) ).
fof(f1374,plain,
! [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)
| ( net_str(net_of_bool_filter(X0,X1,X2),X0)
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(flattening,[],[f1373]) ).
fof(f1426,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(ennf_transformation,[],[f326]) ).
fof(f1509,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(ennf_transformation,[],[f408]) ).
fof(f1510,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(flattening,[],[f1509]) ).
fof(f1570,plain,
! [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)
| ( strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f451]) ).
fof(f1571,plain,
! [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)
| ( strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(flattening,[],[f1570]) ).
fof(f1584,plain,
! [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)
| ( directed_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f458]) ).
fof(f1585,plain,
! [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)
| ( directed_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ) ),
inference(flattening,[],[f1584]) ).
fof(f1851,plain,
! [X0] :
( ~ one_sorted_str(X0)
| cast_as_carrier_subset(X0) = the_carrier(X0) ),
inference(ennf_transformation,[],[f689]) ).
fof(f1865,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(ennf_transformation,[],[f698]) ).
fof(f1866,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
inference(flattening,[],[f1865]) ).
fof(f1884,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(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)
| X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(ennf_transformation,[],[f711]) ).
fof(f1885,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(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)
| X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(flattening,[],[f1884]) ).
fof(f1911,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(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)
& ? [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(ennf_transformation,[],[f731]) ).
fof(f1912,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(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)
& ? [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(flattening,[],[f1911]) ).
fof(f2070,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(ennf_transformation,[],[f848]) ).
fof(f2071,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(flattening,[],[f2070]) ).
fof(f3054,plain,
! [X0] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ! [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) )
& ( ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1)) ) ) ) ) ),
inference(nnf_transformation,[],[f1866]) ).
fof(f3072,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(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)
& ? [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) )
& ( ~ 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(nnf_transformation,[],[f1912]) ).
fof(f3073,plain,
? [X0] :
( top_str(X0)
& topological_space(X0)
& ~ empty_carrier(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)
& ? [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) )
& ( ~ 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(flattening,[],[f3072]) ).
fof(f3074,plain,
( top_str(sK621)
& topological_space(sK621)
& ~ empty_carrier(sK621)
& element(sK622,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK621)))))
& proper_element(sK622,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK621)))))
& upper_relstr_subset(sK622,boole_POSet(cast_as_carrier_subset(sK621)))
& filtered_subset(sK622,boole_POSet(cast_as_carrier_subset(sK621)))
& ~ empty(sK622)
& element(sK623,the_carrier(sK621))
& ( in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| is_a_convergence_point_of_set(sK621,sK622,sK623) )
& ( ~ in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| ~ is_a_convergence_point_of_set(sK621,sK622,sK623) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK621,sK622,sK623]),skolemize(X0,sK621),skolemize(X1,sK622),skolemize(X2,sK623)],[f3073]) ).
fof(f3790,plain,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
inference(cnf_transformation,[],[f167]) ).
fof(f4078,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f1331]) ).
fof(f4109,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f1359]) ).
fof(f4125,plain,
! [X2,X0,X1] :
( ~ 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)
| net_str(net_of_bool_filter(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f1374]) ).
fof(f4173,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1426]) ).
fof(f4388,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(cnf_transformation,[],[f1510]) ).
fof(f4537,plain,
! [X2,X0,X1] :
( ~ 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)
| transitive_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f1571]) ).
fof(f4539,plain,
! [X2,X0,X1] :
( ~ 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)
| ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f1571]) ).
fof(f4562,plain,
! [X2,X0,X1] :
( ~ 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)
| directed_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(cnf_transformation,[],[f1585]) ).
fof(f5171,plain,
! [X0] : powerset(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f591]) ).
fof(f5755,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f1851]) ).
fof(f5773,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X0))
| ~ in(X2,lim_points_of_net(X0,X1))
| is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ),
inference(cnf_transformation,[],[f3054]) ).
fof(f5774,plain,
! [X2,X0,X1] :
( ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X0))
| ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1)) ),
inference(cnf_transformation,[],[f3054]) ).
fof(f5790,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ 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)
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1 ),
inference(cnf_transformation,[],[f1885]) ).
fof(f5827,plain,
top_str(sK621),
inference(cnf_transformation,[],[f3074]) ).
fof(f5828,plain,
topological_space(sK621),
inference(cnf_transformation,[],[f3074]) ).
fof(f5829,plain,
~ empty_carrier(sK621),
inference(cnf_transformation,[],[f3074]) ).
fof(f5830,plain,
element(sK622,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK621))))),
inference(cnf_transformation,[],[f3074]) ).
fof(f5831,plain,
proper_element(sK622,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK621))))),
inference(cnf_transformation,[],[f3074]) ).
fof(f5832,plain,
upper_relstr_subset(sK622,boole_POSet(cast_as_carrier_subset(sK621))),
inference(cnf_transformation,[],[f3074]) ).
fof(f5833,plain,
filtered_subset(sK622,boole_POSet(cast_as_carrier_subset(sK621))),
inference(cnf_transformation,[],[f3074]) ).
fof(f5834,plain,
~ empty(sK622),
inference(cnf_transformation,[],[f3074]) ).
fof(f5835,plain,
element(sK623,the_carrier(sK621)),
inference(cnf_transformation,[],[f3074]) ).
fof(f5836,plain,
( in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| is_a_convergence_point_of_set(sK621,sK622,sK623) ),
inference(cnf_transformation,[],[f3074]) ).
fof(f5837,plain,
( ~ in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| ~ is_a_convergence_point_of_set(sK621,sK622,sK623) ),
inference(cnf_transformation,[],[f3074]) ).
fof(f6047,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f2071]) ).
fof(f6048,plain,
! [X0] : powerset(X0) = the_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f849]) ).
fof(f6395,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| element(lim_points_of_net(X0,X1),k1_pcomps_1(the_carrier(X0))) ),
inference(definition_unfolding,[],[f4078,f5171]) ).
fof(f6401,plain,
! [X0] :
( ~ one_sorted_str(X0)
| element(cast_as_carrier_subset(X0),k1_pcomps_1(the_carrier(X0))) ),
inference(definition_unfolding,[],[f4109,f5171]) ).
fof(f6410,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| empty(X2)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| net_str(net_of_bool_filter(X0,X1,X2),X0) ),
inference(definition_unfolding,[],[f4125,f5171,f3790,f3790,f5171,f3790]) ).
fof(f6561,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| empty(X2)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ),
inference(definition_unfolding,[],[f4539,f5171,f3790,f3790,f5171,f3790]) ).
fof(f6563,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| empty(X2)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| transitive_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(definition_unfolding,[],[f4537,f5171,f3790,f3790,f5171,f3790]) ).
fof(f6569,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ proper_element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| empty(X2)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| directed_relstr(net_of_bool_filter(X0,X1,X2)) ),
inference(definition_unfolding,[],[f4562,f5171,f3790,f3790,f5171,f3790,f5171,f3790]) ).
fof(f7005,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| ~ proper_element(X1,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| ~ upper_relstr_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ filtered_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| empty(X1)
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1 ),
inference(definition_unfolding,[],[f5790,f3790,f3790,f5171,f3790,f5171,f3790]) ).
fof(f7016,plain,
filtered_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))),
inference(definition_unfolding,[],[f5833,f3790]) ).
fof(f7017,plain,
upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))),
inference(definition_unfolding,[],[f5832,f3790]) ).
fof(f7018,plain,
proper_element(sK622,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))))),
inference(definition_unfolding,[],[f5831,f5171,f3790]) ).
fof(f7019,plain,
element(sK622,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))))),
inference(definition_unfolding,[],[f5830,f5171,f3790]) ).
fof(f7092,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(definition_unfolding,[],[f6047,f5171]) ).
fof(f7093,plain,
! [X0] : k1_pcomps_1(X0) = the_carrier(poset_of_lattice(boole_lattice(X0))),
inference(definition_unfolding,[],[f6048,f5171,f3790]) ).
tcf(c_892,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| element(lim_points_of_net(X1,X0),k1_pcomps_1(the_carrier(X1)))
| ~ directed_relstr(X0)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X0)
| ~ net_str(X0,X1) ),
inference(cnf_transformation,[],[f6395]) ).
tcf(c_923,plain,
! [X0: $i] :
( element(cast_as_carrier_subset(X0),k1_pcomps_1(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f6401]) ).
tcf(c_941,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| net_str(net_of_bool_filter(X2,X1,X0),X2)
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(cnf_transformation,[],[f6410]) ).
tcf(c_987,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f4173]) ).
tcf(c_1202,plain,
! [X0: $i] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(cnf_transformation,[],[f4388]) ).
tcf(c_1350,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ empty_carrier(net_of_bool_filter(X2,X1,X0))
| ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(cnf_transformation,[],[f6561]) ).
tcf(c_1352,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| transitive_relstr(net_of_bool_filter(X2,X1,X0))
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(cnf_transformation,[],[f6563]) ).
tcf(c_1380,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| directed_relstr(net_of_bool_filter(X2,X1,X0))
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ proper_element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(cnf_transformation,[],[f6569]) ).
tcf(c_2566,plain,
! [X0: $i] :
( ( the_carrier(X0) = cast_as_carrier_subset(X0) )
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f5755]) ).
tcf(c_2584,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| empty_carrier(X0)
| in(X2,lim_points_of_net(X0,X1))
| ~ directed_relstr(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X0))
| ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ),
inference(cnf_transformation,[],[f5774]) ).
tcf(c_2585,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_a_convergence_point_of_set(X1,filter_of_net_str(X1,X2),X0)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ element(X0,the_carrier(X1))
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(cnf_transformation,[],[f5773]) ).
tcf(c_2601,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| ( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0)) = X0 )
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ proper_element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))))
| ~ element(X0,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1)))))) ),
inference(cnf_transformation,[],[f7005]) ).
tcf(c_2638,negated_conjecture,
( ~ is_a_convergence_point_of_set(sK621,sK622,sK623)
| ~ in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))) ),
inference(cnf_transformation,[],[f5837]) ).
tcf(c_2639,negated_conjecture,
( is_a_convergence_point_of_set(sK621,sK622,sK623)
| in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))) ),
inference(cnf_transformation,[],[f5836]) ).
tcf(c_2640,negated_conjecture,
element(sK623,the_carrier(sK621)),
inference(cnf_transformation,[],[f5835]) ).
tcf(c_2641,negated_conjecture,
~ empty(sK622),
inference(cnf_transformation,[],[f5834]) ).
tcf(c_2642,negated_conjecture,
filtered_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))),
inference(cnf_transformation,[],[f7016]) ).
tcf(c_2643,negated_conjecture,
upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))),
inference(cnf_transformation,[],[f7017]) ).
tcf(c_2644,negated_conjecture,
proper_element(sK622,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))))),
inference(cnf_transformation,[],[f7018]) ).
tcf(c_2645,negated_conjecture,
element(sK622,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621)))))),
inference(cnf_transformation,[],[f7019]) ).
tcf(c_2646,negated_conjecture,
~ empty_carrier(sK621),
inference(cnf_transformation,[],[f5829]) ).
tcf(c_2647,negated_conjecture,
topological_space(sK621),
inference(cnf_transformation,[],[f5828]) ).
tcf(c_2648,negated_conjecture,
top_str(sK621),
inference(cnf_transformation,[],[f5827]) ).
tcf(c_2856,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,k1_pcomps_1(X1)) ),
inference(cnf_transformation,[],[f7092]) ).
tcf(c_2857,plain,
! [X0: $i] : the_carrier(poset_of_lattice(boole_lattice(X0))) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f7093]) ).
tcf(c_3295,plain,
one_sorted_str(sK621),
inference(superposition,[status(thm)],[c_2648,c_987]) ).
tcf(c_3314,plain,
element(sK622,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))),
inference(demodulation,[status(thm)],[c_2645,c_2857]) ).
tcf(c_3315,plain,
proper_element(sK622,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))),
inference(demodulation,[status(thm)],[c_2644,c_2857]) ).
tcf(c_3522,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| element(X0,the_carrier(X1))
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(superposition,[status(thm)],[c_892,c_2856]) ).
tcf(c_3627,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_a_convergence_point_of_set(X1,filter_of_net_str(X1,X2),X0)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(global_subsumption_just,[status(thm)],[c_2585,c_2585,c_3522]) ).
tcf(c_3770,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| transitive_relstr(net_of_bool_filter(X2,X1,X0))
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(X1))) ),
inference(demodulation,[status(thm)],[c_1352,c_2857]) ).
tcf(c_3791,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| empty(cast_as_carrier_subset(X1))
| transitive_relstr(net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0))
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1)))) ),
inference(superposition,[status(thm)],[c_923,c_3770]) ).
tcf(c_3844,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| net_str(net_of_bool_filter(X2,X1,X0),X2)
| ~ one_sorted_str(X2)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(X1))) ),
inference(demodulation,[status(thm)],[c_941,c_2857]) ).
tcf(c_3900,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X2)
| empty(X1)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(k1_pcomps_1(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ empty_carrier(net_of_bool_filter(X0,X1,X2)) ),
inference(demodulation,[status(thm)],[c_1350,c_2857]) ).
tcf(c_3921,plain,
! [X0: $i,X1: $i] :
( empty(X1)
| empty_carrier(X0)
| empty(cast_as_carrier_subset(X0))
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ filtered_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ element(X1,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ),
inference(superposition,[status(thm)],[c_923,c_3900]) ).
tcf(c_3931,plain,
one_sorted_str(sK621),
inference(superposition,[status(thm)],[c_2648,c_987]) ).
tcf(c_3977,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| empty_carrier(X2)
| directed_relstr(net_of_bool_filter(X2,X1,X0))
| ~ one_sorted_str(X2)
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(X1)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(X1)))
| ~ element(X1,k1_pcomps_1(the_carrier(X2)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(X1))) ),
inference(demodulation,[status(thm)],[c_1380,c_2857]) ).
tcf(c_4000,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| empty(cast_as_carrier_subset(X1))
| directed_relstr(net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0))
| ~ one_sorted_str(X1)
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1)))) ),
inference(superposition,[status(thm)],[c_923,c_3977]) ).
tcf(c_4016,plain,
proper_element(sK622,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))),
inference(demodulation,[status(thm)],[c_2644,c_2857]) ).
tcf(c_4119,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| ( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0)) = X0 )
| ~ one_sorted_str(X1)
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1)))) ),
inference(demodulation,[status(thm)],[c_2601,c_2857]) ).
tcf(c_4136,plain,
( empty(sK622)
| empty_carrier(sK621)
| ( filter_of_net_str(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) = sK622 )
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(superposition,[status(thm)],[c_3315,c_4119]) ).
tcf(c_4141,plain,
the_carrier(sK621) = cast_as_carrier_subset(sK621),
inference(superposition,[status(thm)],[c_3295,c_2566]) ).
tcf(c_4144,plain,
proper_element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))),
inference(demodulation,[status(thm)],[c_3315,c_4141]) ).
tcf(c_4145,plain,
element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))),
inference(demodulation,[status(thm)],[c_3314,c_4141]) ).
tcf(c_4146,plain,
filtered_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621)))),
inference(demodulation,[status(thm)],[c_2642,c_4141]) ).
tcf(c_4147,plain,
upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621)))),
inference(demodulation,[status(thm)],[c_2643,c_4141]) ).
tcf(c_5016,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| transitive_relstr(net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0))
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3791,c_1202]) ).
tcf(c_5378,plain,
! [X0: $i,X1: $i] :
( empty(X1)
| empty_carrier(X0)
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| ~ element(X1,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| ~ filtered_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ upper_relstr_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ one_sorted_str(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3921,c_1202,c_3921]) ).
tcf(c_5379,plain,
! [X0: $i,X1: $i] :
( empty(X1)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ filtered_subset(X1,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))
| ~ element(X1,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| ~ empty_carrier(net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ),
inference(renaming,[status(thm)],[c_5378]) ).
tcf(c_5397,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X2)
| empty_carrier(X1)
| is_a_convergence_point_of_set(X1,filter_of_net_str(X1,X2),X0)
| ~ directed_relstr(X2)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ transitive_relstr(X2)
| ~ net_str(X2,X1)
| ~ in(X0,lim_points_of_net(X1,X2)) ),
inference(global_subsumption_just,[status(thm)],[c_2585,c_2585,c_3522]) ).
tcf(c_5603,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| directed_relstr(net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0))
| ~ one_sorted_str(X1)
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4000,c_1202]) ).
tcf(c_5838,plain,
( ( filter_of_net_str(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) = sK622 )
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(global_subsumption_just,[status(thm)],[c_4136,c_2646,c_2641,c_2643,c_2642,c_3295,c_4136]) ).
tcf(c_5891,plain,
! [X0: $i] :
( empty_carrier(sK621)
| empty(X0)
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| ~ empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0)) ),
inference(superposition,[status(thm)],[c_4141,c_5379]) ).
tcf(c_5896,plain,
( element(the_carrier(sK621),k1_pcomps_1(the_carrier(sK621)))
| ~ one_sorted_str(sK621) ),
inference(superposition,[status(thm)],[c_4141,c_923]) ).
tcf(c_5899,plain,
( empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ empty(the_carrier(sK621)) ),
inference(superposition,[status(thm)],[c_4141,c_1202]) ).
tcf(c_5900,plain,
! [X0: $i] :
( empty_carrier(sK621)
| empty(X0)
| directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| ~ one_sorted_str(sK621)
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(superposition,[status(thm)],[c_4141,c_5603]) ).
tcf(c_5902,plain,
! [X0: $i] :
( empty_carrier(sK621)
| empty(X0)
| transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(superposition,[status(thm)],[c_4141,c_5016]) ).
tcf(c_5910,plain,
( ( filter_of_net_str(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) = sK622 )
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))) ),
inference(superposition,[status(thm)],[c_4141,c_5838]) ).
tcf(c_6149,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| ( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0)) = X0 )
| ~ one_sorted_str(X1)
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(X1))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X1)))) ),
inference(demodulation,[status(thm)],[c_2601,c_2857]) ).
tcf(c_6166,plain,
( empty(sK622)
| empty_carrier(sK621)
| ( filter_of_net_str(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) = sK622 )
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(superposition,[status(thm)],[c_4016,c_6149]) ).
tcf(c_6171,plain,
the_carrier(sK621) = cast_as_carrier_subset(sK621),
inference(superposition,[status(thm)],[c_3931,c_2566]) ).
tcf(c_6172,plain,
( ~ is_a_convergence_point_of_set(sK621,sK622,sK623)
| ~ in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,the_carrier(sK621),sK622))) ),
inference(demodulation,[status(thm)],[c_2638,c_6171]) ).
tcf(c_6173,plain,
( is_a_convergence_point_of_set(sK621,sK622,sK623)
| in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,the_carrier(sK621),sK622))) ),
inference(demodulation,[status(thm)],[c_2639,c_6171]) ).
tcf(c_9440,plain,
filter_of_net_str(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) = sK622,
inference(global_subsumption_just,[status(thm)],[c_5910,c_4145,c_5910]) ).
tcf(c_9442,plain,
filter_of_net_str(sK621,net_of_bool_filter(sK621,the_carrier(sK621),sK622)) = sK622,
inference(light_normalisation,[status(thm)],[c_9440,c_4141]) ).
tcf(c_9444,plain,
! [X0: $i] :
( empty_carrier(sK621)
| is_a_convergence_point_of_set(sK621,sK622,X0)
| empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ top_str(sK621)
| ~ topological_space(sK621)
| ~ directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,the_carrier(sK621),sK622),sK621)
| ~ in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,the_carrier(sK621),sK622))) ),
inference(superposition,[status(thm)],[c_9442,c_3627]) ).
tcf(c_9552,plain,
! [X0: $i] :
( ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| empty(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5902,c_2646,c_3295,c_5902]) ).
tcf(c_9553,plain,
! [X0: $i] :
( empty(X0)
| transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(renaming,[status(thm)],[c_9552]) ).
tcf(c_9560,plain,
! [X0: $i] :
( empty(X0)
| transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),X0))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))) ),
inference(light_normalisation,[status(thm)],[c_9553,c_4141]) ).
tcf(c_9572,plain,
( empty(sK622)
| transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))) ),
inference(superposition,[status(thm)],[c_4146,c_9560]) ).
tcf(c_9610,plain,
! [X0: $i] :
( ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| ~ empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| empty(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5891,c_2646,c_3295,c_5891]) ).
tcf(c_9611,plain,
! [X0: $i] :
( empty(X0)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| ~ empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0)) ),
inference(renaming,[status(thm)],[c_9610]) ).
tcf(c_9618,plain,
! [X0: $i] :
( empty(X0)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621))))
| ~ empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),X0)) ),
inference(light_normalisation,[status(thm)],[c_9611,c_4141]) ).
tcf(c_9630,plain,
( empty(sK622)
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621))))
| ~ empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),sK622)) ),
inference(superposition,[status(thm)],[c_4146,c_9618]) ).
tcf(c_9631,plain,
filter_of_net_str(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) = sK622,
inference(global_subsumption_just,[status(thm)],[c_6166,c_4145,c_5910]) ).
tcf(c_9634,plain,
! [X0: $i] :
( empty_carrier(sK621)
| empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| ~ top_str(sK621)
| ~ topological_space(sK621)
| ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ element(X0,the_carrier(sK621))
| ~ directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622),sK621) ),
inference(superposition,[status(thm)],[c_9631,c_2584]) ).
tcf(c_9635,plain,
! [X0: $i] :
( empty_carrier(sK621)
| is_a_convergence_point_of_set(sK621,sK622,X0)
| empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ top_str(sK621)
| ~ topological_space(sK621)
| ~ directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622),sK621)
| ~ in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))) ),
inference(superposition,[status(thm)],[c_9631,c_5397]) ).
tcf(c_9684,plain,
! [X0: $i] :
( ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| empty(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5900,c_2646,c_3295,c_5900]) ).
tcf(c_9685,plain,
! [X0: $i] :
( empty(X0)
| directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),X0))
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(cast_as_carrier_subset(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(sK621)))) ),
inference(renaming,[status(thm)],[c_9684]) ).
tcf(c_9693,plain,
! [X0: $i] :
( empty(X0)
| directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),X0))
| ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621))))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))) ),
inference(light_normalisation,[status(thm)],[c_9685,c_4141]) ).
tcf(c_9707,plain,
( empty(sK622)
| directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ proper_element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621))))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621)))) ),
inference(superposition,[status(thm)],[c_4146,c_9693]) ).
tcf(c_15359,plain,
! [X0: $i] :
( ~ in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| ~ net_str(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622),sK621)
| ~ transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| is_a_convergence_point_of_set(sK621,sK622,X0) ),
inference(global_subsumption_just,[status(thm)],[c_9635,c_2648,c_2647,c_2646,c_9635]) ).
tcf(c_15360,plain,
! [X0: $i] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622),sK621)
| ~ in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))) ),
inference(renaming,[status(thm)],[c_15359]) ).
tcf(c_15368,plain,
! [X0: $i] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,the_carrier(sK621),sK622),sK621)
| ~ in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,the_carrier(sK621),sK622))) ),
inference(light_normalisation,[status(thm)],[c_15360,c_6171]) ).
tcf(c_15382,plain,
( is_a_convergence_point_of_set(sK621,sK622,sK623)
| empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,the_carrier(sK621),sK622),sK621) ),
inference(superposition,[status(thm)],[c_6173,c_15368]) ).
tcf(c_15504,plain,
! [X0: $i] :
( ~ net_str(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622),sK621)
| ~ transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ element(X0,the_carrier(sK621))
| ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)) ),
inference(global_subsumption_just,[status(thm)],[c_9634,c_2648,c_2647,c_2646,c_9634]) ).
tcf(c_15505,plain,
! [X0: $i] :
( empty_carrier(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622)))
| ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ element(X0,the_carrier(sK621))
| ~ directed_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622),sK621) ),
inference(renaming,[status(thm)],[c_15504]) ).
tcf(c_15514,plain,
! [X0: $i] :
( empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| in(X0,lim_points_of_net(sK621,net_of_bool_filter(sK621,the_carrier(sK621),sK622)))
| ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ element(X0,the_carrier(sK621))
| ~ directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,the_carrier(sK621),sK622),sK621) ),
inference(light_normalisation,[status(thm)],[c_15505,c_6171]) ).
tcf(c_15544,plain,
( empty_carrier(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ is_a_convergence_point_of_set(sK621,sK622,sK623)
| ~ element(sK623,the_carrier(sK621))
| ~ directed_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ transitive_relstr(net_of_bool_filter(sK621,the_carrier(sK621),sK622))
| ~ net_str(net_of_bool_filter(sK621,the_carrier(sK621),sK622),sK621) ),
inference(superposition,[status(thm)],[c_15514,c_6172]) ).
tcf(c_16240,plain,
~ net_str(net_of_bool_filter(sK621,the_carrier(sK621),sK622),sK621),
inference(global_subsumption_just,[status(thm)],[c_9444,c_2641,c_2640,c_4147,c_4145,c_4144,c_9572,c_9630,c_9707,c_15382,c_15544]) ).
tcf(c_16242,plain,
( empty(sK622)
| empty_carrier(sK621)
| empty(the_carrier(sK621))
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(the_carrier(sK621))))
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(the_carrier(sK621))))
| ~ element(the_carrier(sK621),k1_pcomps_1(the_carrier(sK621))) ),
inference(superposition,[status(thm)],[c_3844,c_16240]) ).
tcf(c_16243,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_16242,c_5896,c_5899,c_4145,c_4146,c_4147,c_3295,c_2641,c_2646]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU395+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.08 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.44 % Computer : n019.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Thu Sep 24 13:58:50 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.26/0.50 Running first-order theorem proving
% 0.26/0.50 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.26/0.52
% 0.26/0.52 % ======== iProver multi-core TPTP/SMT =========
% 0.26/0.52
% 0.26/0.52 % Detected problem language: tptp
% 0.26/0.54 % Proving...
% 18.90/4.37 % SZS status Started for theBenchmark.p
% 18.90/4.37 ERROR - "ProverProcess:heur/409474:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 4 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution false --res_forward_subs subset_subsumption --res_forward_subs_resolution true --res_lit_sel pos_max --res_lit_sel_side num_var --res_ordering kbo_pred --res_passive_queue_type priority_queues --res_passive_queues "[[-num_lits];[-conj_symb;-num_symb;+num_symb]]" --res_passive_queues_freq "[15;3]" --res_prop_simpl_given false --res_prop_simpl_new true --res_sim_input true --res_time_limit 202.80 --res_to_prop_solver passive --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/x2bmqs6h 2>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/x2bmqs6h_error
% 18.90/4.37 ERROR - "ProverProcess:heur/469571:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 6 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3.0 --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 32 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp false --inst_learning_factor 10 --inst_learning_loop_flag true --inst_learning_start 256 --inst_lit_activity_flag true --inst_lit_sel "[+sign;-ground;-non_prol_conj_symb;-num_var]" --inst_lit_sel_side num_lit --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-ground;-epr]]" --inst_passive_queues_freq "[2]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 0.6939020527068606 --inst_solver_per_active 8 --inst_sos_flag false --inst_start_prop_sim_after_learn 9 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 128 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[DemodLightNormLoopTriv;ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 640 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/0xqmkyk4 2>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/0xqmkyk4_error
% 18.90/4.37 ERROR - "ProverProcess:heur/381325:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 1 --comb_sup_mult 3 --conj_cone_tolerance 3. --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[Demod;DemodLoopTriv;LightNorm;ACNormalisation]" --sup_full_triv "[]" --sup_fun_splitting true --sup_immed_bw_immed "[]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes]" --sup_immed_fw_immed "[Subsumption;UnitSubsAndRes;Demod;DemodLoopTriv;LightNorm;DemodLightNormLoopTriv]" --sup_immed_fw_main "[Subsumption;SubsumptionRes;LightNorm;DemodLightNormLoopTriv]" --sup_immed_triv "[PropSubs]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;FwDemod]" --sup_input_bw "[UnitSubsAndRes]" --sup_input_fw "[]" --sup_input_triv "[PropSubs]" --sup_iter_deepening 0 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_symb;-max_atom_input_occur];[+horn];[+bc_imp_inh;+ground;-conj_dist]]" --sup_passive_queues_freq "[3;1;25]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 8 --sup_score sim_d_gen --sup_share_max_num_cl 40 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver active --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/e55w836s 2>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/e55w836s_error
% 18.90/4.37 ERROR - "ProverProcess:heur/346297:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_sup_deep_mult 6 --comb_sup_mult 32 --conj_cone_tolerance 2.7380125131254 --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red false --extra_neg_conj none --inst_activity_threshold 16 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 6 --inst_learning_loop_flag true --inst_learning_start 1024 --inst_lit_activity_flag true --inst_lit_sel "[+depth;+sign;+num_symb;-split;-eq]" --inst_lit_sel_side cnt --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-num_lits];[-max_atom_input_occur;-ground]]" --inst_passive_queues_freq "[8;50]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.21724605765256222 --inst_solver_per_active 256 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[-depth;+non_prol_conj_symb;-split;-ground;+num_var]" --inst_start_prop_sim_after_learn 8 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl true --prep_def_merge_tr_cl true --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim false --prep_sem_filter none --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten false --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 32 --pure_diseq_elim false --resolution_flag false --schedule none --share_sel_clauses false --smt_ac_axioms full --smt_preprocessing true --splitting_cvd true --splitting_cvd_svl false --splitting_grd true --splitting_mode full --splitting_nvd 128 --stats_out none --sub_typing true --subs_bck_mult 0 --sup_full_bw "[Demod]" --sup_full_fw "[Subsumption;SubsumptionRes;UnitSubsAndRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_full_triv "[PropSubs;Unflattening]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes;Demod;ACJoinability]" --sup_immed_fw_main "[SubsumptionRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_immed_triv "[]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;Subsumption;FwDemod;BwDemod;LightNorm]" --sup_input_bw "[]" --sup_input_fw "[]" --sup_input_triv "[PropSubs;Unflattening]" --sup_iter_deepening 4 --sup_passive_queue_type queue --sup_passive_queues "[[+num_symb]]" --sup_passive_queues_freq "[5]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.4432297345384799 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/ax204zpo 2>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/ax204zpo_error
% 18.90/4.37 ERROR - "ProverProcess:heur/397442:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 64 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 4 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 8 --inst_learning_loop_flag true --inst_learning_start 2 --inst_lit_activity_flag false --inst_lit_sel "[-split]" --inst_lit_sel_side num_lit --inst_orphan_elimination false --inst_passive_queue_type priority_queues --inst_passive_queues "[[+conj_symb]]" --inst_passive_queues_freq "[50]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.8199321230744955 --inst_solver_per_active 4 --inst_sos_flag false --inst_start_prop_sim_after_learn 7 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/90m2fg9o 2>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/90m2fg9o_error
% 18.90/4.37 ERROR - "ProverProcess:heur/421498:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 18.90/4.37 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 8 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 512 --inst_dismatching true --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 8 --inst_learning_loop_flag true --inst_learning_start 128 --inst_lit_activity_flag false --inst_lit_sel "[+sign;+prop]" --inst_lit_sel_side none --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[+num_symb;-age;-age];[+num_symb;+conj_non_prolific_symb]]" --inst_passive_queues_freq "[512;10]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew model --inst_solver_calls_frac 0.006221608720445637 --inst_solver_per_active 32768 --inst_sos_flag true --inst_sos_phase false --inst_sos_sth_lit_sel "[+non_prol_conj_symb;+sign;-depth;-prop]" --inst_start_prop_sim_after_learn 9 --inst_subs_given true --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/dvjy4e8t 2>> /export/starexec/sandbox2/tmp/iprover_out_bpqi66q2/dvjy4e8t_error
% 18.90/4.37 % SZS status Theorem for theBenchmark.p
% 18.90/4.37
% 18.90/4.37 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 18.90/4.37
% 18.90/4.37 % ------ iProver source info
% 18.90/4.37
% 18.90/4.37 % git: date: 2026-07-19 20:42:38 +0200
% 18.90/4.37 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 18.90/4.37 % git: non_committed_changes: false
% 18.90/4.37
% 18.90/4.37 % ------ Parsing...
% 18.90/4.37 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 18.90/4.37 % ------ Proving...
% 18.90/4.37 % ------ Problem Properties
% 18.90/4.37
% 18.90/4.37 %
% 18.90/4.37 % clauses 2932
% 18.90/4.37 % conjectures 11
% 18.90/4.37 % EPR 682
% 18.90/4.37 % Horn 2055
% 18.90/4.37 % unary 604
% 18.90/4.37 % binary 709
% 18.90/4.37 % lits 9746
% 18.90/4.37 % lits eq 791
% 18.90/4.37 % fd_pure 0
% 18.90/4.37 % fd_pseudo 0
% 18.90/4.37 % fd_cond 53
% 18.90/4.37 % fd_pseudo_cond 166
% 18.90/4.37 % AC symbols 0
% 18.90/4.37
% 18.90/4.37 % ------ Input Options Time Limit: Unbounded
% 18.90/4.37
% 18.90/4.37
% 18.90/4.37 % ------
% 18.90/4.37 % Current options:
% 18.90/4.37 % ------
% 18.90/4.37
% 18.90/4.37
% 18.90/4.37 %
% 18.90/4.37
% 18.90/4.37 % ------ Proving...
% 18.90/4.37 %
% 18.90/4.37
% 18.90/4.37 % SZS status Theorem for theBenchmark.p
% 18.90/4.37
% 18.90/4.37 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.90/4.37
% 18.90/4.37
%------------------------------------------------------------------------------