%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU395+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:42 PM UTC 2026
% Result : Theorem 9.64s 2.25s
% Output : Refutation 10.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 29
% Syntax : Number of formulae : 275 ( 56 unt; 16 def)
% Number of atoms : 1459 ( 56 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 2078 ( 894 ~;1030 |; 121 &)
% ( 13 <=>; 18 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 9 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 11 con; 0-3 aty)
% Number of variables : 217 ( 0 sgn 205 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f167,axiom,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_yellow_1) ).
fof(f268,axiom,
! [X0] :
( one_sorted_str(X0)
=> element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f286,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty(X1)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& net_str(net_of_bool_filter(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yellow19) ).
fof(f326,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f408,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(cast_as_carrier_subset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_pre_topc) ).
fof(f451,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty(X1)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_yellow19) ).
fof(f458,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty(X1)
& element(X1,powerset(the_carrier(X0)))
& ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& directed_relstr(net_of_bool_filter(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_yellow19) ).
fof(f591,axiom,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f698,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_yellow19) ).
fof(f711,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_yellow19) ).
fof(f730,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<=> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_yellow19) ).
fof(f731,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( ( ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<=> is_a_convergence_point_of_set(X0,X1,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f730]) ).
fof(f849,axiom,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_waybel_7) ).
fof(f1359,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f268]) ).
fof(f1373,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(ennf_transformation,[],[f286]) ).
fof(f1374,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(flattening,[],[f1373]) ).
fof(f1426,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f326]) ).
fof(f1509,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f408]) ).
fof(f1510,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1509]) ).
fof(f1570,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(ennf_transformation,[],[f451]) ).
fof(f1571,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(flattening,[],[f1570]) ).
fof(f1584,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& directed_relstr(net_of_bool_filter(X0,X1,X2)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(ennf_transformation,[],[f458]) ).
fof(f1585,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
& reflexive_relstr(net_of_bool_filter(X0,X1,X2))
& transitive_relstr(net_of_bool_filter(X0,X1,X2))
& strict_net_str(net_of_bool_filter(X0,X1,X2),X0)
& directed_relstr(net_of_bool_filter(X0,X1,X2)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(flattening,[],[f1584]) ).
fof(f1851,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f689]) ).
fof(f1865,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f698]) ).
fof(f1866,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,lim_points_of_net(X0,X1))
<=> is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f1865]) ).
fof(f1884,plain,
! [X0] :
( ! [X1] :
( X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f711]) ).
fof(f1885,plain,
! [X0] :
( ! [X1] :
( X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1884]) ).
fof(f1911,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<~> is_a_convergence_point_of_set(X0,X1,X2) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(ennf_transformation,[],[f731]) ).
fof(f1912,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)))
<~> is_a_convergence_point_of_set(X0,X1,X2) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(flattening,[],[f1911]) ).
fof(f3054,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( in(X2,lim_points_of_net(X0,X1))
| ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2) )
& ( is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| ~ in(X2,lim_points_of_net(X0,X1)) ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f1866]) ).
fof(f3072,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ~ in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& ( is_a_convergence_point_of_set(X0,X1,X2)
| in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(nnf_transformation,[],[f1912]) ).
fof(f3073,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ is_a_convergence_point_of_set(X0,X1,X2)
| ~ in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& ( is_a_convergence_point_of_set(X0,X1,X2)
| in(X2,lim_points_of_net(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1))) )
& element(X2,the_carrier(X0)) )
& ~ empty(X1)
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0) ),
inference(flattening,[],[f3072]) ).
fof(f3074,plain,
( ( ~ 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)
| in(sK623,lim_points_of_net(sK621,net_of_bool_filter(sK621,cast_as_carrier_subset(sK621),sK622))) )
& element(sK623,the_carrier(sK621))
& ~ empty(sK622)
& filtered_subset(sK622,boole_POSet(cast_as_carrier_subset(sK621)))
& upper_relstr_subset(sK622,boole_POSet(cast_as_carrier_subset(sK621)))
& proper_element(sK622,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK621)))))
& element(sK622,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK621)))))
& ~ empty_carrier(sK621)
& topological_space(sK621)
& top_str(sK621) ),
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(f4109,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1359]) ).
fof(f4125,plain,
! [X2,X0,X1] :
( net_str(net_of_bool_filter(X0,X1,X2),X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f1374]) ).
fof(f4173,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1426]) ).
fof(f4388,plain,
! [X0] :
( ~ empty(cast_as_carrier_subset(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1510]) ).
fof(f4537,plain,
! [X2,X0,X1] :
( transitive_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f1571]) ).
fof(f4539,plain,
! [X2,X0,X1] :
( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f1571]) ).
fof(f4562,plain,
! [X2,X0,X1] :
( directed_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1)))) ),
inference(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] :
( is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| ~ in(X2,lim_points_of_net(X0,X1))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f3054]) ).
fof(f5774,plain,
! [X2,X0,X1] :
( ~ is_a_convergence_point_of_set(X0,filter_of_net_str(X0,X1),X2)
| in(X2,lim_points_of_net(X0,X1))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f3054]) ).
fof(f5790,plain,
! [X0,X1] :
( filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1
| empty(X1)
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(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,
( 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,[],[f3074]) ).
fof(f5837,plain,
( ~ 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,[],[f3074]) ).
fof(f6048,plain,
! [X0] : powerset(X0) = the_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f849]) ).
fof(f6401,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),k1_pcomps_1(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(definition_unfolding,[],[f4109,f5171]) ).
fof(f6410,plain,
! [X2,X0,X1] :
( net_str(net_of_bool_filter(X0,X1,X2),X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(definition_unfolding,[],[f4125,f5171,f3790,f3790,f5171,f3790]) ).
fof(f6561,plain,
! [X2,X0,X1] :
( ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(definition_unfolding,[],[f4539,f5171,f3790,f3790,f5171,f3790]) ).
fof(f6563,plain,
! [X2,X0,X1] :
( transitive_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(definition_unfolding,[],[f4537,f5171,f3790,f3790,f5171,f3790]) ).
fof(f6569,plain,
! [X2,X0,X1] :
( directed_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ proper_element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1)))))
| ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(definition_unfolding,[],[f4562,f5171,f3790,f3790,f5171,f3790,f5171,f3790]) ).
fof(f7005,plain,
! [X0,X1] :
( filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1
| empty(X1)
| ~ 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))))
| ~ proper_element(X1,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| ~ element(X1,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
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(f7093,plain,
! [X0] : k1_pcomps_1(X0) = the_carrier(poset_of_lattice(boole_lattice(X0))),
inference(definition_unfolding,[],[f6048,f5171,f3790]) ).
fof(f7443,definition,
sF655 = cast_as_carrier_subset(sK621),
introduced(definition,[new_symbols(definition,[sF655])],[function_definition]) ).
fof(f7444,plain,
cast_as_carrier_subset(sK621) = sF655,
inference(reorient_equations,[],[f7443]) ).
fof(f7445,definition,
sF656 = net_of_bool_filter(sK621,sF655,sK622),
introduced(definition,[new_symbols(definition,[sF656])],[function_definition]) ).
fof(f7446,plain,
net_of_bool_filter(sK621,sF655,sK622) = sF656,
inference(reorient_equations,[],[f7445]) ).
fof(f7447,definition,
sF657 = lim_points_of_net(sK621,sF656),
introduced(definition,[new_symbols(definition,[sF657])],[function_definition]) ).
fof(f7448,plain,
lim_points_of_net(sK621,sF656) = sF657,
inference(reorient_equations,[],[f7447]) ).
fof(f7449,plain,
( ~ is_a_convergence_point_of_set(sK621,sK622,sK623)
| ~ in(sK623,sF657) ),
inference(definition_folding,[],[f5837,f7448,f7446,f7444]) ).
fof(f7450,plain,
( is_a_convergence_point_of_set(sK621,sK622,sK623)
| in(sK623,sF657) ),
inference(definition_folding,[],[f5836,f7448,f7446,f7444]) ).
fof(f7451,definition,
sF658 = the_carrier(sK621),
introduced(definition,[new_symbols(definition,[sF658])],[function_definition]) ).
fof(f7452,plain,
the_carrier(sK621) = sF658,
inference(reorient_equations,[],[f7451]) ).
fof(f7453,plain,
element(sK623,sF658),
inference(definition_folding,[],[f5835,f7452]) ).
fof(f7454,definition,
sF659 = boole_lattice(sF655),
introduced(definition,[new_symbols(definition,[sF659])],[function_definition]) ).
fof(f7455,plain,
boole_lattice(sF655) = sF659,
inference(reorient_equations,[],[f7454]) ).
fof(f7456,definition,
sF660 = poset_of_lattice(sF659),
introduced(definition,[new_symbols(definition,[sF660])],[function_definition]) ).
fof(f7457,plain,
poset_of_lattice(sF659) = sF660,
inference(reorient_equations,[],[f7456]) ).
fof(f7458,plain,
filtered_subset(sK622,sF660),
inference(definition_folding,[],[f7016,f7457,f7455,f7444]) ).
fof(f7459,plain,
upper_relstr_subset(sK622,sF660),
inference(definition_folding,[],[f7017,f7457,f7455,f7444]) ).
fof(f7460,definition,
sF661 = the_carrier(sF660),
introduced(definition,[new_symbols(definition,[sF661])],[function_definition]) ).
fof(f7461,plain,
the_carrier(sF660) = sF661,
inference(reorient_equations,[],[f7460]) ).
fof(f7462,definition,
sF662 = k1_pcomps_1(sF661),
introduced(definition,[new_symbols(definition,[sF662])],[function_definition]) ).
fof(f7463,plain,
k1_pcomps_1(sF661) = sF662,
inference(reorient_equations,[],[f7462]) ).
fof(f7464,plain,
proper_element(sK622,sF662),
inference(definition_folding,[],[f7018,f7463,f7461,f7457,f7455,f7444]) ).
fof(f7465,plain,
element(sK622,sF662),
inference(definition_folding,[],[f7019,f7463,f7461,f7457,f7455,f7444]) ).
fof(f7516,definition,
( spl663_5
<=> in(sK623,sF657) ),
introduced(definition,[new_symbols(definition,[spl663_5])],[avatar_definition]) ).
fof(f7517,plain,
( ~ in(sK623,sF657)
| spl663_5 ),
inference(avatar_component_clause,[],[f7516]) ).
fof(f7518,plain,
( in(sK623,sF657)
| ~ spl663_5 ),
inference(avatar_component_clause,[],[f7516]) ).
fof(f7520,definition,
( spl663_6
<=> is_a_convergence_point_of_set(sK621,sK622,sK623) ),
introduced(definition,[new_symbols(definition,[spl663_6])],[avatar_definition]) ).
fof(f7521,plain,
( ~ is_a_convergence_point_of_set(sK621,sK622,sK623)
| spl663_6 ),
inference(avatar_component_clause,[],[f7520]) ).
fof(f7522,plain,
( is_a_convergence_point_of_set(sK621,sK622,sK623)
| ~ spl663_6 ),
inference(avatar_component_clause,[],[f7520]) ).
fof(f7523,plain,
( spl663_5
| spl663_6 ),
inference(avatar_split_clause,[],[f7450,f7520,f7516]) ).
fof(f7524,plain,
( ~ spl663_5
| ~ spl663_6 ),
inference(avatar_split_clause,[],[f7449,f7520,f7516]) ).
fof(f7526,plain,
! [X0,X1] :
( ~ proper_element(X1,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1
| empty(X1)
| ~ 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))))
| ~ element(X1,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(cast_as_carrier_subset(X0))))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(forward_demodulation,[],[f7005,f7093]) ).
fof(f7811,plain,
! [X2,X0,X1] :
( ~ proper_element(X2,k1_pcomps_1(k1_pcomps_1(X1)))
| directed_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(the_carrier(poset_of_lattice(boole_lattice(X1))))) ),
inference(forward_demodulation,[],[f6569,f7093]) ).
fof(f7817,plain,
! [X2,X0,X1] :
( ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| transitive_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(k1_pcomps_1(X1))) ),
inference(forward_demodulation,[],[f6563,f7093]) ).
fof(f7819,plain,
! [X2,X0,X1] :
( ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ empty_carrier(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ element(X2,k1_pcomps_1(k1_pcomps_1(X1))) ),
inference(forward_demodulation,[],[f6561,f7093]) ).
fof(f7822,plain,
! [X2,X0,X1] :
( net_str(net_of_bool_filter(X0,X1,X2),X0)
| ~ element(X2,k1_pcomps_1(k1_pcomps_1(X1)))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1))) ),
inference(forward_demodulation,[],[f6410,f7093]) ).
fof(f7885,plain,
! [X0,X1] :
( ~ proper_element(X1,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| ~ element(X1,k1_pcomps_1(k1_pcomps_1(cast_as_carrier_subset(X0))))
| filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) = X1
| empty(X1)
| ~ 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))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(forward_demodulation,[],[f7526,f7093]) ).
fof(f7890,plain,
! [X2,X0,X1] :
( ~ proper_element(X2,k1_pcomps_1(k1_pcomps_1(X1)))
| ~ element(X2,k1_pcomps_1(k1_pcomps_1(X1)))
| directed_relstr(net_of_bool_filter(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty(X1)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| empty(X2)
| ~ filtered_subset(X2,poset_of_lattice(boole_lattice(X1)))
| ~ upper_relstr_subset(X2,poset_of_lattice(boole_lattice(X1))) ),
inference(forward_demodulation,[],[f7811,f7093]) ).
fof(f7946,plain,
( element(sF655,k1_pcomps_1(the_carrier(sK621)))
| ~ one_sorted_str(sK621) ),
inference(superposition,[],[f6401,f7444]) ).
fof(f7952,plain,
( element(sF655,k1_pcomps_1(sF658))
| ~ one_sorted_str(sK621) ),
inference(forward_demodulation,[],[f7946,f7452]) ).
fof(f7955,definition,
( spl663_69
<=> one_sorted_str(sK621) ),
introduced(definition,[new_symbols(definition,[spl663_69])],[avatar_definition]) ).
fof(f7956,plain,
( one_sorted_str(sK621)
| ~ spl663_69 ),
inference(avatar_component_clause,[],[f7955]) ).
fof(f7957,plain,
( ~ one_sorted_str(sK621)
| spl663_69 ),
inference(avatar_component_clause,[],[f7955]) ).
fof(f7959,definition,
( spl663_70
<=> element(sF655,k1_pcomps_1(sF658)) ),
introduced(definition,[new_symbols(definition,[spl663_70])],[avatar_definition]) ).
fof(f7961,plain,
( element(sF655,k1_pcomps_1(sF658))
| ~ spl663_70 ),
inference(avatar_component_clause,[],[f7959]) ).
fof(f7972,plain,
( ~ spl663_69
| spl663_70 ),
inference(avatar_split_clause,[],[f7952,f7959,f7955]) ).
fof(f7974,plain,
k1_pcomps_1(sF655) = the_carrier(poset_of_lattice(sF659)),
inference(superposition,[],[f7093,f7455]) ).
fof(f7977,plain,
the_carrier(sF660) = k1_pcomps_1(sF655),
inference(forward_demodulation,[],[f7974,f7457]) ).
fof(f7978,plain,
sF661 = k1_pcomps_1(sF655),
inference(forward_demodulation,[],[f7977,f7461]) ).
fof(f7990,plain,
one_sorted_str(sK621),
inference(resolution,[],[f4173,f5827]) ).
fof(f7991,plain,
( $false
| spl663_69 ),
inference(forward_subsumption_resolution,[],[f7990,f7957]) ).
fof(f7992,plain,
spl663_69,
inference(avatar_contradiction_clause,[],[f7991]) ).
fof(f7993,plain,
( ~ empty(sF655)
| empty_carrier(sK621)
| ~ one_sorted_str(sK621) ),
inference(superposition,[],[f4388,f7444]) ).
fof(f7994,plain,
( ~ empty(sF655)
| ~ one_sorted_str(sK621) ),
inference(forward_subsumption_resolution,[],[f7993,f5829]) ).
fof(f7995,plain,
( ~ empty(sF655)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f7994,f7956]) ).
fof(f7996,plain,
( cast_as_carrier_subset(sK621) = the_carrier(sK621)
| ~ spl663_69 ),
inference(resolution,[],[f5755,f7956]) ).
fof(f7997,plain,
( cast_as_carrier_subset(sK621) = sF658
| ~ spl663_69 ),
inference(forward_demodulation,[],[f7996,f7452]) ).
fof(f7998,plain,
( sF655 = sF658
| ~ spl663_69 ),
inference(forward_demodulation,[],[f7997,f7444]) ).
fof(f7999,plain,
( element(sK623,sF655)
| ~ spl663_69 ),
inference(superposition,[],[f7453,f7998]) ).
fof(f8000,plain,
! [X0] :
( ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621) ),
inference(superposition,[],[f7885,f7444]) ).
fof(f8001,plain,
! [X0] :
( ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ one_sorted_str(sK621) ),
inference(forward_subsumption_resolution,[],[f8000,f5829]) ).
fof(f8002,plain,
( ! [X0] :
( ~ proper_element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8001,f7956]) ).
fof(f8003,plain,
( ! [X0] :
( ~ proper_element(X0,k1_pcomps_1(sF661))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8002,f7978]) ).
fof(f8004,plain,
( ! [X0] :
( ~ proper_element(X0,sF662)
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655)))
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8003,f7463]) ).
fof(f8005,plain,
( ! [X0] :
( ~ element(X0,k1_pcomps_1(sF661))
| ~ proper_element(X0,sF662)
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8004,f7978]) ).
fof(f8006,plain,
( ! [X0] :
( ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8005,f7463]) ).
fof(f8007,plain,
( ! [X0] :
( ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8006,f7455]) ).
fof(f8008,plain,
( ! [X0] :
( ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8007,f7457]) ).
fof(f8009,plain,
( ! [X0] :
( ~ upper_relstr_subset(X0,poset_of_lattice(sF659))
| ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8008,f7455]) ).
fof(f8010,plain,
( ! [X0] :
( ~ proper_element(X0,sF662)
| ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ upper_relstr_subset(X0,sF660)
| filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,X0)) = X0
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8009,f7457]) ).
fof(f8011,plain,
( ~ filtered_subset(sK622,sF660)
| ~ element(sK622,sF662)
| ~ upper_relstr_subset(sK622,sF660)
| sK622 = filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,sK622))
| empty(sK622)
| ~ spl663_69 ),
inference(resolution,[],[f8010,f7464]) ).
fof(f8012,plain,
( ~ element(sK622,sF662)
| ~ upper_relstr_subset(sK622,sF660)
| sK622 = filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,sK622))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8011,f7458]) ).
fof(f8013,plain,
( ~ upper_relstr_subset(sK622,sF660)
| sK622 = filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,sK622))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8012,f7465]) ).
fof(f8014,plain,
( sK622 = filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,sK622))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8013,f7459]) ).
fof(f8015,plain,
( sK622 = filter_of_net_str(sK621,net_of_bool_filter(sK621,sF655,sK622))
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8014,f5834]) ).
fof(f8016,plain,
( sK622 = filter_of_net_str(sK621,sF656)
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8015,f7446]) ).
fof(f8100,plain,
! [X0,X1] :
( ~ upper_relstr_subset(X0,poset_of_lattice(sF659))
| ~ empty_carrier(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) ),
inference(superposition,[],[f7819,f7455]) ).
fof(f8101,plain,
( ! [X0,X1] :
( ~ upper_relstr_subset(X0,poset_of_lattice(sF659))
| ~ empty_carrier(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) )
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8100,f7995]) ).
fof(f8102,plain,
( ! [X0,X1] :
( ~ upper_relstr_subset(X0,sF660)
| ~ empty_carrier(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8101,f7457]) ).
fof(f8103,plain,
( ! [X0,X1] :
( ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| ~ empty_carrier(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8102,f7457]) ).
fof(f8104,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(sF661))
| ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| ~ empty_carrier(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8103,f7978]) ).
fof(f8105,plain,
( ! [X0,X1] :
( ~ empty_carrier(net_of_bool_filter(X1,sF655,X0))
| ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| ~ element(X0,sF662)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8104,f7463]) ).
fof(f8106,plain,
( ~ empty_carrier(sF656)
| ~ filtered_subset(sK622,sF660)
| ~ upper_relstr_subset(sK622,sF660)
| ~ element(sK622,sF662)
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ spl663_69 ),
inference(superposition,[],[f8105,f7446]) ).
fof(f8107,plain,
( ~ empty_carrier(sF656)
| ~ upper_relstr_subset(sK622,sF660)
| ~ element(sK622,sF662)
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8106,f7458]) ).
fof(f8108,plain,
( ~ empty_carrier(sF656)
| ~ element(sK622,sF662)
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8107,f7459]) ).
fof(f8109,plain,
( ~ empty_carrier(sF656)
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8108,f7465]) ).
fof(f8110,plain,
( ~ empty_carrier(sF656)
| ~ one_sorted_str(sK621)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8109,f5829]) ).
fof(f8111,plain,
( ~ empty_carrier(sF656)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8110,f7956]) ).
fof(f8112,plain,
( ~ empty_carrier(sF656)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8111,f5834]) ).
fof(f8113,plain,
( ~ element(sF655,k1_pcomps_1(sF658))
| ~ empty_carrier(sF656)
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8112,f7452]) ).
fof(f8114,plain,
( ~ empty_carrier(sF656)
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8113,f7961]) ).
fof(f8116,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| empty_carrier(sF656)
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69 ),
inference(superposition,[],[f5773,f8016]) ).
fof(f8118,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8116,f8114]) ).
fof(f8120,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8118,f5829]) ).
fof(f8122,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8120,f5828]) ).
fof(f8124,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8122,f5827]) ).
fof(f8125,plain,
( ! [X0] :
( ~ in(X0,sF657)
| is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ element(X0,the_carrier(sK621))
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_demodulation,[],[f8124,f7448]) ).
fof(f8126,plain,
( ! [X0] :
( ~ element(X0,sF658)
| ~ in(X0,sF657)
| is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_demodulation,[],[f8125,f7452]) ).
fof(f8127,plain,
( ! [X0] :
( ~ element(X0,sF655)
| ~ in(X0,sF657)
| is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_demodulation,[],[f8126,f7998]) ).
fof(f8129,definition,
( spl663_80
<=> net_str(sF656,sK621) ),
introduced(definition,[new_symbols(definition,[spl663_80])],[avatar_definition]) ).
fof(f8130,plain,
( net_str(sF656,sK621)
| ~ spl663_80 ),
inference(avatar_component_clause,[],[f8129]) ).
fof(f8131,plain,
( ~ net_str(sF656,sK621)
| spl663_80 ),
inference(avatar_component_clause,[],[f8129]) ).
fof(f8133,definition,
( spl663_81
<=> directed_relstr(sF656) ),
introduced(definition,[new_symbols(definition,[spl663_81])],[avatar_definition]) ).
fof(f8134,plain,
( directed_relstr(sF656)
| ~ spl663_81 ),
inference(avatar_component_clause,[],[f8133]) ).
fof(f8135,plain,
( ~ directed_relstr(sF656)
| spl663_81 ),
inference(avatar_component_clause,[],[f8133]) ).
fof(f8137,definition,
( spl663_82
<=> transitive_relstr(sF656) ),
introduced(definition,[new_symbols(definition,[spl663_82])],[avatar_definition]) ).
fof(f8138,plain,
( transitive_relstr(sF656)
| ~ spl663_82 ),
inference(avatar_component_clause,[],[f8137]) ).
fof(f8139,plain,
( ~ transitive_relstr(sF656)
| spl663_82 ),
inference(avatar_component_clause,[],[f8137]) ).
fof(f8141,definition,
( spl663_83
<=> ! [X0] :
( ~ element(X0,sF655)
| is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ in(X0,sF657) ) ),
introduced(definition,[new_symbols(definition,[spl663_83])],[avatar_definition]) ).
fof(f8142,plain,
( ! [X0] :
( is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ element(X0,sF655)
| ~ in(X0,sF657) )
| ~ spl663_83 ),
inference(avatar_component_clause,[],[f8141]) ).
fof(f8143,plain,
( ~ spl663_80
| ~ spl663_81
| ~ spl663_82
| spl663_83
| ~ spl663_69
| ~ spl663_70 ),
inference(avatar_split_clause,[],[f8127,f7959,f7955,f8141,f8137,f8133,f8129]) ).
fof(f8269,plain,
! [X0,X1] :
( ~ upper_relstr_subset(X0,poset_of_lattice(sF659))
| transitive_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) ),
inference(superposition,[],[f7817,f7455]) ).
fof(f8270,plain,
( ! [X0,X1] :
( ~ upper_relstr_subset(X0,poset_of_lattice(sF659))
| transitive_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) )
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8269,f7995]) ).
fof(f8272,plain,
( ! [X0,X1] :
( ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8270,f7457]) ).
fof(f8274,plain,
( ! [X0,X1] :
( ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ element(X0,k1_pcomps_1(k1_pcomps_1(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8272,f7457]) ).
fof(f8276,plain,
( ! [X0,X1] :
( ~ element(X0,k1_pcomps_1(sF661))
| ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8274,f7978]) ).
fof(f8277,plain,
( ! [X0,X1] :
( ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(X0,sF662)
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8276,f7463]) ).
fof(f8280,plain,
( ! [X0] :
( ~ element(sF655,k1_pcomps_1(sF658))
| ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(sK621,sF655,X0))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ element(X0,sF662)
| empty(X0) )
| ~ spl663_69 ),
inference(superposition,[],[f8277,f7452]) ).
fof(f8283,plain,
( ! [X0] :
( ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(sK621,sF655,X0))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ element(X0,sF662)
| empty(X0) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8280,f7961]) ).
fof(f8286,plain,
( ! [X0] :
( ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| transitive_relstr(net_of_bool_filter(sK621,sF655,X0))
| ~ one_sorted_str(sK621)
| ~ element(X0,sF662)
| empty(X0) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8283,f5829]) ).
fof(f8287,plain,
( ! [X0] :
( transitive_relstr(net_of_bool_filter(sK621,sF655,X0))
| ~ upper_relstr_subset(X0,sF660)
| ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| empty(X0) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8286,f7956]) ).
fof(f8417,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| empty_carrier(sF656)
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69 ),
inference(superposition,[],[f5774,f8016]) ).
fof(f8765,plain,
( net_str(sF656,sK621)
| ~ element(sK622,k1_pcomps_1(k1_pcomps_1(sF655)))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655))) ),
inference(superposition,[],[f7822,f7446]) ).
fof(f8766,plain,
( ~ element(sK622,k1_pcomps_1(k1_pcomps_1(sF655)))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8765,f8131]) ).
fof(f8767,plain,
( ~ element(sK622,k1_pcomps_1(k1_pcomps_1(sF655)))
| ~ one_sorted_str(sK621)
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8766,f5829]) ).
fof(f8768,plain,
( ~ element(sK622,k1_pcomps_1(k1_pcomps_1(sF655)))
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8767,f7956]) ).
fof(f8769,plain,
( ~ element(sK622,k1_pcomps_1(k1_pcomps_1(sF655)))
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| empty(sK622)
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8768,f7995]) ).
fof(f8770,plain,
( ~ element(sK622,k1_pcomps_1(k1_pcomps_1(sF655)))
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8769,f5834]) ).
fof(f8771,plain,
( ~ element(sK622,k1_pcomps_1(sF661))
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_demodulation,[],[f8770,f7978]) ).
fof(f8772,plain,
( ~ element(sK622,sF662)
| ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_demodulation,[],[f8771,f7463]) ).
fof(f8773,plain,
( ~ element(sF655,k1_pcomps_1(the_carrier(sK621)))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8772,f7465]) ).
fof(f8774,plain,
( ~ element(sF655,k1_pcomps_1(sF658))
| ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| spl663_80 ),
inference(forward_demodulation,[],[f8773,f7452]) ).
fof(f8775,plain,
( ~ filtered_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8774,f7961]) ).
fof(f8776,plain,
( ~ filtered_subset(sK622,poset_of_lattice(sF659))
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_demodulation,[],[f8775,f7455]) ).
fof(f8777,plain,
( ~ filtered_subset(sK622,sF660)
| ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_demodulation,[],[f8776,f7457]) ).
fof(f8778,plain,
( ~ upper_relstr_subset(sK622,poset_of_lattice(boole_lattice(sF655)))
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8777,f7458]) ).
fof(f8779,plain,
( ~ upper_relstr_subset(sK622,poset_of_lattice(sF659))
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_demodulation,[],[f8778,f7455]) ).
fof(f8780,plain,
( ~ upper_relstr_subset(sK622,sF660)
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_demodulation,[],[f8779,f7457]) ).
fof(f8781,plain,
( $false
| ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(forward_subsumption_resolution,[],[f8780,f7459]) ).
fof(f8782,plain,
( ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(avatar_contradiction_clause,[],[f8781]) ).
fof(f8803,plain,
! [X0,X1] :
( ~ proper_element(X0,k1_pcomps_1(sF661))
| ~ element(X0,k1_pcomps_1(sF661))
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| empty(sF655)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) ),
inference(superposition,[],[f7890,f7978]) ).
fof(f8804,plain,
( ! [X0,X1] :
( ~ proper_element(X0,k1_pcomps_1(sF661))
| ~ element(X0,k1_pcomps_1(sF661))
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_subsumption_resolution,[],[f8803,f7995]) ).
fof(f8814,plain,
( ! [X0,X1] :
( ~ proper_element(X0,sF662)
| ~ element(X0,k1_pcomps_1(sF661))
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8804,f7463]) ).
fof(f8816,plain,
( ! [X0,X1] :
( ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ filtered_subset(X0,poset_of_lattice(boole_lattice(sF655)))
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8814,f7463]) ).
fof(f8818,plain,
( ! [X0,X1] :
( ~ filtered_subset(X0,poset_of_lattice(sF659))
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8816,f7455]) ).
fof(f8820,plain,
( ! [X0,X1] :
( ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0)
| ~ upper_relstr_subset(X0,poset_of_lattice(boole_lattice(sF655))) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8818,f7457]) ).
fof(f8821,plain,
( ! [X0,X1] :
( ~ upper_relstr_subset(X0,poset_of_lattice(sF659))
| ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8820,f7455]) ).
fof(f8822,plain,
( ! [X0,X1] :
( ~ element(sF655,k1_pcomps_1(the_carrier(X1)))
| ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(X1,sF655,X0))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X0,sF660)
| empty(X0) )
| ~ spl663_69 ),
inference(forward_demodulation,[],[f8821,f7457]) ).
fof(f8825,plain,
( ! [X0] :
( ~ element(sF655,k1_pcomps_1(sF658))
| ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(sK621,sF655,X0))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(X0,sF660)
| empty(X0) )
| ~ spl663_69 ),
inference(superposition,[],[f8822,f7452]) ).
fof(f8828,plain,
( ! [X0] :
( ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(sK621,sF655,X0))
| empty_carrier(sK621)
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(X0,sF660)
| empty(X0) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8825,f7961]) ).
fof(f8831,plain,
( ! [X0] :
( ~ filtered_subset(X0,sF660)
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| directed_relstr(net_of_bool_filter(sK621,sF655,X0))
| ~ one_sorted_str(sK621)
| ~ upper_relstr_subset(X0,sF660)
| empty(X0) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8828,f5829]) ).
fof(f8832,plain,
( ! [X0] :
( directed_relstr(net_of_bool_filter(sK621,sF655,X0))
| ~ element(X0,sF662)
| ~ proper_element(X0,sF662)
| ~ filtered_subset(X0,sF660)
| ~ upper_relstr_subset(X0,sF660)
| empty(X0) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8831,f7956]) ).
fof(f8889,plain,
( directed_relstr(sF656)
| ~ element(sK622,sF662)
| ~ proper_element(sK622,sF662)
| ~ filtered_subset(sK622,sF660)
| ~ upper_relstr_subset(sK622,sF660)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70 ),
inference(superposition,[],[f8832,f7446]) ).
fof(f8890,plain,
( ~ element(sK622,sF662)
| ~ proper_element(sK622,sF662)
| ~ filtered_subset(sK622,sF660)
| ~ upper_relstr_subset(sK622,sF660)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(forward_subsumption_resolution,[],[f8889,f8135]) ).
fof(f8891,plain,
( ~ proper_element(sK622,sF662)
| ~ filtered_subset(sK622,sF660)
| ~ upper_relstr_subset(sK622,sF660)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(forward_subsumption_resolution,[],[f8890,f7465]) ).
fof(f8892,plain,
( ~ filtered_subset(sK622,sF660)
| ~ upper_relstr_subset(sK622,sF660)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(forward_subsumption_resolution,[],[f8891,f7464]) ).
fof(f8893,plain,
( ~ upper_relstr_subset(sK622,sF660)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(forward_subsumption_resolution,[],[f8892,f7458]) ).
fof(f8894,plain,
( empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(forward_subsumption_resolution,[],[f8893,f7459]) ).
fof(f8895,plain,
( $false
| ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(forward_subsumption_resolution,[],[f8894,f5834]) ).
fof(f8896,plain,
( ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(avatar_contradiction_clause,[],[f8895]) ).
fof(f9189,plain,
( transitive_relstr(sF656)
| ~ upper_relstr_subset(sK622,sF660)
| ~ filtered_subset(sK622,sF660)
| ~ element(sK622,sF662)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70 ),
inference(superposition,[],[f8287,f7446]) ).
fof(f9190,plain,
( ~ upper_relstr_subset(sK622,sF660)
| ~ filtered_subset(sK622,sF660)
| ~ element(sK622,sF662)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(forward_subsumption_resolution,[],[f9189,f8139]) ).
fof(f9191,plain,
( ~ filtered_subset(sK622,sF660)
| ~ element(sK622,sF662)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(forward_subsumption_resolution,[],[f9190,f7459]) ).
fof(f9192,plain,
( ~ element(sK622,sF662)
| empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(forward_subsumption_resolution,[],[f9191,f7458]) ).
fof(f9193,plain,
( empty(sK622)
| ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(forward_subsumption_resolution,[],[f9192,f7465]) ).
fof(f9194,plain,
( $false
| ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(forward_subsumption_resolution,[],[f9193,f5834]) ).
fof(f9195,plain,
( ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(avatar_contradiction_clause,[],[f9194]) ).
fof(f9197,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ transitive_relstr(sF656)
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70 ),
inference(forward_subsumption_resolution,[],[f8417,f8114]) ).
fof(f9200,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ directed_relstr(sF656)
| ~ net_str(sF656,sK621)
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9197,f8138]) ).
fof(f9203,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ net_str(sF656,sK621)
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9200,f8134]) ).
fof(f9206,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| empty_carrier(sK621)
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9203,f8130]) ).
fof(f9209,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ topological_space(sK621)
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9206,f5829]) ).
fof(f9212,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621))
| ~ top_str(sK621) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9209,f5828]) ).
fof(f9215,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,lim_points_of_net(sK621,sF656))
| ~ element(X0,the_carrier(sK621)) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9212,f5827]) ).
fof(f9218,plain,
( ! [X0] :
( in(X0,sF657)
| ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| ~ element(X0,the_carrier(sK621)) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_demodulation,[],[f9215,f7448]) ).
fof(f9220,plain,
( ! [X0] :
( ~ element(X0,sF658)
| in(X0,sF657)
| ~ is_a_convergence_point_of_set(sK621,sK622,X0) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_demodulation,[],[f9218,f7452]) ).
fof(f9222,plain,
( ! [X0] :
( ~ is_a_convergence_point_of_set(sK621,sK622,X0)
| in(X0,sF657)
| ~ element(X0,sF655) )
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_demodulation,[],[f9220,f7998]) ).
fof(f9223,plain,
( ~ element(sK623,sF655)
| ~ in(sK623,sF657)
| spl663_6
| ~ spl663_83 ),
inference(resolution,[],[f8142,f7521]) ).
fof(f9228,plain,
( ~ in(sK623,sF657)
| spl663_6
| ~ spl663_69
| ~ spl663_83 ),
inference(forward_subsumption_resolution,[],[f9223,f7999]) ).
fof(f9231,plain,
( $false
| ~ spl663_5
| spl663_6
| ~ spl663_69
| ~ spl663_83 ),
inference(forward_subsumption_resolution,[],[f9228,f7518]) ).
fof(f9232,plain,
( ~ spl663_5
| spl663_6
| ~ spl663_69
| ~ spl663_83 ),
inference(avatar_contradiction_clause,[],[f9231]) ).
fof(f9248,plain,
( in(sK623,sF657)
| ~ element(sK623,sF655)
| ~ spl663_6
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(resolution,[],[f7522,f9222]) ).
fof(f9253,plain,
( ~ element(sK623,sF655)
| spl663_5
| ~ spl663_6
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9248,f7517]) ).
fof(f9256,plain,
( $false
| spl663_5
| ~ spl663_6
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(forward_subsumption_resolution,[],[f9253,f7999]) ).
fof(f9257,plain,
( spl663_5
| ~ spl663_6
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(avatar_contradiction_clause,[],[f9256]) ).
cnf(s3,plain,
( spl663_5
| spl663_6 ),
inference(sat_conversion,[],[f7523]) ).
cnf(s4,plain,
( ~ spl663_5
| ~ spl663_6 ),
inference(sat_conversion,[],[f7524]) ).
cnf(s56,plain,
( ~ spl663_69
| spl663_70 ),
inference(sat_conversion,[],[f7972]) ).
cnf(s58,plain,
spl663_69,
inference(sat_conversion,[],[f7992]) ).
cnf(s61,plain,
( ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82
| spl663_83 ),
inference(sat_conversion,[],[f8143]) ).
cnf(s79,plain,
( ~ spl663_69
| ~ spl663_70
| spl663_80 ),
inference(sat_conversion,[],[f8782]) ).
cnf(s83,plain,
( ~ spl663_69
| ~ spl663_70
| spl663_81 ),
inference(sat_conversion,[],[f8896]) ).
cnf(s88,plain,
( ~ spl663_69
| ~ spl663_70
| spl663_82 ),
inference(sat_conversion,[],[f9195]) ).
cnf(s89,plain,
( ~ spl663_5
| spl663_6
| ~ spl663_69
| ~ spl663_83 ),
inference(sat_conversion,[],[f9232]) ).
cnf(s92,plain,
( spl663_5
| ~ spl663_6
| ~ spl663_69
| ~ spl663_70
| ~ spl663_80
| ~ spl663_81
| ~ spl663_82 ),
inference(sat_conversion,[],[f9257]) ).
cnf(s94,plain,
spl663_70,
inference(rat,[],[s56,s58]) ).
cnf(s95,plain,
spl663_82,
inference(rat,[],[s88,s58,s94]) ).
cnf(s96,plain,
spl663_81,
inference(rat,[],[s83,s58,s94]) ).
cnf(s97,plain,
spl663_80,
inference(rat,[],[s79,s58,s94]) ).
cnf(s98,plain,
spl663_83,
inference(rat,[],[s61,s94,s95,s96,s58,s97]) ).
cnf(s100,plain,
spl663_5,
inference(rat,[],[s3,s92,s58,s94,s97,s96,s95]) ).
cnf(s101,plain,
spl663_6,
inference(rat,[],[s89,s98,s58,s100]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s4,s101,s100]) ).
fof(f9259,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU395+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.35 % Computer : n020.cluster.edu
% 0.04/0.35 % Model : x86_64 x86_64
% 0.04/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.35 % Memory : 8046.5625MB
% 0.04/0.35 % OS : Linux 6.8.0-71-generic
% 0.04/0.36 % CPULimit : 300
% 0.04/0.36 % WCLimit : 300
% 0.04/0.36 % DateTime : Mon Sep 28 05:06:34 UTC 2026
% 0.04/0.36 % CPUTime :
% 0.04/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.40 Running first-order theorem proving
% 0.04/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.64/2.25 % (4035608)Detected formulas, will run a generic FOF schedule.
% 9.64/2.25 % (4035616)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2507987302:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.64/2.25 % (4035614)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4164270232:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.64/2.25 % (4035615)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=415176498:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.64/2.25 % (4035619)dis-21_1_sil=8000:lcm=predicate:random_seed=3526216709:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.64/2.25 % (4035617)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3490680533:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.64/2.25 % (4035613)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1460281593:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.64/2.25 % (4035616)Instruction limit reached!
% 9.64/2.25 % (4035616)------------------------------
% 9.64/2.25 % (4035616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035616)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035616)Termination reason: Instruction limit
% 9.64/2.25 % (4035616)Termination phase: Blocked clause elimination
% 9.64/2.25 % (4035616)Time elapsed: 0.036 s
% 9.64/2.25 % (4035616)Peak memory usage: 90 MB
% 9.64/2.25 % (4035616)Instructions burned: 111 (million)
% 9.64/2.25 % (4035618)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3869120019:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.64/2.25 % (4035619)Instruction limit reached!
% 9.64/2.25 % (4035619)------------------------------
% 9.64/2.25 % (4035619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035619)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035619)Termination reason: Instruction limit
% 9.64/2.25 % (4035619)Termination phase: Saturation
% 9.64/2.25 % (4035619)Time elapsed: 0.067 s
% 9.64/2.25 % (4035619)Peak memory usage: 92 MB
% 9.64/2.25 % (4035619)Instructions burned: 130 (million)
% 9.64/2.25 % (4035617)Instruction limit reached!
% 9.64/2.25 % (4035617)------------------------------
% 9.64/2.25 % (4035617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035617)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035617)Termination reason: Instruction limit
% 9.64/2.25 % (4035617)Termination phase: Saturation
% 9.64/2.25 % (4035617)Time elapsed: 0.071 s
% 9.64/2.25 % (4035617)Peak memory usage: 92 MB
% 9.64/2.25 % (4035617)Instructions burned: 120 (million)
% 9.64/2.25 % (4035618)Instruction limit reached!
% 9.64/2.25 % (4035618)------------------------------
% 9.64/2.25 % (4035618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035618)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035618)Termination reason: Instruction limit
% 9.64/2.25 % (4035618)Termination phase: Saturation
% 9.64/2.25 % (4035618)Time elapsed: 0.079 s
% 9.64/2.25 % (4035618)Peak memory usage: 92 MB
% 9.64/2.25 % (4035618)Instructions burned: 140 (million)
% 9.64/2.25 % (4035626)lrs+10_1_sil=8000:sp=occurrence:random_seed=1275359268:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.64/2.25 % (4035628)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2790307274:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.64/2.25 % (4035629)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3173983150:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.64/2.25 % (4035626)Instruction limit reached!
% 9.64/2.25 % (4035626)------------------------------
% 9.64/2.25 % (4035626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035626)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035626)Termination reason: Instruction limit
% 9.64/2.25 % (4035626)Termination phase: Saturation
% 9.64/2.25 % (4035626)Time elapsed: 0.095 s
% 9.64/2.25 % (4035626)Peak memory usage: 95 MB
% 9.64/2.25 % (4035626)Instructions burned: 285 (million)
% 9.64/2.25 % (4035630)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3593598593:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 9.64/2.25 % (4035628)Instruction limit reached!
% 9.64/2.25 % (4035628)------------------------------
% 9.64/2.25 % (4035628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035628)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035628)Termination reason: Instruction limit
% 9.64/2.25 % (4035628)Termination phase: Saturation
% 9.64/2.25 % (4035628)Time elapsed: 0.093 s
% 9.64/2.25 % (4035628)Peak memory usage: 91 MB
% 9.64/2.25 % (4035628)Instructions burned: 158 (million)
% 9.64/2.25 % (4035634)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1301429630:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.64/2.25 % (4035630)Instruction limit reached!
% 9.64/2.25 % (4035630)------------------------------
% 9.64/2.25 % (4035630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035630)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035630)Termination reason: Instruction limit
% 9.64/2.25 % (4035630)Termination phase: Saturation
% 9.64/2.25 % (4035630)Time elapsed: 0.151 s
% 9.64/2.25 % (4035630)Peak memory usage: 94 MB
% 9.64/2.25 % (4035630)Instructions burned: 249 (million)
% 9.64/2.25 % (4035629)Instruction limit reached!
% 9.64/2.25 % (4035629)------------------------------
% 9.64/2.25 % (4035629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035629)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035629)Termination reason: Instruction limit
% 9.64/2.25 % (4035629)Termination phase: Saturation
% 9.64/2.25 % (4035629)Time elapsed: 0.209 s
% 9.64/2.25 % (4035629)Peak memory usage: 96 MB
% 9.64/2.25 % (4035629)Instructions burned: 326 (million)
% 9.64/2.25 % (4035634)Instruction limit reached!
% 9.64/2.25 % (4035634)------------------------------
% 9.64/2.25 % (4035634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035634)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035634)Termination reason: Instruction limit
% 9.64/2.25 % (4035634)Termination phase: Saturation
% 9.64/2.25 % (4035634)Time elapsed: 0.092 s
% 9.64/2.25 % (4035634)Peak memory usage: 94 MB
% 9.64/2.25 % (4035634)Instructions burned: 296 (million)
% 9.64/2.25 % (4035636)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2377568812:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.64/2.25 % (4035638)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2467916665:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 9.64/2.25 % (4035640)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3047151406:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 9.64/2.25 % (4035640)Instruction limit reached!
% 9.64/2.25 % (4035640)------------------------------
% 9.64/2.25 % (4035640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035640)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035640)Termination reason: Instruction limit
% 9.64/2.25 % (4035640)Termination phase: Saturation
% 9.64/2.25 % (4035640)Time elapsed: 0.031 s
% 9.64/2.25 % (4035640)Peak memory usage: 90 MB
% 9.64/2.25 % (4035640)Instructions burned: 115 (million)
% 9.64/2.25 % (4035638)Instruction limit reached!
% 9.64/2.25 % (4035638)------------------------------
% 9.64/2.25 % (4035638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035638)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035638)Termination reason: Instruction limit
% 9.64/2.25 % (4035638)Termination phase: Saturation
% 9.64/2.25 % (4035638)Time elapsed: 0.063 s
% 9.64/2.25 % (4035638)Peak memory usage: 92 MB
% 9.64/2.25 % (4035638)Instructions burned: 114 (million)
% 9.64/2.25 % (4035639)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1551595934:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 9.64/2.25 % (4035639)Instruction limit reached!
% 9.64/2.25 % (4035639)------------------------------
% 9.64/2.25 % (4035639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035639)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035639)Termination reason: Instruction limit
% 9.64/2.25 % (4035639)Termination phase: Blocked clause elimination
% 9.64/2.25 % (4035639)Time elapsed: 0.076 s
% 9.64/2.25 % (4035639)Peak memory usage: 91 MB
% 9.64/2.25 % (4035639)Instructions burned: 128 (million)
% 9.64/2.25 % (4035644)lrs+10_1_sil=8000:sp=occurrence:random_seed=69413656:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 9.64/2.25 % (4035646)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2236856779:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 9.64/2.25 % (4035647)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2868290191:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 9.64/2.25 % (4035646)Instruction limit reached!
% 9.64/2.25 % (4035646)------------------------------
% 9.64/2.25 % (4035646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.25 % (4035646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.25 % (4035646)CaDiCaL version: 2.1.3
% 9.64/2.25 % (4035646)Termination reason: Instruction limit
% 9.64/2.25 % (4035646)Termination phase: Saturation
% 9.64/2.25 % (4035646)Time elapsed: 0.261 s
% 9.64/2.25 % (4035646)Peak memory usage: 97 MB
% 9.64/2.25 % (4035646)Instructions burned: 437 (million)
% 9.64/2.25 % (4035613)First to succeed.
% 9.64/2.25 % (4035613)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4035608"
% 9.64/2.25 % (4035651)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=122262840:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 9.64/2.25 % (4035613)Refutation found. Thanks to Tanya!
% 9.64/2.25 % SZS status Theorem for theBenchmark
% 9.64/2.25 % SZS output start Proof for theBenchmark
% See solution above
% 10.30/2.45 % (4035613)------------------------------
% 10.30/2.45 % (4035613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.45 % (4035613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.45 % (4035613)CaDiCaL version: 2.1.3
% 10.30/2.45 % (4035613)Termination reason: Refutation
% 10.30/2.45 % (4035613)Time elapsed: 1.034 s
% 10.30/2.45 % (4035613)Peak memory usage: 166 MB
% 10.30/2.45 % (4035613)Instructions burned: 2243 (million)
% 10.30/2.45 % (4035613)------------------------------
% 10.30/2.45 % (4035613)------------------------------
% 10.30/2.45 % (4035608)Success in time 1.414 s
% 10.30/2.45 % Vampire exiting
%------------------------------------------------------------------------------