%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU401+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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.09s 0.57s
% Output : CNFRefutation 0.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 85
% Syntax : Number of formulae : 410 ( 21 unt; 61 def)
% Number of atoms : 1624 ( 198 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 1972 ( 758 ~; 863 |; 242 &)
% ( 69 <=>; 39 =>; 0 <=; 1 <~>)
% Maximal formula depth : 27 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 90 ( 88 usr; 62 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 6 con; 0-4 aty)
% Number of variables : 364 ( 318 !; 46 ?)
% 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] :
( ( ! [G] :
( in(G,F)
<=> ( ? [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) )
& in(G,the_carrier(B)) ) )
& ! [G] :
( in(G,E)
<=> ( ? [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)))
& G = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& in(G,the_carrier(B)) ) ) )
=> E = F ) ),
file('/export/starexec/sandbox2/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] :
( ( ! [G] :
( in(G,F)
<=> ( ? [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) )
& in(G,the_carrier(B)) ) )
& ! [G] :
( in(G,E)
<=> ( ? [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)))
& G = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& in(G,the_carrier(B)) ) ) )
=> E = F ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [A] :
( top_str(A)
=> ? [B] :
( boundary_set(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& empty(B)
& element(B,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( ( top_str(A)
& topological_space(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)
& element(B,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A,B,C,D] :
( ( relation_of2(D,B,the_carrier(A))
& quasi_total(D,B,the_carrier(A))
& function(D)
& relation_of2(C,B,B)
& one_sorted_str(A) )
=> ( net_str(net_str_of(A,B,C,D),A)
& strict_net_str(net_str_of(A,B,C,D),A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( empty(B)
=> ( closed_subset(B,A)
& open_subset(B,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( empty(B)
=> nowhere_dense(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B] :
( ( net_str(B,A)
& one_sorted_str(A) )
=> ( strict_net_str(B,A)
=> B = net_str_of(A,the_carrier(B),the_InternalRel(B),the_mapping(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B,C] :
( ( element(C,the_carrier(B))
& net_str(B,A)
& ~ empty_carrier(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> ( net_str(netstr_restr_to_element(A,B,C),A)
& strict_net_str(netstr_restr_to_element(A,B,C),A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A,B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [C] :
( subnet(C,A,B)
=> ( net_str(C,A)
& directed_relstr(C)
& transitive_relstr(C)
& ~ empty_carrier(C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> closed_subset(topstr_closure(A,B),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A] :
( one_sorted_str(A)
=> ? [B] :
( strict_net_str(B,A)
& net_str(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> relation_rng_as_subset(A,B,C) = relation_rng(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A,B,C] :
( ( element(C,the_carrier(B))
& net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> subnetstr_of_element(A,B,C) = netstr_restr_to_element(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A) )
=> element(topstr_closure(A,B),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,plain,
? [A,B,C] :
( ? [D,E,F] :
( E != F
& ! [G] :
( in(G,F)
<=> ( ? [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) )
& in(G,the_carrier(B)) ) )
& ! [G] :
( in(G,E)
<=> ( ? [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)))
& G = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& in(G,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] :
( 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) )
| ~ in(G,the_carrier(B))
| in(G,F) )
& ( ( ? [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) )
& in(G,the_carrier(B)) )
| ~ in(G,F) ) )
& ! [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)))
| G != I
| D != topstr_closure(A,H)
| ~ element(I,the_carrier(B)) )
| ~ netstr_induced_subset(H,A,B) )
| ~ in(G,the_carrier(B))
| in(G,E) )
& ( ( ? [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)))
& G = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& in(G,the_carrier(B)) )
| ~ in(G,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] :
( ? [E,F] :
( E != F
& ? [D] :
( ! [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) )
| ~ in(G,the_carrier(B))
| in(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) )
& in(G,the_carrier(B)) )
| ~ in(G,F) )
& ! [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)))
| G != I
| D != topstr_closure(A,H)
| ~ element(I,the_carrier(B)) )
| ~ netstr_induced_subset(H,A,B) )
| ~ in(G,the_carrier(B))
| in(G,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)))
& G = I
& D = topstr_closure(A,H)
& element(I,the_carrier(B)) )
& netstr_induced_subset(H,A,B) )
& in(G,the_carrier(B)) )
| ~ in(G,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,
( sK2_skl != sK3_skl
& ! [G] :
( ! [J] :
( ! [K] :
( J != relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,K)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,K)))
| G != K
| sK4_skl != topstr_closure(sK0_skl,J)
| ~ element(K,the_carrier(sK1_skl)) )
| ~ netstr_induced_subset(J,sK0_skl,sK1_skl) )
| ~ in(G,the_carrier(sK1_skl))
| in(G,sK3_skl) )
& ! [G] :
( ( sK7_skl(G) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(G))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(G))))
& G = sK8_skl(G)
& sK4_skl = topstr_closure(sK0_skl,sK7_skl(G))
& element(sK8_skl(G),the_carrier(sK1_skl))
& netstr_induced_subset(sK7_skl(G),sK0_skl,sK1_skl)
& in(G,the_carrier(sK1_skl)) )
| ~ in(G,sK3_skl) )
& ! [G] :
( ! [H] :
( ! [I] :
( H != relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,I)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,I)))
| G != I
| sK4_skl != topstr_closure(sK0_skl,H)
| ~ element(I,the_carrier(sK1_skl)) )
| ~ netstr_induced_subset(H,sK0_skl,sK1_skl) )
| ~ in(G,the_carrier(sK1_skl))
| in(G,sK2_skl) )
& ! [G] :
( ( sK5_skl(G) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(G))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(G))))
& G = sK6_skl(G)
& sK4_skl = topstr_closure(sK0_skl,sK5_skl(G))
& element(sK6_skl(G),the_carrier(sK1_skl))
& netstr_induced_subset(sK5_skl(G),sK0_skl,sK1_skl)
& in(G,the_carrier(sK1_skl)) )
| ~ in(G,sK2_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(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(E,sK2_skl),skolemize(F,sK3_skl),skolemize(D,sK4_skl),skolemize(H,sK5_skl(G)),skolemize(I,sK6_skl(G)),skolemize(J,sK7_skl(G)),skolemize(K,sK8_skl(G))],[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(X0,the_carrier(sK1_skl))
| ~ in(X0,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f83,plain,
! [X0] :
( netstr_induced_subset(sK5_skl(X0),sK0_skl,sK1_skl)
| ~ in(X0,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f84,plain,
! [X0] :
( element(sK6_skl(X0),the_carrier(sK1_skl))
| ~ in(X0,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f85,plain,
! [X0] :
( sK4_skl = topstr_closure(sK0_skl,sK5_skl(X0))
| ~ in(X0,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f86,plain,
! [X0] :
( X0 = sK6_skl(X0)
| ~ in(X0,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f87,plain,
! [X0] :
( sK5_skl(X0) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(X0))))
| ~ in(X0,sK2_skl) ),
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)))
| X0 != X2
| sK4_skl != topstr_closure(sK0_skl,X1)
| ~ element(X2,the_carrier(sK1_skl))
| ~ netstr_induced_subset(X1,sK0_skl,sK1_skl)
| ~ in(X0,the_carrier(sK1_skl))
| in(X0,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f89,plain,
! [X0] :
( in(X0,the_carrier(sK1_skl))
| ~ in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f90,plain,
! [X0] :
( netstr_induced_subset(sK7_skl(X0),sK0_skl,sK1_skl)
| ~ in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f91,plain,
! [X0] :
( element(sK8_skl(X0),the_carrier(sK1_skl))
| ~ in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f92,plain,
! [X0] :
( sK4_skl = topstr_closure(sK0_skl,sK7_skl(X0))
| ~ in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f93,plain,
! [X0] :
( X0 = sK8_skl(X0)
| ~ in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f94,plain,
! [X0] :
( sK7_skl(X0) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(X0))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(X0))))
| ~ in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f95,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)))
| X0 != X2
| sK4_skl != topstr_closure(sK0_skl,X1)
| ~ element(X2,the_carrier(sK1_skl))
| ~ netstr_induced_subset(X1,sK0_skl,sK1_skl)
| ~ in(X0,the_carrier(sK1_skl))
| in(X0,sK3_skl) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f96,plain,
sK2_skl != sK3_skl,
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f97,plain,
! [A] :
( ? [B] :
( boundary_set(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& empty(B)
& element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f98,plain,
! [A] :
( ( boundary_set(sK9_skl(A),A)
& v5_membered(sK9_skl(A))
& v4_membered(sK9_skl(A))
& v3_membered(sK9_skl(A))
& v2_membered(sK9_skl(A))
& v1_membered(sK9_skl(A))
& empty(sK9_skl(A))
& element(sK9_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f97]) ).
fof(f99,plain,
! [X0] :
( element(sK9_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0] :
( empty(sK9_skl(X0))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f106,plain,
! [X0] :
( boundary_set(sK9_skl(X0),X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f107,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)
& element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f108,plain,
! [A] :
( ( nowhere_dense(sK10_skl(A),A)
& boundary_set(sK10_skl(A),A)
& v5_membered(sK10_skl(A))
& v4_membered(sK10_skl(A))
& v3_membered(sK10_skl(A))
& v2_membered(sK10_skl(A))
& v1_membered(sK10_skl(A))
& closed_subset(sK10_skl(A),A)
& open_subset(sK10_skl(A),A)
& empty(sK10_skl(A))
& element(sK10_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f107]) ).
fof(f109,plain,
! [X0] :
( element(sK10_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f111,plain,
! [X0] :
( open_subset(sK10_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f119,plain,
! [X0] :
( nowhere_dense(sK10_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f152,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(f153,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)],[f152]) ).
fof(f154,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(f156,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)],[f154]) ).
fof(f157,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(f158,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)],[f157]) ).
fof(f160,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)],[f157]) ).
fof(f182,plain,
! [A,B,C,D] :
( ( net_str(net_str_of(A,B,C,D),A)
& strict_net_str(net_str_of(A,B,C,D),A) )
| ~ relation_of2(D,B,the_carrier(A))
| ~ quasi_total(D,B,the_carrier(A))
| ~ function(D)
| ~ relation_of2(C,B,B)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( net_str(net_str_of(X0,X2,X1,X3),X0)
| ~ relation_of2(X3,X2,the_carrier(X0))
| ~ quasi_total(X3,X2,the_carrier(X0))
| ~ function(X3)
| ~ relation_of2(X1,X2,X2)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f185,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f186,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f211,plain,
! [A] :
( ! [B] :
( ( closed_subset(B,A)
& open_subset(B,A) )
| ~ empty(B)
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f212,plain,
! [X0,X1] :
( open_subset(X1,X0)
| ~ empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f216,plain,
! [A] :
( ! [B] :
( nowhere_dense(B,A)
| ~ empty(B)
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f217,plain,
! [X0,X1] :
( nowhere_dense(X1,X0)
| ~ empty(X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f237,plain,
! [A,B] :
( B = net_str_of(A,the_carrier(B),the_InternalRel(B),the_mapping(A,B))
| ~ strict_net_str(B,A)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f238,plain,
! [X0,X1] :
( X1 = net_str_of(X0,the_carrier(X1),the_InternalRel(X1),the_mapping(X0,X1))
| ~ strict_net_str(X1,X0)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f239,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f240,plain,
( ! [A,B,C] :
( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ! [A,B,C] :
( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f239]) ).
fof(f241,plain,
! [X0,X1,X2] :
( relation_of2(X0,X1,X2)
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f243,plain,
! [A,B,C] :
( ( net_str(netstr_restr_to_element(A,B,C),A)
& strict_net_str(netstr_restr_to_element(A,B,C),A) )
| ~ element(C,the_carrier(B))
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f244,plain,
! [X0,X1,X2] :
( strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f245,plain,
! [X0,X1,X2] :
( net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f250,plain,
! [A,B] :
( ! [C] :
( ( net_str(C,A)
& directed_relstr(C)
& transitive_relstr(C)
& ~ empty_carrier(C) )
| ~ subnet(C,A,B) )
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f254,plain,
! [X0,X1,X2] :
( net_str(X2,X0)
| ~ subnet(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f256,plain,
( ~ empty_carrier(sK26_skl)
& one_sorted_str(sK26_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f50]) ).
fof(f257,plain,
one_sorted_str(sK26_skl),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f258,plain,
~ empty_carrier(sK26_skl),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f261,plain,
! [A,B] :
( closed_subset(topstr_closure(A,B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f262,plain,
! [X0,X1] :
( closed_subset(topstr_closure(X0,X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f263,plain,
! [A] :
( ? [B] :
( strict_net_str(B,A)
& net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f264,plain,
! [A] :
( ( strict_net_str(sK27_skl(A),A)
& net_str(sK27_skl(A),A) )
| ~ one_sorted_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(B,sK27_skl(A))],[f263]) ).
fof(f265,plain,
! [X0] :
( net_str(sK27_skl(X0),X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f289,plain,
! [A,B,C] :
( relation_rng_as_subset(A,B,C) = relation_rng(C)
| ~ relation_of2(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f290,plain,
! [X0,X1,X2] :
( relation_rng_as_subset(X1,X2,X0) = relation_rng(X0)
| ~ relation_of2(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f291,plain,
! [A,B,C] :
( subnetstr_of_element(A,B,C) = netstr_restr_to_element(A,B,C)
| ~ element(C,the_carrier(B))
| ~ net_str(B,A)
| ~ directed_relstr(B)
| ~ transitive_relstr(B)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f292,plain,
! [X0,X1,X2] :
( subnetstr_of_element(X0,X1,X2) = netstr_restr_to_element(X0,X1,X2)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f295,plain,
! [A,B] :
( element(topstr_closure(A,B),powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f296,plain,
! [X0,X1] :
( element(topstr_closure(X0,X1),powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f300,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f301,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f302,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f65]) ).
fof(f303,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f304,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(f305,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)],[f304]) ).
fof(f310,plain,
! [A,B] :
( A = B
| ? [C] :
( in(C,A)
<~> in(C,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f311,plain,
! [A,B] :
( A = B
| ? [C] :
( ( ~ in(C,B)
| ~ in(C,A) )
& ( in(C,B)
| in(C,A) ) ) ),
inference(NNF_transformation,[status(thm)],[f310]) ).
fof(f312,plain,
! [A,B] :
( A = B
| ( ( ~ in(sK29_skl(B,A),B)
| ~ in(sK29_skl(B,A),A) )
& ( in(sK29_skl(B,A),B)
| in(sK29_skl(B,A),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(C,sK29_skl(B,A))],[f311]) ).
fof(f313,plain,
! [X0,X1] :
( X1 = X0
| in(sK29_skl(X0,X1),X0)
| in(sK29_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f314,plain,
! [X0,X1] :
( X1 = X0
| ~ in(sK29_skl(X0,X1),X0)
| ~ in(sK29_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f315,plain,
! [X0] :
( sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,X0)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,X0))))
| ~ element(X0,the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,X0)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,X0))),sK0_skl,sK1_skl)
| ~ in(X0,the_carrier(sK1_skl))
| in(X0,sK2_skl) ),
inference(destructive_equality_resolution,[status(thm)],[f88]) ).
fof(f316,plain,
! [X0] :
( sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,X0)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,X0))))
| ~ element(X0,the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,X0)),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,X0))),sK0_skl,sK1_skl)
| ~ in(X0,the_carrier(sK1_skl))
| in(X0,sK3_skl) ),
inference(destructive_equality_resolution,[status(thm)],[f95]) ).
fof(f318,plain,
! [X0,X1,X2] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_rng_as_subset(X0,X1,X2) = relation_rng(X2) ),
inference(resolution,[status(thm)],[f290,f241]) ).
fof(f320,plain,
! [X0] :
( relation_rng_as_subset(the_carrier(X0),the_carrier(X0),the_InternalRel(X0)) = relation_rng(the_InternalRel(X0))
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f186,f318]) ).
fof(f321,plain,
! [X0] :
( empty(X0)
| ~ nowhere_dense(X0,sK0_skl)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f158,f76]) ).
fof(f322,definition,
( sQ0_spl
<=> top_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f324,plain,
( sQ0_spl
| ~ top_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f325,definition,
! [X0] :
( sQ1_spl
<=> ( empty(X0)
| ~ nowhere_dense(X0,sK0_skl)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f326,plain,
! [X0] :
( ~ sQ1_spl
| empty(X0)
| ~ nowhere_dense(X0,sK0_skl)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f328,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f321,f322,f325]) ).
fof(f329,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f324,f77]) ).
fof(f330,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f329]) ).
fof(f331,plain,
( ~ sQ1_spl
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty(sK10_skl(sK0_skl))
| ~ open_subset(sK10_skl(sK0_skl),sK0_skl)
| ~ element(sK10_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f326,f119]) ).
fof(f332,plain,
! [X0] :
( ~ sQ1_spl
| ~ boundary_set(X0,sK0_skl)
| ~ closed_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| empty(X0)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f326,f156]) ).
fof(f333,definition,
( sQ2_spl
<=> element(sK10_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f335,plain,
( sQ2_spl
| ~ element(sK10_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f336,definition,
( sQ3_spl
<=> open_subset(sK10_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f338,plain,
( sQ3_spl
| ~ open_subset(sK10_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f336]) ).
fof(f339,definition,
( sQ4_spl
<=> empty(sK10_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f342,definition,
( sQ5_spl
<=> topological_space(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f344,plain,
( sQ5_spl
| ~ topological_space(sK0_skl) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ5_spl
| sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f331,f333,f336,f339,f342,f322,f325]) ).
fof(f346,definition,
! [X0] :
( sQ6_spl
<=> ( ~ boundary_set(X0,sK0_skl)
| ~ closed_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| empty(X0)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f347,plain,
! [X0] :
( ~ sQ6_spl
| ~ boundary_set(X0,sK0_skl)
| ~ closed_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| empty(X0)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f346]) ).
fof(f349,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ5_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f332,f346,f342,f322,f325]) ).
fof(f350,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f344,f76]) ).
fof(f351,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f350]) ).
fof(f352,plain,
! [X0] :
( ~ sQ6_spl
| ~ boundary_set(X0,sK0_skl)
| ~ closed_subset(X0,sK0_skl)
| empty(X0)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f347]) ).
fof(f355,plain,
! [X0] :
( ~ sQ6_spl
| ~ nowhere_dense(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| ~ closed_subset(X0,sK0_skl)
| empty(X0)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f352,f153]) ).
fof(f360,definition,
( sQ8_spl
<=> element(sK9_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( sQ8_spl
| ~ element(sK9_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f360]) ).
fof(f363,definition,
( sQ9_spl
<=> open_subset(sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( sQ9_spl
| ~ open_subset(sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f366,definition,
( sQ10_spl
<=> empty(sK9_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( sQ10_spl
| ~ empty(sK9_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f366]) ).
fof(f369,definition,
( sQ11_spl
<=> closed_subset(sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f371,plain,
( sQ11_spl
| ~ closed_subset(sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f373,definition,
! [X0] :
( sQ12_spl
<=> ( ~ nowhere_dense(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ closed_subset(X0,sK0_skl)
| empty(X0)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f376,plain,
( ~ sQ6_spl
| ~ sQ0_spl
| ~ sQ5_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f355,f373,f342,f322,f346]) ).
fof(f378,plain,
( sQ3_spl
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f338,f111]) ).
fof(f379,plain,
( sQ3_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f378,f342,f322,f336]) ).
fof(f380,plain,
( sQ2_spl
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f335,f109]) ).
fof(f382,plain,
( sQ2_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f380,f342,f322,f333]) ).
fof(f383,definition,
( sQ13_spl
<=> empty_carrier(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f384,plain,
( ~ sQ13_spl
| empty_carrier(sK0_skl) ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f386,definition,
( sQ14_spl
<=> one_sorted_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( ~ sQ14_spl
| one_sorted_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f388,plain,
( sQ14_spl
| ~ one_sorted_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f393,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f384,f75]) ).
fof(f394,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f393]) ).
fof(f395,plain,
( sQ14_spl
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f388,f301]) ).
fof(f397,plain,
( sQ14_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f395,f322,f386]) ).
fof(f398,plain,
! [X0] :
( closed_subset(X0,sK0_skl)
| ~ nowhere_dense(X0,sK0_skl)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f160,f76]) ).
fof(f399,definition,
! [X0] :
( sQ16_spl
<=> ( closed_subset(X0,sK0_skl)
| ~ nowhere_dense(X0,sK0_skl)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f400,plain,
! [X0] :
( ~ sQ16_spl
| closed_subset(X0,sK0_skl)
| ~ nowhere_dense(X0,sK0_skl)
| ~ open_subset(X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f399]) ).
fof(f402,plain,
( sQ16_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f398,f322,f399]) ).
fof(f403,plain,
( sQ11_spl
| ~ sQ16_spl
| ~ nowhere_dense(sK9_skl(sK0_skl),sK0_skl)
| ~ open_subset(sK9_skl(sK0_skl),sK0_skl)
| ~ element(sK9_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f400,f371]) ).
fof(f404,definition,
( sQ17_spl
<=> nowhere_dense(sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ17_spl
| ~ nowhere_dense(sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,plain,
( sQ11_spl
| ~ sQ16_spl
| ~ sQ17_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f403,f360,f363,f404,f399,f369]) ).
fof(f412,plain,
! [X0] :
( sK5_skl(sK29_skl(X0,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(X0,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(X0,sK2_skl)))))
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(resolution,[status(thm)],[f313,f87]) ).
fof(f413,plain,
! [X0] :
( sK29_skl(X0,sK2_skl) = sK6_skl(sK29_skl(X0,sK2_skl))
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(resolution,[status(thm)],[f313,f86]) ).
fof(f414,plain,
! [X0] :
( sK4_skl = topstr_closure(sK0_skl,sK5_skl(sK29_skl(X0,sK2_skl)))
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(resolution,[status(thm)],[f313,f85]) ).
fof(f427,definition,
( sQ19_spl
<=> element(sK4_skl,powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f431,definition,
( sQ20_spl
<=> closed_subset(sK4_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f473,definition,
( sQ27_spl
<=> sK3_skl = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( ~ sQ27_spl
| sK3_skl = sK2_skl ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f495,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f96]) ).
fof(f496,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f495]) ).
fof(f512,plain,
( sQ8_spl
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f362,f99]) ).
fof(f514,plain,
( sQ8_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f512,f322,f360]) ).
fof(f519,plain,
! [X0] :
( sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0)
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(X0,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(X0,sK2_skl))))))
| ~ element(sK6_skl(sK29_skl(X0,sK2_skl)),the_carrier(sK1_skl))
| ~ netstr_induced_subset(sK5_skl(sK29_skl(X0,sK2_skl)),sK0_skl,sK1_skl)
| ~ in(sK6_skl(sK29_skl(X0,sK2_skl)),the_carrier(sK1_skl))
| in(sK6_skl(sK29_skl(X0,sK2_skl)),sK3_skl) ),
inference(paramodulation,[status(thm)],[f412,f316]) ).
fof(f524,plain,
( sK4_skl = topstr_closure(sK0_skl,sK7_skl(sK29_skl(sK3_skl,sK2_skl)))
| sK29_skl(sK3_skl,sK2_skl) = sK6_skl(sK29_skl(sK3_skl,sK2_skl))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f413,f92]) ).
fof(f525,plain,
( in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| sK29_skl(sK3_skl,sK2_skl) = sK6_skl(sK29_skl(sK3_skl,sK2_skl))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f413,f89]) ).
fof(f532,definition,
( sQ37_spl
<=> sK2_skl = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f542,definition,
( sQ40_spl
<=> sK29_skl(sK3_skl,sK2_skl) = sK6_skl(sK29_skl(sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( ~ sQ40_spl
| sK29_skl(sK3_skl,sK2_skl) = sK6_skl(sK29_skl(sK3_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,definition,
( sQ41_spl
<=> sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f549,definition,
( sQ42_spl
<=> sK4_skl = topstr_closure(sK0_skl,sK7_skl(sK29_skl(sK3_skl,sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( ~ sQ42_spl
| sK4_skl = topstr_closure(sK0_skl,sK7_skl(sK29_skl(sK3_skl,sK2_skl))) ),
inference(component_clause,[status(thm)],[f549]) ).
fof(f552,plain,
( sQ42_spl
| sQ40_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f524,f473,f542,f549]) ).
fof(f553,definition,
( sQ43_spl
<=> in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ43_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,plain,
( sQ43_spl
| sQ40_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f525,f473,f542,f553]) ).
fof(f557,definition,
( sQ44_spl
<=> sK29_skl(sK3_skl,sK2_skl) = sK8_skl(sK29_skl(sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f620,plain,
! [X0] :
( sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0)
| element(sK4_skl,powerset(the_carrier(sK0_skl)))
| ~ element(sK5_skl(sK29_skl(X0,sK2_skl)),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(paramodulation,[status(thm)],[f414,f296]) ).
fof(f621,plain,
! [X0] :
( sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0)
| closed_subset(sK4_skl,sK0_skl)
| ~ element(sK5_skl(sK29_skl(X0,sK2_skl)),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f414,f262]) ).
fof(f622,definition,
! [X0] :
( sQ53_spl
<=> ( sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0)
| ~ element(sK5_skl(sK29_skl(X0,sK2_skl)),powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f623,plain,
! [X0] :
( ~ sQ53_spl
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0)
| ~ element(sK5_skl(sK29_skl(X0,sK2_skl)),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f622]) ).
fof(f625,plain,
( sQ19_spl
| sQ53_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f620,f322,f622,f427]) ).
fof(f626,plain,
( sQ20_spl
| sQ53_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f621,f342,f322,f622,f431]) ).
fof(f680,plain,
( ~ sQ40_spl
| sK5_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))))
| sK2_skl = sK3_skl
| in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(paramodulation,[status(thm)],[f543,f412]) ).
fof(f681,plain,
( ~ sQ40_spl
| element(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(paramodulation,[status(thm)],[f543,f84]) ).
fof(f682,definition,
( sQ59_spl
<=> in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f683,plain,
( ~ sQ59_spl
| in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f684,plain,
( sQ59_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f689,definition,
( sQ61_spl
<=> sK5_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( ~ sQ61_spl
| sK5_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl))))) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,plain,
( ~ sQ40_spl
| sQ61_spl
| sQ27_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f680,f682,f473,f689,f542]) ).
fof(f693,definition,
( sQ62_spl
<=> in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f694,plain,
( ~ sQ62_spl
| in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f695,plain,
( sQ62_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f696,definition,
( sQ63_spl
<=> element(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f697,plain,
( ~ sQ63_spl
| element(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
inference(component_clause,[status(thm)],[f696]) ).
fof(f699,plain,
( ~ sQ40_spl
| sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f681,f693,f696,f542]) ).
fof(f700,plain,
( ~ sQ61_spl
| ~ sQ40_spl
| sK5_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))) ),
inference(forward_demodulation,[status(thm)],[f543,f690]) ).
fof(f704,plain,
( ~ sQ59_spl
| sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))))) ),
inference(resolution,[status(thm)],[f683,f94]) ).
fof(f705,plain,
( ~ sQ59_spl
| sK4_skl = topstr_closure(sK0_skl,sK7_skl(sK29_skl(sK3_skl,sK2_skl))) ),
inference(resolution,[status(thm)],[f683,f92]) ).
fof(f707,plain,
( ~ sQ59_spl
| sK29_skl(sK3_skl,sK2_skl) = sK8_skl(sK29_skl(sK3_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f683,f93]) ).
fof(f711,plain,
( sQ62_spl
| sK2_skl = sK3_skl
| in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f695,f313]) ).
fof(f712,plain,
( sQ62_spl
| sQ27_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f711,f682,f473,f693]) ).
fof(f713,plain,
! [X0] :
( open_subset(X0,sK0_skl)
| ~ empty(X0)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f212,f76]) ).
fof(f714,definition,
! [X0] :
( sQ64_spl
<=> ( open_subset(X0,sK0_skl)
| ~ empty(X0)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f715,plain,
! [X0] :
( ~ sQ64_spl
| open_subset(X0,sK0_skl)
| ~ empty(X0)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,plain,
( sQ64_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f713,f322,f714]) ).
fof(f733,plain,
( sQ9_spl
| ~ sQ64_spl
| ~ empty(sK9_skl(sK0_skl))
| ~ element(sK9_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f715,f365]) ).
fof(f734,plain,
( sQ9_spl
| ~ sQ64_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f733,f360,f366,f714,f363]) ).
fof(f736,definition,
( sQ68_spl
<=> boundary_set(sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f738,plain,
( sQ68_spl
| ~ boundary_set(sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f736]) ).
fof(f740,plain,
( sQ68_spl
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f738,f106]) ).
fof(f743,plain,
( sQ68_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f740,f322,f736]) ).
fof(f751,plain,
( sQ10_spl
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f368,f100]) ).
fof(f752,plain,
( sQ10_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f751,f322,f366]) ).
fof(f757,plain,
! [X0] :
( nowhere_dense(X0,sK0_skl)
| ~ empty(X0)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f217,f76]) ).
fof(f758,definition,
! [X0] :
( sQ70_spl
<=> ( nowhere_dense(X0,sK0_skl)
| ~ empty(X0)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f759,plain,
! [X0] :
( ~ sQ70_spl
| nowhere_dense(X0,sK0_skl)
| ~ empty(X0)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f758]) ).
fof(f761,plain,
( sQ70_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f757,f322,f758]) ).
fof(f766,plain,
( sQ17_spl
| ~ sQ70_spl
| ~ empty(sK9_skl(sK0_skl))
| ~ element(sK9_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f759,f406]) ).
fof(f768,plain,
( sQ17_spl
| ~ sQ70_spl
| ~ sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f766,f360,f366,f758,f404]) ).
fof(f773,plain,
( ~ sQ59_spl
| sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))))) ),
inference(forward_demodulation,[status(thm)],[f707,f704]) ).
fof(f774,plain,
( ~ sQ59_spl
| sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))) ),
inference(forward_demodulation,[status(thm)],[f707,f773]) ).
fof(f780,plain,
( ~ sQ40_spl
| sK2_skl = sK3_skl
| in(sK29_skl(sK3_skl,sK2_skl),sK3_skl)
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl))))))
| ~ element(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),the_carrier(sK1_skl))
| ~ netstr_induced_subset(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,sK1_skl)
| ~ in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| in(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),sK3_skl) ),
inference(paramodulation,[status(thm)],[f543,f519]) ).
fof(f781,definition,
( sQ71_spl
<=> in(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( ~ sQ71_spl
| in(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),sK3_skl) ),
inference(component_clause,[status(thm)],[f781]) ).
fof(f784,definition,
( sQ72_spl
<=> netstr_induced_subset(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f786,plain,
( sQ72_spl
| ~ netstr_induced_subset(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f784]) ).
fof(f787,definition,
( sQ73_spl
<=> element(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),the_carrier(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( sQ73_spl
| ~ element(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),the_carrier(sK1_skl)) ),
inference(component_clause,[status(thm)],[f787]) ).
fof(f790,definition,
( sQ74_spl
<=> sK4_skl = topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f792,plain,
( sQ74_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))))) ),
inference(component_clause,[status(thm)],[f790]) ).
fof(f793,plain,
( ~ sQ40_spl
| sQ27_spl
| sQ59_spl
| ~ sQ74_spl
| ~ sQ73_spl
| ~ sQ72_spl
| ~ sQ43_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f780,f781,f553,f784,f787,f790,f682,f473,f542]) ).
fof(f794,plain,
( sQ74_spl
| ~ sQ40_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK6_skl(sK29_skl(sK3_skl,sK2_skl)))))) ),
inference(forward_demodulation,[status(thm)],[f543,f792]) ).
fof(f795,plain,
( sQ74_spl
| ~ sQ40_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))))) ),
inference(forward_demodulation,[status(thm)],[f543,f794]) ).
fof(f800,plain,
( sQ73_spl
| ~ sQ40_spl
| ~ element(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f543,f789]) ).
fof(f801,plain,
( sQ73_spl
| ~ sQ40_spl
| ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f800,f697]) ).
fof(f802,plain,
( sQ73_spl
| ~ sQ40_spl
| ~ sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f801]) ).
fof(f804,plain,
( ~ sQ71_spl
| ~ sQ40_spl
| in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f543,f782]) ).
fof(f805,plain,
( ~ sQ59_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f705,f549,f682]) ).
fof(f811,definition,
( sQ75_spl
<=> in(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f812,plain,
( ~ sQ75_spl
| in(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),sK2_skl) ),
inference(component_clause,[status(thm)],[f811]) ).
fof(f813,plain,
( sQ75_spl
| ~ in(sK6_skl(sK29_skl(sK3_skl,sK2_skl)),sK2_skl) ),
inference(component_clause,[status(thm)],[f811]) ).
fof(f815,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f543,f812]) ).
fof(f819,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| sK4_skl = topstr_closure(sK0_skl,sK5_skl(sK29_skl(sK3_skl,sK2_skl))) ),
inference(resolution,[status(thm)],[f815,f85]) ).
fof(f820,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
inference(resolution,[status(thm)],[f815,f82]) ).
fof(f827,plain,
( sQ75_spl
| ~ sQ40_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f543,f813]) ).
fof(f828,plain,
( sQ75_spl
| ~ sQ40_spl
| sK2_skl = sK3_skl
| in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f827,f313]) ).
fof(f829,plain,
( sQ75_spl
| ~ sQ40_spl
| sQ27_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f828,f682,f473,f542,f811]) ).
fof(f852,plain,
! [X0,X1,X2] :
( netstr_restr_to_element(X0,X1,X2) = net_str_of(X0,the_carrier(netstr_restr_to_element(X0,X1,X2)),the_InternalRel(netstr_restr_to_element(X0,X1,X2)),the_mapping(X0,netstr_restr_to_element(X0,X1,X2)))
| ~ net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ one_sorted_str(X0)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(resolution,[status(thm)],[f244,f238]) ).
fof(f853,plain,
! [X0,X1,X2] :
( netstr_restr_to_element(X0,X1,X2) = net_str_of(X0,the_carrier(netstr_restr_to_element(X0,X1,X2)),the_InternalRel(netstr_restr_to_element(X0,X1,X2)),the_mapping(X0,netstr_restr_to_element(X0,X1,X2)))
| ~ net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f852]) ).
fof(f854,plain,
! [X0,X1,X2] :
( netstr_restr_to_element(X0,X1,X2) = net_str_of(X0,the_carrier(netstr_restr_to_element(X0,X1,X2)),the_InternalRel(netstr_restr_to_element(X0,X1,X2)),the_mapping(X0,netstr_restr_to_element(X0,X1,X2)))
| ~ element(X2,the_carrier(X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f853,f245]) ).
fof(f865,plain,
( ~ sQ59_spl
| element(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(paramodulation,[status(thm)],[f707,f91]) ).
fof(f866,plain,
( sQ63_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f865,f682,f696]) ).
fof(f872,plain,
( ~ sQ42_spl
| element(sK4_skl,powerset(the_carrier(sK0_skl)))
| ~ element(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(paramodulation,[status(thm)],[f550,f296]) ).
fof(f873,plain,
( ~ sQ42_spl
| closed_subset(sK4_skl,sK0_skl)
| ~ element(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f550,f262]) ).
fof(f874,definition,
( sQ77_spl
<=> element(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f876,plain,
( sQ77_spl
| ~ element(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f874]) ).
fof(f877,plain,
( ~ sQ42_spl
| sQ19_spl
| ~ sQ77_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f872,f322,f874,f427,f549]) ).
fof(f878,plain,
( ~ sQ42_spl
| sQ20_spl
| ~ sQ77_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f873,f342,f322,f874,f431,f549]) ).
fof(f879,plain,
! [X0,X1] :
( ~ sQ53_spl
| ~ netstr_induced_subset(sK5_skl(sK29_skl(X0,sK2_skl)),sK0_skl,X1)
| ~ net_str(X1,sK0_skl)
| empty_carrier(X1)
| ~ one_sorted_str(sK0_skl)
| empty_carrier(sK0_skl)
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(resolution,[status(thm)],[f623,f305]) ).
fof(f880,definition,
! [X0,X1] :
( sQ78_spl
<=> ( ~ netstr_induced_subset(sK5_skl(sK29_skl(X0,sK2_skl)),sK0_skl,X1)
| ~ net_str(X1,sK0_skl)
| empty_carrier(X1)
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f881,plain,
! [X0,X1] :
( ~ sQ78_spl
| ~ netstr_induced_subset(sK5_skl(sK29_skl(X0,sK2_skl)),sK0_skl,X1)
| ~ net_str(X1,sK0_skl)
| empty_carrier(X1)
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(component_clause,[status(thm)],[f880]) ).
fof(f883,plain,
( ~ sQ53_spl
| ~ sQ14_spl
| sQ13_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f879,f880,f383,f386,f622]) ).
fof(f971,definition,
( sQ91_spl
<=> empty_carrier(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f972,plain,
( ~ sQ91_spl
| empty_carrier(sK1_skl) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,definition,
( sQ92_spl
<=> net_str(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f976,plain,
( sQ92_spl
| ~ net_str(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f974]) ).
fof(f978,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f976,f81]) ).
fof(f979,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f978]) ).
fof(f980,plain,
( ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f972,f78]) ).
fof(f981,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f980]) ).
fof(f1008,plain,
! [X0] :
( sQ77_spl
| ~ netstr_induced_subset(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,X0)
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0)
| ~ one_sorted_str(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f876,f305]) ).
fof(f1009,definition,
! [X0] :
( sQ93_spl
<=> ( ~ netstr_induced_subset(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,X0)
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1010,plain,
! [X0] :
( ~ sQ93_spl
| ~ netstr_induced_subset(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,X0)
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0) ),
inference(component_clause,[status(thm)],[f1009]) ).
fof(f1012,plain,
( sQ77_spl
| sQ93_spl
| ~ sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f1008,f383,f386,f1009,f874]) ).
fof(f1035,plain,
( ~ sQ93_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK3_skl)
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl) ),
inference(resolution,[status(thm)],[f1010,f90]) ).
fof(f1037,plain,
( ~ sQ93_spl
| ~ sQ59_spl
| ~ sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1035,f971,f974,f682,f1009]) ).
fof(f1040,plain,
( sQ59_spl
| sK29_skl(sK3_skl,sK2_skl) = sK6_skl(sK29_skl(sK3_skl,sK2_skl))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f684,f413]) ).
fof(f1041,plain,
( sQ59_spl
| sQ40_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1040,f473,f542,f682]) ).
fof(f1045,plain,
( ~ sQ71_spl
| ~ sQ40_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f804,f682,f542,f781]) ).
fof(f1061,plain,
( sQ43_spl
| ~ sQ75_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f820]) ).
fof(f1062,plain,
( sQ43_spl
| ~ sQ75_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f1061]) ).
fof(f1064,plain,
( ~ sQ62_spl
| sK2_skl = sK3_skl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f694,f314]) ).
fof(f1070,plain,
( ~ sQ62_spl
| sQ27_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1064,f682,f473,f693]) ).
fof(f1102,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| element(sK4_skl,powerset(the_carrier(sK0_skl)))
| ~ element(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(paramodulation,[status(thm)],[f819,f296]) ).
fof(f1103,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| closed_subset(sK4_skl,sK0_skl)
| ~ element(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f819,f262]) ).
fof(f1109,definition,
( sQ95_spl
<=> element(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1111,plain,
( sQ95_spl
| ~ element(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1112,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| sQ19_spl
| ~ sQ95_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1102,f322,f1109,f427,f542,f811]) ).
fof(f1113,plain,
( ~ sQ75_spl
| ~ sQ40_spl
| sQ20_spl
| ~ sQ95_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1103,f342,f322,f1109,f431,f542,f811]) ).
fof(f1120,plain,
( sQ72_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(resolution,[status(thm)],[f786,f83]) ).
fof(f1121,plain,
( sQ72_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f1120,f693,f784]) ).
fof(f1122,plain,
( sQ74_spl
| ~ sQ40_spl
| ~ sQ61_spl
| sK4_skl != topstr_closure(sK0_skl,sK5_skl(sK29_skl(sK3_skl,sK2_skl))) ),
inference(forward_demodulation,[status(thm)],[f700,f795]) ).
fof(f1123,plain,
( sQ74_spl
| ~ sQ40_spl
| ~ sQ61_spl
| ~ sQ75_spl
| sK4_skl != sK4_skl ),
inference(forward_demodulation,[status(thm)],[f819,f1122]) ).
fof(f1124,plain,
( sQ74_spl
| ~ sQ40_spl
| ~ sQ61_spl
| ~ sQ75_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1123]) ).
fof(f1125,plain,
( sQ74_spl
| ~ sQ40_spl
| ~ sQ61_spl
| ~ sQ75_spl ),
inference(contradiction_clause,[status(thm)],[f1124]) ).
fof(f1132,plain,
( ~ sQ59_spl
| in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl)) ),
inference(resolution,[status(thm)],[f683,f89]) ).
fof(f1149,plain,
! [X0] :
( sQ95_spl
| ~ netstr_induced_subset(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,X0)
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0)
| ~ one_sorted_str(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f1111,f305]) ).
fof(f1154,definition,
! [X0] :
( sQ97_spl
<=> ( ~ netstr_induced_subset(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,X0)
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1155,plain,
! [X0] :
( ~ sQ97_spl
| ~ netstr_induced_subset(sK5_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,X0)
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0) ),
inference(component_clause,[status(thm)],[f1154]) ).
fof(f1157,plain,
( sQ95_spl
| sQ97_spl
| ~ sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f1149,f383,f386,f1154,f1109]) ).
fof(f1158,plain,
( ~ sQ97_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK2_skl)
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl) ),
inference(resolution,[status(thm)],[f1155,f83]) ).
fof(f1159,plain,
( ~ sQ97_spl
| ~ sQ62_spl
| ~ sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1158,f971,f974,f693,f1154]) ).
fof(f1162,plain,
! [X0] :
( ~ sQ78_spl
| ~ in(sK29_skl(X0,sK2_skl),sK2_skl)
| ~ net_str(sK1_skl,sK0_skl)
| empty_carrier(sK1_skl)
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(resolution,[status(thm)],[f881,f83]) ).
fof(f1163,definition,
! [X0] :
( sQ98_spl
<=> ( ~ in(sK29_skl(X0,sK2_skl),sK2_skl)
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1164,plain,
! [X0] :
( ~ sQ98_spl
| ~ in(sK29_skl(X0,sK2_skl),sK2_skl)
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0) ),
inference(component_clause,[status(thm)],[f1163]) ).
fof(f1166,plain,
( ~ sQ78_spl
| ~ sQ92_spl
| sQ91_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1162,f1163,f971,f974,f880]) ).
fof(f1167,plain,
! [X0] :
( ~ sQ98_spl
| ~ in(sK29_skl(X0,sK2_skl),sK2_skl)
| sK2_skl = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1164,f314]) ).
fof(f1169,plain,
! [X0] :
( ~ sQ98_spl
| sK2_skl = X0
| in(sK29_skl(X0,sK2_skl),X0)
| sK2_skl = X0 ),
inference(resolution,[status(thm)],[f1167,f313]) ).
fof(f1171,plain,
! [X0] :
( ~ sQ98_spl
| in(sK29_skl(X0,sK2_skl),X0)
| sK2_skl = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f1169]) ).
fof(f1173,plain,
( ~ sQ98_spl
| sK2_skl = sK2_skl
| sK2_skl = sK2_skl ),
inference(resolution,[status(thm)],[f1171,f1167]) ).
fof(f1175,plain,
( ~ sQ98_spl
| sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl)))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl)))))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f1171,f94]) ).
fof(f1176,plain,
( ~ sQ98_spl
| sK4_skl = topstr_closure(sK0_skl,sK7_skl(sK29_skl(sK3_skl,sK2_skl)))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f1171,f92]) ).
fof(f1177,plain,
( ~ sQ98_spl
| in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f1171,f89]) ).
fof(f1178,plain,
( ~ sQ98_spl
| sK29_skl(sK3_skl,sK2_skl) = sK8_skl(sK29_skl(sK3_skl,sK2_skl))
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f1171,f93]) ).
fof(f1184,plain,
( ~ sQ98_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1173,f532,f1163]) ).
fof(f1186,plain,
( ~ sQ98_spl
| sQ41_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1175,f473,f545,f1163]) ).
fof(f1187,plain,
( ~ sQ98_spl
| sQ42_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1176,f473,f549,f1163]) ).
fof(f1188,plain,
( ~ sQ98_spl
| sQ43_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1177,f473,f553,f1163]) ).
fof(f1189,plain,
( ~ sQ98_spl
| sQ44_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1178,f473,f557,f1163]) ).
fof(f1195,plain,
! [X0,X1] :
( ~ net_str(X0,X1)
| ~ one_sorted_str(X1)
| relation_rng_as_subset(the_carrier(X0),the_carrier(X0),the_InternalRel(X0)) = relation_rng(the_InternalRel(X0)) ),
inference(resolution,[status(thm)],[f320,f303]) ).
fof(f1197,plain,
! [X0] :
( ~ net_str(X0,sK26_skl)
| relation_rng_as_subset(the_carrier(X0),the_carrier(X0),the_InternalRel(X0)) = relation_rng(the_InternalRel(X0)) ),
inference(resolution,[status(thm)],[f1195,f257]) ).
fof(f1202,plain,
! [X0,X1] :
( subnetstr_of_element(X0,sK1_skl,X1) = netstr_restr_to_element(X0,sK1_skl,X1)
| ~ element(X1,the_carrier(sK1_skl))
| ~ net_str(sK1_skl,X0)
| ~ directed_relstr(sK1_skl)
| empty_carrier(sK1_skl)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(resolution,[status(thm)],[f292,f79]) ).
fof(f1210,definition,
! [X0,X1] :
( sQ99_spl
<=> ( subnetstr_of_element(X0,sK1_skl,X1) = netstr_restr_to_element(X0,sK1_skl,X1)
| ~ element(X1,the_carrier(sK1_skl))
| ~ net_str(sK1_skl,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1211,plain,
! [X0,X1] :
( ~ sQ99_spl
| subnetstr_of_element(X0,sK1_skl,X1) = netstr_restr_to_element(X0,sK1_skl,X1)
| ~ element(X1,the_carrier(sK1_skl))
| ~ net_str(sK1_skl,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(component_clause,[status(thm)],[f1210]) ).
fof(f1213,definition,
( sQ100_spl
<=> directed_relstr(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
( sQ100_spl
| ~ directed_relstr(sK1_skl) ),
inference(component_clause,[status(thm)],[f1213]) ).
fof(f1216,plain,
( ~ sQ100_spl
| sQ91_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f1202,f1210,f971,f1213]) ).
fof(f1220,definition,
( sQ101_spl
<=> transitive_relstr(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
( sQ101_spl
| ~ transitive_relstr(sK1_skl) ),
inference(component_clause,[status(thm)],[f1220]) ).
fof(f1225,plain,
( sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1222,f79]) ).
fof(f1226,plain,
sQ101_spl,
inference(contradiction_clause,[status(thm)],[f1225]) ).
fof(f1227,plain,
( sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1215,f80]) ).
fof(f1228,plain,
sQ100_spl,
inference(contradiction_clause,[status(thm)],[f1227]) ).
fof(f1231,plain,
! [X0] :
( ~ sQ99_spl
| subnetstr_of_element(sK0_skl,sK1_skl,X0) = netstr_restr_to_element(sK0_skl,sK1_skl,X0)
| ~ element(X0,the_carrier(sK1_skl))
| ~ one_sorted_str(sK0_skl)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f1211,f81]) ).
fof(f1233,definition,
! [X0] :
( sQ102_spl
<=> ( subnetstr_of_element(sK0_skl,sK1_skl,X0) = netstr_restr_to_element(sK0_skl,sK1_skl,X0)
| ~ element(X0,the_carrier(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1234,plain,
! [X0] :
( ~ sQ102_spl
| subnetstr_of_element(sK0_skl,sK1_skl,X0) = netstr_restr_to_element(sK0_skl,sK1_skl,X0)
| ~ element(X0,the_carrier(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1233]) ).
fof(f1236,plain,
( ~ sQ99_spl
| sQ102_spl
| ~ sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f1231,f383,f386,f1233,f1210]) ).
fof(f1240,plain,
( ~ sQ63_spl
| ~ sQ102_spl
| subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)) = netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f1234,f697]) ).
fof(f1242,plain,
! [X0] :
( ~ sQ102_spl
| ~ in(X0,sK3_skl)
| subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(X0)) = netstr_restr_to_element(sK0_skl,sK1_skl,sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f1234,f91]) ).
fof(f1246,plain,
( ~ sQ59_spl
| ~ sQ63_spl
| ~ sQ102_spl
| sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))) ),
inference(backward_demodulation,[status(thm)],[f1240,f774]) ).
fof(f1250,plain,
( ~ sQ59_spl
| ~ sQ63_spl
| ~ sQ102_spl
| sK7_skl(sK29_skl(sK3_skl,sK2_skl)) = relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))) ),
inference(forward_demodulation,[status(thm)],[f1240,f1246]) ).
fof(f1254,plain,
( ~ sQ98_spl
| ~ sQ102_spl
| sK2_skl = sK3_skl
| subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))) = netstr_restr_to_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))) ),
inference(resolution,[status(thm)],[f1242,f1171]) ).
fof(f1259,definition,
( sQ103_spl
<=> subnetstr_of_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))) = netstr_restr_to_element(sK0_skl,sK1_skl,sK8_skl(sK29_skl(sK3_skl,sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1262,plain,
( ~ sQ98_spl
| ~ sQ102_spl
| sQ27_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1254,f1259,f473,f1233,f1163]) ).
fof(f1318,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| ~ net_str(X0,sK26_skl)
| empty_carrier(X0)
| ~ one_sorted_str(sK26_skl)
| empty_carrier(sK26_skl)
| relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK26_skl,X0,X1)),the_carrier(netstr_restr_to_element(sK26_skl,X0,X1)),the_InternalRel(netstr_restr_to_element(sK26_skl,X0,X1))) = relation_rng(the_InternalRel(netstr_restr_to_element(sK26_skl,X0,X1))) ),
inference(resolution,[status(thm)],[f1197,f245]) ).
fof(f1319,plain,
! [X0,X1,X2] :
( ~ relation_of2(X2,X0,the_carrier(sK26_skl))
| ~ quasi_total(X2,X0,the_carrier(sK26_skl))
| ~ function(X2)
| ~ relation_of2(X1,X0,X0)
| ~ one_sorted_str(sK26_skl)
| relation_rng_as_subset(the_carrier(net_str_of(sK26_skl,X0,X1,X2)),the_carrier(net_str_of(sK26_skl,X0,X1,X2)),the_InternalRel(net_str_of(sK26_skl,X0,X1,X2))) = relation_rng(the_InternalRel(net_str_of(sK26_skl,X0,X1,X2))) ),
inference(resolution,[status(thm)],[f1197,f184]) ).
fof(f1320,plain,
( ~ one_sorted_str(sK26_skl)
| relation_rng_as_subset(the_carrier(sK27_skl(sK26_skl)),the_carrier(sK27_skl(sK26_skl)),the_InternalRel(sK27_skl(sK26_skl))) = relation_rng(the_InternalRel(sK27_skl(sK26_skl))) ),
inference(resolution,[status(thm)],[f1197,f265]) ).
fof(f1321,plain,
! [X0,X1] :
( ~ subnet(X0,sK26_skl,X1)
| ~ net_str(X1,sK26_skl)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| ~ one_sorted_str(sK26_skl)
| empty_carrier(sK26_skl)
| relation_rng_as_subset(the_carrier(X0),the_carrier(X0),the_InternalRel(X0)) = relation_rng(the_InternalRel(X0)) ),
inference(resolution,[status(thm)],[f1197,f254]) ).
fof(f1322,definition,
! [X0,X1] :
( sQ105_spl
<=> ( ~ element(X1,the_carrier(X0))
| ~ net_str(X0,sK26_skl)
| empty_carrier(X0)
| relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK26_skl,X0,X1)),the_carrier(netstr_restr_to_element(sK26_skl,X0,X1)),the_InternalRel(netstr_restr_to_element(sK26_skl,X0,X1))) = relation_rng(the_InternalRel(netstr_restr_to_element(sK26_skl,X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1325,definition,
( sQ106_spl
<=> empty_carrier(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1326,plain,
( ~ sQ106_spl
| empty_carrier(sK26_skl) ),
inference(component_clause,[status(thm)],[f1325]) ).
fof(f1328,definition,
( sQ107_spl
<=> one_sorted_str(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1330,plain,
( sQ107_spl
| ~ one_sorted_str(sK26_skl) ),
inference(component_clause,[status(thm)],[f1328]) ).
fof(f1331,plain,
( ~ sQ107_spl
| sQ106_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1318,f1322,f1325,f1328]) ).
fof(f1332,definition,
! [X0,X1,X2] :
( sQ108_spl
<=> ( ~ relation_of2(X2,X0,the_carrier(sK26_skl))
| ~ quasi_total(X2,X0,the_carrier(sK26_skl))
| ~ function(X2)
| ~ relation_of2(X1,X0,X0)
| relation_rng_as_subset(the_carrier(net_str_of(sK26_skl,X0,X1,X2)),the_carrier(net_str_of(sK26_skl,X0,X1,X2)),the_InternalRel(net_str_of(sK26_skl,X0,X1,X2))) = relation_rng(the_InternalRel(net_str_of(sK26_skl,X0,X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1335,plain,
( ~ sQ107_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f1319,f1332,f1328]) ).
fof(f1336,definition,
( sQ109_spl
<=> relation_rng_as_subset(the_carrier(sK27_skl(sK26_skl)),the_carrier(sK27_skl(sK26_skl)),the_InternalRel(sK27_skl(sK26_skl))) = relation_rng(the_InternalRel(sK27_skl(sK26_skl))) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( ~ sQ107_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f1320,f1336,f1328]) ).
fof(f1340,definition,
! [X0,X1] :
( sQ110_spl
<=> ( ~ subnet(X0,sK26_skl,X1)
| ~ net_str(X1,sK26_skl)
| ~ directed_relstr(X1)
| ~ transitive_relstr(X1)
| empty_carrier(X1)
| relation_rng_as_subset(the_carrier(X0),the_carrier(X0),the_InternalRel(X0)) = relation_rng(the_InternalRel(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1343,plain,
( ~ sQ107_spl
| sQ106_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f1321,f1340,f1325,f1328]) ).
fof(f1344,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1330,f257]) ).
fof(f1345,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f1344]) ).
fof(f1346,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1326,f258]) ).
fof(f1347,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1346]) ).
fof(f1485,plain,
! [X0,X1] :
( ~ sQ14_spl
| netstr_restr_to_element(sK0_skl,X0,X1) = net_str_of(sK0_skl,the_carrier(netstr_restr_to_element(sK0_skl,X0,X1)),the_InternalRel(netstr_restr_to_element(sK0_skl,X0,X1)),the_mapping(sK0_skl,netstr_restr_to_element(sK0_skl,X0,X1)))
| ~ element(X1,the_carrier(X0))
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0)
| empty_carrier(sK0_skl) ),
inference(resolution,[status(thm)],[f854,f387]) ).
fof(f1486,plain,
! [X0,X1] :
( netstr_restr_to_element(sK26_skl,X0,X1) = net_str_of(sK26_skl,the_carrier(netstr_restr_to_element(sK26_skl,X0,X1)),the_InternalRel(netstr_restr_to_element(sK26_skl,X0,X1)),the_mapping(sK26_skl,netstr_restr_to_element(sK26_skl,X0,X1)))
| ~ element(X1,the_carrier(X0))
| ~ net_str(X0,sK26_skl)
| empty_carrier(X0)
| empty_carrier(sK26_skl) ),
inference(resolution,[status(thm)],[f854,f257]) ).
fof(f1489,definition,
! [X0,X1] :
( sQ127_spl
<=> ( netstr_restr_to_element(sK0_skl,X0,X1) = net_str_of(sK0_skl,the_carrier(netstr_restr_to_element(sK0_skl,X0,X1)),the_InternalRel(netstr_restr_to_element(sK0_skl,X0,X1)),the_mapping(sK0_skl,netstr_restr_to_element(sK0_skl,X0,X1)))
| ~ element(X1,the_carrier(X0))
| ~ net_str(X0,sK0_skl)
| empty_carrier(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1492,plain,
( ~ sQ14_spl
| sQ127_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f1485,f383,f1489,f386]) ).
fof(f1493,definition,
! [X0,X1] :
( sQ128_spl
<=> ( netstr_restr_to_element(sK26_skl,X0,X1) = net_str_of(sK26_skl,the_carrier(netstr_restr_to_element(sK26_skl,X0,X1)),the_InternalRel(netstr_restr_to_element(sK26_skl,X0,X1)),the_mapping(sK26_skl,netstr_restr_to_element(sK26_skl,X0,X1)))
| ~ element(X1,the_carrier(X0))
| ~ net_str(X0,sK26_skl)
| empty_carrier(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1496,plain,
( sQ128_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f1486,f1325,f1493]) ).
fof(f1606,plain,
( ~ sQ63_spl
| ~ sQ102_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))))
| ~ element(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))),sK0_skl,sK1_skl)
| ~ in(sK29_skl(sK3_skl,sK2_skl),the_carrier(sK1_skl))
| in(sK29_skl(sK3_skl,sK2_skl),sK2_skl) ),
inference(paramodulation,[status(thm)],[f1240,f315]) ).
fof(f1612,definition,
( sQ133_spl
<=> sK4_skl = topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1614,plain,
( sQ133_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))))) ),
inference(component_clause,[status(thm)],[f1612]) ).
fof(f1616,definition,
( sQ134_spl
<=> netstr_induced_subset(relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1618,plain,
( sQ134_spl
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1616]) ).
fof(f1621,plain,
( ~ sQ102_spl
| ~ sQ133_spl
| ~ sQ63_spl
| ~ sQ134_spl
| ~ sQ43_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1606,f693,f553,f1616,f696,f1612,f1233]) ).
fof(f1630,plain,
( sQ133_spl
| ~ sQ63_spl
| ~ sQ102_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,subnetstr_of_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))))) ),
inference(forward_demodulation,[status(thm)],[f1240,f1614]) ).
fof(f1631,plain,
( sQ133_spl
| ~ sQ63_spl
| ~ sQ102_spl
| sK4_skl != topstr_closure(sK0_skl,relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))))) ),
inference(forward_demodulation,[status(thm)],[f1240,f1630]) ).
fof(f1632,plain,
( sQ133_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl
| sK4_skl != topstr_closure(sK0_skl,sK7_skl(sK29_skl(sK3_skl,sK2_skl))) ),
inference(forward_demodulation,[status(thm)],[f1250,f1631]) ).
fof(f1633,plain,
( sQ133_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl
| ~ sQ42_spl
| sK4_skl != sK4_skl ),
inference(forward_demodulation,[status(thm)],[f550,f1632]) ).
fof(f1634,plain,
( sQ133_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl
| ~ sQ42_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1633]) ).
fof(f1635,plain,
( sQ133_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl
| ~ sQ42_spl ),
inference(contradiction_clause,[status(thm)],[f1634]) ).
fof(f1636,plain,
( sQ134_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl))),the_carrier(sK0_skl),the_mapping(sK0_skl,netstr_restr_to_element(sK0_skl,sK1_skl,sK29_skl(sK3_skl,sK2_skl)))),sK0_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f1240,f1618]) ).
fof(f1637,plain,
( sQ134_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl
| ~ netstr_induced_subset(sK7_skl(sK29_skl(sK3_skl,sK2_skl)),sK0_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f1250,f1636]) ).
fof(f1643,plain,
( sQ43_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f1132]) ).
fof(f1644,plain,
( sQ43_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f1643]) ).
fof(f1645,plain,
( sQ134_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl
| ~ in(sK29_skl(sK3_skl,sK2_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f1637,f90]) ).
fof(f1646,plain,
( sQ134_spl
| ~ sQ63_spl
| ~ sQ102_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1645,f682,f1233,f696,f1616]) ).
fof(f1647,plain,
$false,
inference(sat_refutation,[status(thm)],[f328,f330,f345,f349,f351,f376,f379,f382,f394,f397,f402,f407,f496,f514,f552,f556,f625,f626,f692,f699,f712,f717,f734,f743,f752,f761,f768,f793,f802,f805,f829,f866,f877,f878,f883,f979,f981,f1012,f1037,f1041,f1045,f1062,f1070,f1112,f1113,f1121,f1125,f1157,f1159,f1166,f1184,f1186,f1187,f1188,f1189,f1216,f1226,f1228,f1236,f1262,f1331,f1335,f1339,f1343,f1345,f1347,f1492,f1496,f1621,f1635,f1644,f1646]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU401+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:19:34 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.57 % Refutation found
% 0.09/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.82/0.59 % Elapsed time: 0.219983 seconds
% 0.82/0.59 % CPU time: 1.424180 seconds
% 0.82/0.59 % Total memory used: 123.786 MB
% 0.82/0.59 % Net memory used: 122.657 MB
%------------------------------------------------------------------------------