%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU399+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:20:25 PM UTC 2026
% Result : Theorem 0.16s 11.12s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 52
% Syntax : Number of formulae : 273 ( 17 unt; 43 def)
% Number of atoms : 1689 ( 196 equ)
% Maximal formula atoms : 28 ( 6 avg)
% Number of connectives : 2284 ( 868 ~;1127 |; 220 &)
% ( 48 <=>; 20 =>; 0 <=; 1 <~>)
% Maximal formula depth : 27 ( 8 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 66 ( 64 usr; 43 prp; 0-6 aty)
% Number of functors : 23 ( 23 usr; 3 con; 0-6 aty)
% Number of variables : 429 ( 351 !; 78 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A,B,C] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [D] :
? [E] :
! [F] :
( in(F,E)
<=> ( ? [G] :
( ? [H] :
( G = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
& F = H
& D = topstr_closure(A,G)
& element(H,the_carrier(B)) )
& netstr_induced_subset(G,A,B) )
& in(F,the_carrier(B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A,B,C] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [D] :
? [E] :
! [F] :
( in(F,E)
<=> ( ? [G] :
( ? [H] :
( G = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
& F = H
& D = topstr_closure(A,G)
& element(H,the_carrier(B)) )
& netstr_induced_subset(G,A,B) )
& in(F,the_carrier(B)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f13,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( nowhere_dense(B,A)
=> boundary_set(B,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( ( boundary_set(B,A)
& closed_subset(B,A) )
=> ( nowhere_dense(B,A)
& boundary_set(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( ( nowhere_dense(B,A)
& open_subset(B,A) )
=> ( nowhere_dense(B,A)
& boundary_set(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& closed_subset(B,A)
& open_subset(B,A)
& empty(B) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A,B] :
( ( net_str(B,A)
& ~ empty_carrier(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [C] :
( netstr_induced_subset(C,A,B)
=> element(C,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B,C] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [D] :
( ! [E,F,G] :
( ( ? [J] :
( ? [K] :
( J = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
& G = K
& D = topstr_closure(A,J)
& element(K,the_carrier(B)) )
& netstr_induced_subset(J,A,B) )
& E = G
& ? [H] :
( ? [I] :
( H = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
& F = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& E = F )
=> F = G )
=> ? [E] :
! [F] :
( in(F,E)
<=> ? [G] :
( ? [L] :
( ? [M] :
( L = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
& F = M
& D = topstr_closure(A,L)
& element(M,the_carrier(B)) )
& netstr_induced_subset(L,A,B) )
& G = F
& in(G,the_carrier(B)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,plain,
? [A,B,C] :
( ? [D] :
! [E] :
? [F] :
( in(F,E)
<~> ( ? [G] :
( ? [H] :
( G = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
& F = H
& D = topstr_closure(A,G)
& element(H,the_carrier(B)) )
& netstr_induced_subset(G,A,B) )
& in(F,the_carrier(B)) ) )
& net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f72,plain,
? [A,B,C] :
( ? [D] :
! [E] :
? [F] :
( ( ! [G] :
( ! [H] :
( G != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
| F != H
| D != topstr_closure(A,G)
| ~ element(H,the_carrier(B)) )
| ~ netstr_induced_subset(G,A,B) )
| ~ in(F,the_carrier(B))
| ~ in(F,E) )
& ( ( ? [G] :
( ? [H] :
( G = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
& F = H
& D = topstr_closure(A,G)
& element(H,the_carrier(B)) )
& netstr_induced_subset(G,A,B) )
& in(F,the_carrier(B)) )
| in(F,E) ) )
& net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
? [A,B] :
( ? [D] :
! [E] :
? [F] :
( ( ! [G] :
( ! [H] :
( G != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
| F != H
| D != topstr_closure(A,G)
| ~ element(H,the_carrier(B)) )
| ~ netstr_induced_subset(G,A,B) )
| ~ in(F,the_carrier(B))
| ~ in(F,E) )
& ( ( ? [G] :
( ? [H] :
( G = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,H)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,H)))
& F = H
& D = topstr_closure(A,G)
& element(H,the_carrier(B)) )
& netstr_induced_subset(G,A,B) )
& in(F,the_carrier(B)) )
| in(F,E) ) )
& net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
( ! [E] :
( ( ! [G] :
( ! [H] :
( G != relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,H)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,H)))
| sK3_skl(E) != H
| sK2_skl != topstr_closure(sK0_skl,G)
| ~ element(H,the_carrier(sK1_skl)) )
| ~ netstr_induced_subset(G,sK0_skl,sK1_skl) )
| ~ in(sK3_skl(E),the_carrier(sK1_skl))
| ~ in(sK3_skl(E),E) )
& ( ( sK4_skl(E) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(E))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(E))))
& sK3_skl(E) = sK5_skl(E)
& sK2_skl = topstr_closure(sK0_skl,sK4_skl(E))
& element(sK5_skl(E),the_carrier(sK1_skl))
& netstr_induced_subset(sK4_skl(E),sK0_skl,sK1_skl)
& in(sK3_skl(E),the_carrier(sK1_skl)) )
| in(sK3_skl(E),E) ) )
& net_str(sK1_skl,sK0_skl)
& directed_relstr(sK1_skl)
& transitive_relstr(sK1_skl)
& ~ empty_carrier(sK1_skl)
& top_str(sK0_skl)
& topological_space(sK0_skl)
& ~ empty_carrier(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl),skolemize(F,sK3_skl(E)),skolemize(G,sK4_skl(E)),skolemize(H,sK5_skl(E))],[f73]) ).
fof(f75,plain,
~ empty_carrier(sK0_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
topological_space(sK0_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f77,plain,
top_str(sK0_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,plain,
~ empty_carrier(sK1_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f79,plain,
transitive_relstr(sK1_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f80,plain,
directed_relstr(sK1_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f81,plain,
net_str(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f82,plain,
! [X0] :
( in(sK3_skl(X0),the_carrier(sK1_skl))
| in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f83,plain,
! [X0] :
( netstr_induced_subset(sK4_skl(X0),sK0_skl,sK1_skl)
| in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f84,plain,
! [X0] :
( element(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f85,plain,
! [X0] :
( sK2_skl = topstr_closure(sK0_skl,sK4_skl(X0))
| in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f86,plain,
! [X0] :
( sK3_skl(X0) = sK5_skl(X0)
| in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f87,plain,
! [X0] :
( sK4_skl(X0) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))
| in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f88,plain,
! [X0,X1,X2] :
( X1 != relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,X2)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,X2)))
| sK3_skl(X0) != X2
| sK2_skl != topstr_closure(sK0_skl,X1)
| ~ element(X2,the_carrier(sK1_skl))
| ~ netstr_induced_subset(X1,sK0_skl,sK1_skl)
| ~ in(sK3_skl(X0),the_carrier(sK1_skl))
| ~ in(sK3_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f144,plain,
! [A] :
( ! [B] :
( boundary_set(B,A)
| ~ nowhere_dense(B,A)
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f145,plain,
! [X0,X1] :
( boundary_set(X1,X0)
| ~ nowhere_dense(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f146,plain,
! [A] :
( ! [B] :
( ( nowhere_dense(B,A)
& boundary_set(B,A) )
| ~ boundary_set(B,A)
| ~ closed_subset(B,A)
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f148,plain,
! [X0,X1] :
( nowhere_dense(X1,X0)
| ~ boundary_set(X1,X0)
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
! [A] :
( ! [B] :
( ( nowhere_dense(B,A)
& boundary_set(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& closed_subset(B,A)
& open_subset(B,A)
& empty(B) )
| ~ nowhere_dense(B,A)
| ~ open_subset(B,A)
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f150,plain,
! [X0,X1] :
( empty(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f152,plain,
! [X0,X1] :
( closed_subset(X1,X0)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f153,plain,
! [X0,X1] :
( v1_membered(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f154,plain,
! [X0,X1] :
( v2_membered(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f279,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f280,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f292,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f293,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f294,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f65]) ).
fof(f295,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f296,plain,
! [A,B] :
( ! [C] :
( element(C,powerset(the_carrier(A)))
| ~ netstr_induced_subset(C,A,B) )
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f297,plain,
! [X0,X1,X2] :
( element(X2,powerset(the_carrier(X0)))
| ~ netstr_induced_subset(X2,X0,X1)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f302,plain,
! [A,B,C] :
( ! [D] :
( ? [E] :
! [F] :
( in(F,E)
<=> ? [G] :
( ? [L] :
( ? [M] :
( L = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
& F = M
& D = topstr_closure(A,L)
& element(M,the_carrier(B)) )
& netstr_induced_subset(L,A,B) )
& G = F
& in(G,the_carrier(B)) ) )
| ? [E,F,G] :
( F != G
& ? [J] :
( ? [K] :
( J = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
& G = K
& D = topstr_closure(A,J)
& element(K,the_carrier(B)) )
& netstr_induced_subset(J,A,B) )
& E = G
& ? [H] :
( ? [I] :
( H = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
& F = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& E = F ) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f303,definition,
! [A,B,D,E,F,G] :
( sP0_prd(G,F,E,D,B,A)
<=> ( F != G
& ? [J] :
( ? [K] :
( J = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
& G = K
& D = topstr_closure(A,J)
& element(K,the_carrier(B)) )
& netstr_induced_subset(J,A,B) )
& E = G
& ? [H] :
( ? [I] :
( H = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
& F = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& E = F ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f304,plain,
! [A,B,C] :
( ! [D] :
( ? [E] :
! [F] :
( in(F,E)
<=> ? [G] :
( ? [L] :
( ? [M] :
( L = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
& F = M
& D = topstr_closure(A,L)
& element(M,the_carrier(B)) )
& netstr_induced_subset(L,A,B) )
& G = F
& in(G,the_carrier(B)) ) )
| ? [E,F,G] : sP0_prd(G,F,E,D,B,A) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(formula_renaming,[status(thm)],[f302,f303]) ).
fof(f305,plain,
! [A,B,C] :
( ! [D] :
( ? [E] :
! [F] :
( ( ! [G] :
( ! [L] :
( ! [M] :
( L != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
| F != M
| D != topstr_closure(A,L)
| ~ element(M,the_carrier(B)) )
| ~ netstr_induced_subset(L,A,B) )
| G != F
| ~ in(G,the_carrier(B)) )
| in(F,E) )
& ( ? [G] :
( ? [L] :
( ? [M] :
( L = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
& F = M
& D = topstr_closure(A,L)
& element(M,the_carrier(B)) )
& netstr_induced_subset(L,A,B) )
& G = F
& in(G,the_carrier(B)) )
| ~ in(F,E) ) )
| ? [E,F,G] : sP0_prd(G,F,E,D,B,A) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f304]) ).
fof(f306,plain,
! [A,B] :
( ! [D] :
( ? [E] :
( ! [F] :
( ! [L] :
( ! [M] :
( L != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
| F != M
| D != topstr_closure(A,L)
| ~ element(M,the_carrier(B)) )
| ~ netstr_induced_subset(L,A,B) )
| ! [G] :
( G != F
| ~ in(G,the_carrier(B)) )
| in(F,E) )
& ! [F] :
( ( ? [L] :
( ? [M] :
( L = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
& F = M
& D = topstr_closure(A,L)
& element(M,the_carrier(B)) )
& netstr_induced_subset(L,A,B) )
& ? [G] :
( G = F
& in(G,the_carrier(B)) ) )
| ~ in(F,E) ) )
| ? [E,F,G] : sP0_prd(G,F,E,D,B,A) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(miniscoping,[status(thm)],[f305]) ).
fof(f307,plain,
! [A,B] :
( ! [D] :
( ( ! [F] :
( ! [L] :
( ! [M] :
( L != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,M)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,M)))
| F != M
| D != topstr_closure(A,L)
| ~ element(M,the_carrier(B)) )
| ~ netstr_induced_subset(L,A,B) )
| ! [G] :
( G != F
| ~ in(G,the_carrier(B)) )
| in(F,sK29_skl(D,B,A)) )
& ! [F] :
( ( sK31_skl(F,D,B,A) = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,sK32_skl(F,D,B,A))),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,sK32_skl(F,D,B,A))))
& F = sK32_skl(F,D,B,A)
& D = topstr_closure(A,sK31_skl(F,D,B,A))
& element(sK32_skl(F,D,B,A),the_carrier(B))
& netstr_induced_subset(sK31_skl(F,D,B,A),A,B)
& sK30_skl(F,D,B,A) = F
& in(sK30_skl(F,D,B,A),the_carrier(B)) )
| ~ in(F,sK29_skl(D,B,A)) ) )
| sP0_prd(sK28_skl(D,B,A),sK27_skl(D,B,A),sK26_skl(D,B,A),D,B,A) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl,sK32_skl]),skolemize(E,sK26_skl(D,B,A)),skolemize(F,sK27_skl(D,B,A)),skolemize(G,sK28_skl(D,B,A)),skolemize(E,sK29_skl(D,B,A)),skolemize(G,sK30_skl(F,D,B,A)),skolemize(L,sK31_skl(F,D,B,A)),skolemize(M,sK32_skl(F,D,B,A))],[f306]) ).
fof(f308,plain,
! [X0,X1,X2,X3] :
( in(sK30_skl(X3,X2,X1,X0),the_carrier(X1))
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f309,plain,
! [X0,X1,X2,X3] :
( sK30_skl(X3,X2,X1,X0) = X3
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f310,plain,
! [X0,X1,X2,X3] :
( netstr_induced_subset(sK31_skl(X3,X2,X1,X0),X0,X1)
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f311,plain,
! [X0,X1,X2,X3] :
( element(sK32_skl(X3,X2,X1,X0),the_carrier(X1))
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f312,plain,
! [X0,X1,X2,X3] :
( X2 = topstr_closure(X0,sK31_skl(X3,X2,X1,X0))
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f313,plain,
! [X0,X1,X2,X3] :
( X3 = sK32_skl(X3,X2,X1,X0)
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f314,plain,
! [X0,X1,X2,X3] :
( sK31_skl(X3,X2,X1,X0) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,sK32_skl(X3,X2,X1,X0))),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,sK32_skl(X3,X2,X1,X0))))
| ~ in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f315,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X5 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X6)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X6)))
| X3 != X6
| X2 != topstr_closure(X0,X5)
| ~ element(X6,the_carrier(X1))
| ~ netstr_induced_subset(X5,X0,X1)
| X4 != X3
| ~ in(X4,the_carrier(X1))
| in(X3,sK29_skl(X2,X1,X0))
| sP0_prd(sK28_skl(X2,X1,X0),sK27_skl(X2,X1,X0),sK26_skl(X2,X1,X0),X2,X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f316,plain,
! [A,B,D,E,F,G] :
( ( F = G
| ! [J] :
( ! [K] :
( J != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
| G != K
| D != topstr_closure(A,J)
| ~ element(K,the_carrier(B)) )
| ~ netstr_induced_subset(J,A,B) )
| E != G
| ! [H] :
( ! [I] :
( H != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
| F != I
| D != topstr_closure(A,H)
| ~ element(I,the_carrier(B)) )
| ~ netstr_induced_subset(H,A,B) )
| E != F
| sP0_prd(G,F,E,D,B,A) )
& ( ( F != G
& ? [J] :
( ? [K] :
( J = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
& G = K
& D = topstr_closure(A,J)
& element(K,the_carrier(B)) )
& netstr_induced_subset(J,A,B) )
& E = G
& ? [H] :
( ? [I] :
( H = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
& F = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& E = F )
| ~ sP0_prd(G,F,E,D,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f303]) ).
fof(f317,plain,
( ! [A,B,D,E,F,G] :
( F = G
| ! [J] :
( ! [K] :
( J != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
| G != K
| D != topstr_closure(A,J)
| ~ element(K,the_carrier(B)) )
| ~ netstr_induced_subset(J,A,B) )
| E != G
| ! [H] :
( ! [I] :
( H != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
| F != I
| D != topstr_closure(A,H)
| ~ element(I,the_carrier(B)) )
| ~ netstr_induced_subset(H,A,B) )
| E != F
| sP0_prd(G,F,E,D,B,A) )
& ! [A,B,D,E,F,G] :
( ( F != G
& ? [J] :
( ? [K] :
( J = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
& G = K
& D = topstr_closure(A,J)
& element(K,the_carrier(B)) )
& netstr_induced_subset(J,A,B) )
& E = G
& ? [H] :
( ? [I] :
( H = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
& F = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& E = F )
| ~ sP0_prd(G,F,E,D,B,A) ) ),
inference(miniscoping,[status(thm)],[f316]) ).
fof(f318,plain,
( ! [A,B,D,E,F,G] :
( F = G
| ! [J] :
( ! [K] :
( J != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,K)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,K)))
| G != K
| D != topstr_closure(A,J)
| ~ element(K,the_carrier(B)) )
| ~ netstr_induced_subset(J,A,B) )
| E != G
| ! [H] :
( ! [I] :
( H != relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,I)),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,I)))
| F != I
| D != topstr_closure(A,H)
| ~ element(I,the_carrier(B)) )
| ~ netstr_induced_subset(H,A,B) )
| E != F
| sP0_prd(G,F,E,D,B,A) )
& ! [A,B,D,E,F,G] :
( ( F != G
& sK35_skl(G,F,E,D,B,A) = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,sK36_skl(G,F,E,D,B,A))),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,sK36_skl(G,F,E,D,B,A))))
& G = sK36_skl(G,F,E,D,B,A)
& D = topstr_closure(A,sK35_skl(G,F,E,D,B,A))
& element(sK36_skl(G,F,E,D,B,A),the_carrier(B))
& netstr_induced_subset(sK35_skl(G,F,E,D,B,A),A,B)
& E = G
& sK33_skl(G,F,E,D,B,A) = relation_rng_as_subset(the_carrier(subnetstr_of_element(A,B,sK34_skl(G,F,E,D,B,A))),the_carrier(A),the_mapping(A,subnetstr_of_element(A,B,sK34_skl(G,F,E,D,B,A))))
& F = sK34_skl(G,F,E,D,B,A)
& D = topstr_closure(A,sK33_skl(G,F,E,D,B,A))
& element(sK34_skl(G,F,E,D,B,A),the_carrier(B))
& netstr_induced_subset(sK33_skl(G,F,E,D,B,A),A,B)
& E = F )
| ~ sP0_prd(G,F,E,D,B,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl,sK34_skl,sK35_skl,sK36_skl]),skolemize(H,sK33_skl(G,F,E,D,B,A)),skolemize(I,sK34_skl(G,F,E,D,B,A)),skolemize(J,sK35_skl(G,F,E,D,B,A)),skolemize(K,sK36_skl(G,F,E,D,B,A))],[f317]) ).
fof(f319,plain,
! [X0,X1,X2,X3,X4,X5] :
( X2 = X1
| ~ sP0_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f325,plain,
! [X0,X1,X2,X3,X4,X5] :
( X2 = X0
| ~ sP0_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f331,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 != X0
| ~ sP0_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f333,plain,
! [X0] :
( sK2_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(X0)))))
| ~ element(sK3_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK3_skl(X0),the_carrier(sK1_skl))
| ~ in(sK3_skl(X0),X0) ),
inference(destructive_equality_resolution,[status(thm)],[f88]) ).
fof(f334,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X1))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2))),X0,X1)
| ~ in(X2,the_carrier(X1))
| in(X2,sK29_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0))
| sP0_prd(sK28_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0),sK27_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0),sK26_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0),topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f315]) ).
fof(f335,plain,
! [X0,X1,X2,X3,X4] : ~ sP0_prd(X0,X0,X1,X2,X3,X4),
inference(destructive_equality_resolution,[status(thm)],[f331]) ).
fof(f340,definition,
( sQ0_spl
<=> top_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( sQ0_spl
| ~ top_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f350,definition,
( sQ3_spl
<=> topological_space(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f352,plain,
( sQ3_spl
| ~ topological_space(sK0_skl) ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f374,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl)
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f334]) ).
fof(f375,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl)
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f334]) ).
fof(f376,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl)
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f334]) ).
fof(f377,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f334]) ).
fof(f378,definition,
( sQ5_spl
<=> empty_carrier(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( ~ sQ5_spl
| empty_carrier(sK0_skl) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f381,definition,
( sQ6_spl
<=> empty_carrier(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( ~ sQ6_spl
| empty_carrier(sK1_skl) ),
inference(component_clause,[status(thm)],[f381]) ).
fof(f384,definition,
( sQ7_spl
<=> transitive_relstr(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f386,plain,
( sQ7_spl
| ~ transitive_relstr(sK1_skl) ),
inference(component_clause,[status(thm)],[f384]) ).
fof(f387,definition,
( sQ8_spl
<=> directed_relstr(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ8_spl
| ~ directed_relstr(sK1_skl) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f390,definition,
( sQ9_spl
<=> net_str(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f392,plain,
( sQ9_spl
| ~ net_str(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,definition,
! [X0] :
( sQ10_spl
<=> ( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f394,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f396,plain,
( sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f374,f378,f350,f340,f381,f384,f387,f390,f393]) ).
fof(f397,definition,
! [X0] :
( sQ11_spl
<=> ( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( sQ11_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f375,f378,f350,f340,f381,f384,f387,f390,f397]) ).
fof(f401,definition,
! [X0] :
( sQ12_spl
<=> ( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( sQ12_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f376,f378,f350,f340,f381,f384,f387,f390,f401]) ).
fof(f405,definition,
! [X0] :
( sQ13_spl
<=> ( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( sQ13_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f377,f378,f350,f340,f381,f384,f387,f390,f405]) ).
fof(f409,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f342,f77]) ).
fof(f410,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f409]) ).
fof(f411,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f352,f76]) ).
fof(f412,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f411]) ).
fof(f413,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f81]) ).
fof(f414,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f413]) ).
fof(f415,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f80]) ).
fof(f416,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f415]) ).
fof(f417,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f79]) ).
fof(f418,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f417]) ).
fof(f419,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f78]) ).
fof(f420,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f419]) ).
fof(f421,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f379,f75]) ).
fof(f422,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f421]) ).
fof(f423,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f394,f84]) ).
fof(f428,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f423]) ).
fof(f432,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f428]) ).
fof(f437,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f432]) ).
fof(f441,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f437]) ).
fof(f446,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f441]) ).
fof(f450,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f446]) ).
fof(f451,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f85,f450]) ).
fof(f455,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f451]) ).
fof(f459,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f85,f455]) ).
fof(f462,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f459]) ).
fof(f465,plain,
! [X0] :
( ~ sQ10_spl
| ~ in(sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f462,f280]) ).
fof(f466,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f462]) ).
fof(f467,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f466]) ).
fof(f468,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f85,f467]) ).
fof(f470,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f468]) ).
fof(f472,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f85,f470]) ).
fof(f473,definition,
( sQ14_spl
<=> sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( ~ sQ14_spl
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f475,plain,
( sQ14_spl
| ~ sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,definition,
! [X0] :
( sQ15_spl
<=> ( in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f477,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f479,plain,
( ~ sQ10_spl
| sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f472,f473,f476,f393]) ).
fof(f498,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ in(sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f465]) ).
fof(f499,plain,
! [X0] :
( ~ sQ10_spl
| ~ in(sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f498]) ).
fof(f500,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ in(sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f85,f499]) ).
fof(f502,plain,
! [X0] :
( ~ sQ10_spl
| ~ in(sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f500]) ).
fof(f504,plain,
! [X0] :
( ~ sQ10_spl
| in(sK3_skl(X0),X0)
| ~ in(sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f85,f502]) ).
fof(f505,definition,
! [X0] :
( sQ16_spl
<=> ( in(sK3_skl(X0),X0)
| ~ in(sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl),sK5_skl(X0))
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( ~ sQ10_spl
| sQ16_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f504,f473,f505,f393]) ).
fof(f617,definition,
( sQ18_spl
<=> one_sorted_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f619,plain,
( sQ18_spl
| ~ one_sorted_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f625,plain,
( rel_str(sK1_skl)
| ~ one_sorted_str(sK0_skl) ),
inference(resolution,[status(thm)],[f295,f81]) ).
fof(f629,definition,
( sQ19_spl
<=> rel_str(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f625,f617,f629]) ).
fof(f633,plain,
( ~ sQ14_spl
| sK26_skl(sK2_skl,sK1_skl,sK0_skl) = sK27_skl(sK2_skl,sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f319,f474]) ).
fof(f663,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X1))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2))),X0,X1)
| ~ in(X2,the_carrier(X1))
| in(X2,sK29_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| sK26_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0) = sK27_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0) ),
inference(resolution,[status(thm)],[f319,f334]) ).
fof(f682,plain,
( ~ sQ14_spl
| sK26_skl(sK2_skl,sK1_skl,sK0_skl) = sK28_skl(sK2_skl,sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f325,f474]) ).
fof(f712,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X1))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2))),X0,X1)
| ~ in(X2,the_carrier(X1))
| in(X2,sK29_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0)
| sK26_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0) = sK28_skl(topstr_closure(X0,relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X2)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X2)))),X1,X0) ),
inference(resolution,[status(thm)],[f325,f334]) ).
fof(f874,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl)
| sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) = sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f663]) ).
fof(f875,definition,
! [X0] :
( sQ26_spl
<=> ( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) = sK27_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f878,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f874,f875,f378,f350,f340,f381,f384,f387,f390]) ).
fof(f879,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl)
| sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) = sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f87,f712]) ).
fof(f880,definition,
! [X0] :
( sQ27_spl
<=> ( in(sK3_skl(X0),X0)
| ~ element(sK5_skl(X0),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl))
| sK26_skl(topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))))),sK1_skl,sK0_skl) = sK28_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f883,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f879,f880,f378,f350,f340,f381,f384,f387,f390]) ).
fof(f937,plain,
( sQ18_spl
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f619,f293]) ).
fof(f938,plain,
( sQ18_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f937,f340,f617]) ).
fof(f949,plain,
( ~ sQ14_spl
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f633,f474]) ).
fof(f993,definition,
! [X0] :
( sQ34_spl
<=> ( sK2_skl = topstr_closure(sK0_skl,sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f994,plain,
! [X0] :
( ~ sQ34_spl
| sK2_skl = topstr_closure(sK0_skl,sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f993]) ).
fof(f997,definition,
! [X0] :
( sQ35_spl
<=> ( sK30_skl(X0,sK2_skl,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f998,plain,
! [X0] :
( ~ sQ35_spl
| sK30_skl(X0,sK2_skl,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f997]) ).
fof(f1001,definition,
! [X0] :
( sQ36_spl
<=> ( X0 = sK32_skl(X0,sK2_skl,sK1_skl,sK0_skl)
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1002,plain,
! [X0] :
( ~ sQ36_spl
| X0 = sK32_skl(X0,sK2_skl,sK1_skl,sK0_skl)
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1001]) ).
fof(f1008,definition,
! [X0] :
( sQ38_spl
<=> ( element(sK32_skl(X0,sK2_skl,sK1_skl,sK0_skl),the_carrier(sK1_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
! [X0] :
( ~ sQ38_spl
| element(sK32_skl(X0,sK2_skl,sK1_skl,sK0_skl),the_carrier(sK1_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1008]) ).
fof(f1013,definition,
! [X0] :
( sQ39_spl
<=> ( netstr_induced_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl)
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1014,plain,
! [X0] :
( ~ sQ39_spl
| netstr_induced_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl)
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1013]) ).
fof(f1019,definition,
! [X0] :
( sQ40_spl
<=> ( in(sK30_skl(X0,sK2_skl,sK1_skl,sK0_skl),the_carrier(sK1_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1020,plain,
! [X0] :
( ~ sQ40_spl
| in(sK30_skl(X0,sK2_skl,sK1_skl,sK0_skl),the_carrier(sK1_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1019]) ).
fof(f1088,plain,
( ~ sQ35_spl
| sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) = sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| sK30_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f998,f86]) ).
fof(f1089,definition,
( sQ47_spl
<=> sK30_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1090,plain,
( ~ sQ47_spl
| sK30_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1089]) ).
fof(f1092,definition,
( sQ48_spl
<=> sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) = sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1093,plain,
( ~ sQ48_spl
| sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) = sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1092]) ).
fof(f1095,plain,
( ~ sQ35_spl
| sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1088,f1089,f1092,f997]) ).
fof(f1096,plain,
( ~ sQ14_spl
| sP0_prd(sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f682,f949]) ).
fof(f1097,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1096,f335]) ).
fof(f1098,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f1097]) ).
fof(f1101,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK5_skl(X0)))),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f477]) ).
fof(f1103,plain,
! [X0] :
( sQ14_spl
| element(sK32_skl(X0,sK2_skl,sK1_skl,sK0_skl),the_carrier(sK1_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f311]) ).
fof(f1104,plain,
! [X0] :
( sQ14_spl
| sK2_skl = topstr_closure(sK0_skl,sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f312]) ).
fof(f1105,plain,
! [X0] :
( sQ14_spl
| netstr_induced_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl)
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f310]) ).
fof(f1106,plain,
! [X0] :
( sQ14_spl
| X0 = sK32_skl(X0,sK2_skl,sK1_skl,sK0_skl)
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f313]) ).
fof(f1107,plain,
! [X0] :
( sQ14_spl
| sK30_skl(X0,sK2_skl,sK1_skl,sK0_skl) = X0
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f309]) ).
fof(f1108,plain,
! [X0] :
( sQ14_spl
| in(sK30_skl(X0,sK2_skl,sK1_skl,sK0_skl),the_carrier(sK1_skl))
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f308]) ).
fof(f1109,plain,
( sQ14_spl
| sQ38_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1103,f378,f350,f340,f381,f384,f387,f390,f1008,f473]) ).
fof(f1110,plain,
( sQ14_spl
| sQ34_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1104,f378,f350,f340,f381,f384,f387,f390,f993,f473]) ).
fof(f1111,plain,
( sQ14_spl
| sQ39_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1105,f378,f350,f340,f381,f384,f387,f390,f1013,f473]) ).
fof(f1112,plain,
( sQ14_spl
| sQ36_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1106,f378,f350,f340,f381,f384,f387,f390,f1001,f473]) ).
fof(f1113,plain,
( sQ14_spl
| sQ35_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1107,f378,f350,f340,f381,f384,f387,f390,f997,f473]) ).
fof(f1114,plain,
( sQ14_spl
| sQ40_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1108,f378,f350,f340,f381,f384,f387,f390,f1019,f473]) ).
fof(f1134,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(sK4_skl(X0),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f87,f1101]) ).
fof(f1135,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| ~ netstr_induced_subset(sK4_skl(X0),sK0_skl,sK1_skl)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1134]) ).
fof(f1136,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(topstr_closure(sK0_skl,sK4_skl(X0)),sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1135,f83]) ).
fof(f1138,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| in(sK3_skl(X0),X0)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f85,f1136]) ).
fof(f1139,plain,
! [X0] :
( ~ sQ15_spl
| in(sK3_skl(X0),X0)
| ~ in(sK5_skl(X0),the_carrier(sK1_skl))
| in(sK5_skl(X0),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1138]) ).
fof(f1497,plain,
( ~ sQ47_spl
| ~ sQ40_spl
| in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl))
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1090,f1020]) ).
fof(f1502,definition,
( sQ50_spl
<=> in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1503,plain,
( ~ sQ50_spl
| in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1502]) ).
fof(f1504,plain,
( sQ50_spl
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1502]) ).
fof(f1509,definition,
( sQ52_spl
<=> in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( ~ sQ47_spl
| ~ sQ40_spl
| sQ52_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1497,f1502,f1509,f1019,f1089]) ).
fof(f1635,plain,
( sQ50_spl
| sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) = sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f1504,f86]) ).
fof(f1671,definition,
( sQ56_spl
<=> in(sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1673,plain,
( sQ56_spl
| ~ in(sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1671]) ).
fof(f1781,definition,
( sQ84_spl
<=> element(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1795,plain,
( sQ56_spl
| ~ sQ48_spl
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f1093,f1673]) ).
fof(f1800,plain,
( sQ56_spl
| ~ sQ48_spl
| in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f1795,f82]) ).
fof(f1801,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| sK30_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f1503,f998]) ).
fof(f1802,plain,
( ~ sQ36_spl
| ~ sQ50_spl
| sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)) = sK32_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f1503,f1002]) ).
fof(f1804,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1801,f1089,f1502,f997]) ).
fof(f1886,plain,
( ~ sQ36_spl
| ~ sQ50_spl
| ~ sQ38_spl
| element(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl))
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1802,f1009]) ).
fof(f1889,plain,
( ~ sQ36_spl
| ~ sQ50_spl
| sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK32_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))))
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| sP0_prd(sK28_skl(sK2_skl,sK1_skl,sK0_skl),sK27_skl(sK2_skl,sK1_skl,sK0_skl),sK26_skl(sK2_skl,sK1_skl,sK0_skl),sK2_skl,sK1_skl,sK0_skl)
| ~ net_str(sK1_skl,sK0_skl)
| ~ directed_relstr(sK1_skl)
| ~ transitive_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1802,f314]) ).
fof(f1891,plain,
( ~ sQ36_spl
| ~ sQ38_spl
| sQ84_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1886,f1502,f1781,f1008,f1001]) ).
fof(f1894,definition,
( sQ91_spl
<=> sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK32_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1895,plain,
( ~ sQ91_spl
| sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK32_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl))))) ),
inference(component_clause,[status(thm)],[f1894]) ).
fof(f1897,plain,
( ~ sQ36_spl
| sQ91_spl
| ~ sQ50_spl
| sQ14_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1889,f378,f350,f340,f381,f384,f387,f390,f473,f1502,f1894,f1001]) ).
fof(f1902,plain,
( ~ sQ91_spl
| ~ sQ36_spl
| ~ sQ50_spl
| sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl))))) ),
inference(forward_demodulation,[status(thm)],[f1802,f1895]) ).
fof(f1938,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| boundary_set(X1,X0)
| ~ nowhere_dense(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f145,f297]) ).
fof(f1954,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| empty_carrier(X0)
| boundary_set(X1,X0)
| ~ nowhere_dense(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1938,f293]) ).
fof(f1969,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| nowhere_dense(X1,X0)
| ~ boundary_set(X1,X0)
| ~ closed_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f148,f297]) ).
fof(f1984,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| empty_carrier(X0)
| nowhere_dense(X1,X0)
| ~ boundary_set(X1,X0)
| ~ closed_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1969,f293]) ).
fof(f1999,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| empty(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f150,f297]) ).
fof(f2022,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| empty_carrier(X0)
| empty(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1999,f293]) ).
fof(f2023,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| boundary_set(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f1954,f1014]) ).
fof(f2026,definition,
! [X0] :
( sQ97_spl
<=> ( ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| boundary_set(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f2029,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| sQ97_spl
| ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2023,f350,f340,f2026,f378,f381,f390,f1013]) ).
fof(f2032,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| empty(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f2022,f1014]) ).
fof(f2035,definition,
! [X0] :
( sQ98_spl
<=> ( ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| empty(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2038,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| sQ98_spl
| ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2032,f350,f340,f2035,f378,f381,f390,f1013]) ).
fof(f2041,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ boundary_set(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ closed_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f1984,f1014]) ).
fof(f2044,definition,
! [X0] :
( sQ99_spl
<=> ( ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ boundary_set(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ closed_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2047,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| sQ99_spl
| ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2041,f350,f340,f2044,f378,f381,f390,f1013]) ).
fof(f2084,definition,
( sQ100_spl
<=> netstr_induced_subset(sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2086,plain,
( sQ100_spl
| ~ netstr_induced_subset(sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f2084]) ).
fof(f2087,definition,
( sQ101_spl
<=> sK2_skl = topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2089,plain,
( sQ101_spl
| sK2_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))))) ),
inference(component_clause,[status(thm)],[f2087]) ).
fof(f2158,plain,
( ~ sQ39_spl
| sQ100_spl
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f2086,f1014]) ).
fof(f2161,plain,
( ~ sQ39_spl
| sQ100_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f2158,f1502,f2084,f1013]) ).
fof(f2165,plain,
! [X0] :
( ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| nowhere_dense(sK4_skl(X0),sK0_skl)
| ~ boundary_set(sK4_skl(X0),sK0_skl)
| ~ closed_subset(sK4_skl(X0),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| in(sK3_skl(X0),X0) ),
inference(resolution,[status(thm)],[f83,f1984]) ).
fof(f2166,plain,
! [X0] :
( ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| empty(sK4_skl(X0))
| ~ nowhere_dense(sK4_skl(X0),sK0_skl)
| ~ open_subset(sK4_skl(X0),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| in(sK3_skl(X0),X0) ),
inference(resolution,[status(thm)],[f83,f2022]) ).
fof(f2167,plain,
! [X0] :
( ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| boundary_set(sK4_skl(X0),sK0_skl)
| ~ nowhere_dense(sK4_skl(X0),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| in(sK3_skl(X0),X0) ),
inference(resolution,[status(thm)],[f83,f1954]) ).
fof(f2169,definition,
! [X0] :
( sQ115_spl
<=> ( nowhere_dense(sK4_skl(X0),sK0_skl)
| ~ boundary_set(sK4_skl(X0),sK0_skl)
| ~ closed_subset(sK4_skl(X0),sK0_skl)
| in(sK3_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f2172,plain,
( ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f2165,f2169,f350,f340,f378,f381,f390]) ).
fof(f2173,definition,
! [X0] :
( sQ116_spl
<=> ( empty(sK4_skl(X0))
| ~ nowhere_dense(sK4_skl(X0),sK0_skl)
| ~ open_subset(sK4_skl(X0),sK0_skl)
| in(sK3_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f2176,plain,
( ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f2166,f2173,f350,f340,f378,f381,f390]) ).
fof(f2177,definition,
! [X0] :
( sQ117_spl
<=> ( boundary_set(sK4_skl(X0),sK0_skl)
| ~ nowhere_dense(sK4_skl(X0),sK0_skl)
| in(sK3_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2180,plain,
( ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| ~ sQ0_spl
| ~ sQ3_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2167,f2177,f350,f340,f378,f381,f390]) ).
fof(f2281,plain,
( ~ sQ48_spl
| ~ sQ15_spl
| in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ in(sK5_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl))
| in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1093,f1139]) ).
fof(f2282,plain,
( ~ sQ48_spl
| ~ sQ15_spl
| ~ sQ56_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2281,f1502,f1671,f476,f1092]) ).
fof(f2442,plain,
( ~ sQ91_spl
| ~ sQ36_spl
| ~ sQ50_spl
| sK2_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl))))))
| ~ element(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl))
| ~ netstr_induced_subset(sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl)
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),the_carrier(sK1_skl))
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1902,f333]) ).
fof(f2443,plain,
( ~ sQ91_spl
| ~ sQ36_spl
| ~ sQ101_spl
| ~ sQ84_spl
| ~ sQ100_spl
| ~ sQ52_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f2442,f1502,f1509,f2084,f1781,f2087,f1001,f1894]) ).
fof(f2444,plain,
( sQ101_spl
| ~ sQ91_spl
| ~ sQ36_spl
| ~ sQ50_spl
| sK2_skl != topstr_closure(sK0_skl,sK31_skl(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK2_skl,sK1_skl,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1902,f2089]) ).
fof(f2482,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| closed_subset(X1,X0)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f152,f297]) ).
fof(f2494,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| empty_carrier(X0)
| closed_subset(X1,X0)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2482,f293]) ).
fof(f2510,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| v1_membered(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f153,f297]) ).
fof(f2526,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| empty_carrier(X0)
| v1_membered(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2510,f293]) ).
fof(f2542,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| v2_membered(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f154,f297]) ).
fof(f2558,plain,
! [X0,X1,X2] :
( ~ netstr_induced_subset(X1,X0,X2)
| ~ net_str(X2,X0)
| empty_carrier(X2)
| empty_carrier(X0)
| v2_membered(X1)
| ~ nowhere_dense(X1,X0)
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2542,f293]) ).
fof(f2559,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| v1_membered(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f2526,f1014]) ).
fof(f2562,definition,
! [X0] :
( sQ136_spl
<=> ( ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| v1_membered(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f2565,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| sQ136_spl
| ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2559,f350,f340,f2562,f378,f381,f390,f1013]) ).
fof(f2568,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| v2_membered(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f2558,f1014]) ).
fof(f2571,definition,
! [X0] :
( sQ137_spl
<=> ( ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| v2_membered(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl))
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2574,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| sQ137_spl
| ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2568,f350,f340,f2571,f378,f381,f390,f1013]) ).
fof(f2577,plain,
! [X0] :
( ~ sQ39_spl
| ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| empty_carrier(sK0_skl)
| closed_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f2494,f1014]) ).
fof(f2580,definition,
! [X0] :
( sQ138_spl
<=> ( ~ in(X0,sK29_skl(sK2_skl,sK1_skl,sK0_skl))
| closed_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ nowhere_dense(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl)
| ~ open_subset(sK31_skl(X0,sK2_skl,sK1_skl,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f2583,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ6_spl
| sQ5_spl
| sQ138_spl
| ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2577,f350,f340,f2580,f378,f381,f390,f1013]) ).
fof(f2675,plain,
( ~ sQ34_spl
| sQ101_spl
| ~ sQ91_spl
| ~ sQ36_spl
| ~ sQ50_spl
| ~ in(sK3_skl(sK29_skl(sK2_skl,sK1_skl,sK0_skl)),sK29_skl(sK2_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f2444,f994]) ).
fof(f2676,plain,
( ~ sQ34_spl
| sQ101_spl
| ~ sQ91_spl
| ~ sQ36_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f2675,f1502,f1001,f1894,f2087,f993]) ).
fof(f2679,plain,
( sQ56_spl
| ~ sQ48_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1800,f1502,f1092,f1671]) ).
fof(f2680,plain,
( sQ50_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1635,f1092,f1502]) ).
fof(f2681,plain,
$false,
inference(sat_refutation,[status(thm)],[f396,f400,f404,f408,f410,f412,f414,f416,f418,f420,f422,f479,f508,f632,f878,f883,f938,f1095,f1098,f1109,f1110,f1111,f1112,f1113,f1114,f1512,f1804,f1891,f1897,f2029,f2038,f2047,f2161,f2172,f2176,f2180,f2282,f2443,f2565,f2574,f2583,f2676,f2679,f2680]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU399+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/10.60 % Computer : n013.cluster.edu
% 0.12/10.60 % Model : x86_64 x86_64
% 0.12/10.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.60 % Memory : 8046.5625MB
% 0.12/10.60 % OS : Linux 6.8.0-71-generic
% 0.12/10.60 % CPULimit : 300
% 0.12/10.60 % WCLimit : 300
% 0.12/10.60 % DateTime : Mon Sep 21 06:19:51 UTC 2026
% 0.12/10.61 % CPUTime :
% 0.12/10.62 % Drodi V4.1.1
% 0.16/11.12 % Refutation found
% 0.16/11.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/11.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.16/11.16 % Elapsed time: 0.549309 seconds
% 0.16/11.16 % CPU time: 4.049839 seconds
% 0.16/11.16 % Total memory used: 151.229 MB
% 0.16/11.16 % Net memory used: 149.023 MB
%------------------------------------------------------------------------------