%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU324+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 : n011.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:10 PM UTC 2026
% Result : Theorem 0.15s 5.41s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 111
% Syntax : Number of formulae : 448 ( 32 unt; 92 def)
% Number of atoms : 1303 ( 132 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1513 ( 658 ~; 668 |; 61 &)
% ( 95 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 100 ( 98 usr; 92 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-2 aty)
% Number of variables : 199 ( 183 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A) )
=> element(interior(A,B),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A) )
=> element(topstr_closure(A,B),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
? [A] : top_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,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/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& closed_subset(B,A)
& top_str(A)
& topological_space(A) )
=> open_subset(subset_complement(the_carrier(A),B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& open_subset(B,A)
& top_str(A)
& topological_space(A) )
=> closed_subset(subset_complement(the_carrier(A),B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> open_subset(interior(A,B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,subset_complement(A,B)) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ? [B] :
( open_subset(B,A)
& element(B,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ? [B] :
( closed_subset(B,A)
& open_subset(B,A)
& element(B,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ? [B] :
( closed_subset(B,A)
& element(B,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( open_subset(B,A)
<=> closed_subset(subset_complement(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( ( ( topstr_closure(A,B) = B
& topological_space(A) )
=> closed_subset(B,A) )
& ( closed_subset(B,A)
=> topstr_closure(A,B) = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( top_str(B)
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ! [D] :
( element(D,powerset(the_carrier(B)))
=> ( ( interior(A,C) = C
=> open_subset(C,A) )
& ( open_subset(D,B)
=> interior(B,D) = D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( top_str(B)
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ! [D] :
( element(D,powerset(the_carrier(B)))
=> ( ( interior(A,C) = C
=> open_subset(C,A) )
& ( open_subset(D,B)
=> interior(B,D) = D ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f25]) ).
fof(f27,plain,
! [A] :
( ! [B] :
( interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B)))
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f28,plain,
! [X0,X1] :
( interior(X0,X1) = subset_complement(the_carrier(X0),topstr_closure(X0,subset_complement(the_carrier(X0),X1)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
! [A,B] :
( element(interior(A,B),powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
! [X0,X1] :
( element(interior(X0,X1),powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f32,plain,
! [X0,X1] :
( element(subset_complement(X1,X0),powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f33,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)],[f5]) ).
fof(f34,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)],[f33]) ).
fof(f37,plain,
top_str(sK0_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f10]) ).
fof(f38,plain,
top_str(sK0_skl),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f41,plain,
! [A] : element(sK2_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B,sK2_skl(A))],[f12]) ).
fof(f42,plain,
! [X0] : element(sK2_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,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)],[f13]) ).
fof(f44,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)],[f43]) ).
fof(f45,plain,
! [A,B] :
( open_subset(subset_complement(the_carrier(A),B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ closed_subset(B,A)
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f46,plain,
! [X0,X1] :
( open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ closed_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [A,B] :
( closed_subset(subset_complement(the_carrier(A),B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ open_subset(B,A)
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f48,plain,
! [X0,X1] :
( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ open_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [A,B] :
( open_subset(interior(A,B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f50,plain,
! [X0,X1] :
( open_subset(interior(X0,X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [A,B] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f52,plain,
! [X0,X1] :
( subset_complement(X1,subset_complement(X1,X0)) = X0
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [A] :
( ? [B] :
( open_subset(B,A)
& element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f54,plain,
! [A] :
( ( open_subset(sK3_skl(A),A)
& element(sK3_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl(A))],[f53]) ).
fof(f55,plain,
! [X0] :
( element(sK3_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0] :
( open_subset(sK3_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f57,plain,
! [A] :
( ? [B] :
( closed_subset(B,A)
& open_subset(B,A)
& element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f58,plain,
! [A] :
( ( closed_subset(sK4_skl(A),A)
& open_subset(sK4_skl(A),A)
& element(sK4_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f57]) ).
fof(f59,plain,
! [X0] :
( element(sK4_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0] :
( open_subset(sK4_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f61,plain,
! [X0] :
( closed_subset(sK4_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f62,plain,
! [A] :
( ? [B] :
( closed_subset(B,A)
& element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f63,plain,
! [A] :
( ( closed_subset(sK5_skl(A),A)
& element(sK5_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B,sK5_skl(A))],[f62]) ).
fof(f64,plain,
! [X0] :
( element(sK5_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0] :
( closed_subset(sK5_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f66,plain,
! [A] : subset(A,A),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f67,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [A] :
( ! [B] :
( ( open_subset(B,A)
<=> closed_subset(subset_complement(the_carrier(A),B),A) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f69,plain,
! [A] :
( ! [B] :
( ( ( ~ closed_subset(subset_complement(the_carrier(A),B),A)
| open_subset(B,A) )
& ( closed_subset(subset_complement(the_carrier(A),B),A)
| ~ open_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
! [X0,X1] :
( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [X0,X1] :
( ~ closed_subset(subset_complement(the_carrier(X0),X1),X0)
| open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f23]) ).
fof(f73,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f75,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f76,plain,
! [A] :
( ! [B] :
( ( ( closed_subset(B,A)
| topstr_closure(A,B) != B
| ~ topological_space(A) )
& ( topstr_closure(A,B) = B
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f77,plain,
! [X0,X1] :
( topstr_closure(X0,X1) = X1
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [X0,X1] :
( closed_subset(X1,X0)
| topstr_closure(X0,X1) != X1
| ~ topological_space(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ( ( ~ open_subset(C,A)
& interior(A,C) = C )
| ( interior(B,D) != D
& open_subset(D,B) ) )
& element(D,powerset(the_carrier(B))) )
& element(C,powerset(the_carrier(A))) )
& top_str(B) )
& top_str(A)
& topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f80,definition,
! [B,D] :
( sP0_prd(D,B)
<=> ( interior(B,D) != D
& open_subset(D,B) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f81,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ( ( ~ open_subset(C,A)
& interior(A,C) = C )
| sP0_prd(D,B) )
& element(D,powerset(the_carrier(B))) )
& element(C,powerset(the_carrier(A))) )
& top_str(B) )
& top_str(A)
& topological_space(A) ),
inference(formula_renaming,[status(thm)],[f79,f80]) ).
fof(f82,plain,
( ( ( ~ open_subset(sK8_skl,sK6_skl)
& interior(sK6_skl,sK8_skl) = sK8_skl )
| sP0_prd(sK9_skl,sK7_skl) )
& element(sK9_skl,powerset(the_carrier(sK7_skl)))
& element(sK8_skl,powerset(the_carrier(sK6_skl)))
& top_str(sK7_skl)
& top_str(sK6_skl)
& topological_space(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(A,sK6_skl),skolemize(B,sK7_skl),skolemize(C,sK8_skl),skolemize(D,sK9_skl)],[f81]) ).
fof(f83,plain,
topological_space(sK6_skl),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
top_str(sK6_skl),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f85,plain,
top_str(sK7_skl),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f86,plain,
element(sK8_skl,powerset(the_carrier(sK6_skl))),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f87,plain,
element(sK9_skl,powerset(the_carrier(sK7_skl))),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f88,plain,
( interior(sK6_skl,sK8_skl) = sK8_skl
| sP0_prd(sK9_skl,sK7_skl) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f89,plain,
( ~ open_subset(sK8_skl,sK6_skl)
| sP0_prd(sK9_skl,sK7_skl) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f90,plain,
! [B,D] :
( ( interior(B,D) = D
| ~ open_subset(D,B)
| sP0_prd(D,B) )
& ( ( interior(B,D) != D
& open_subset(D,B) )
| ~ sP0_prd(D,B) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f91,plain,
( ! [B,D] :
( interior(B,D) = D
| ~ open_subset(D,B)
| sP0_prd(D,B) )
& ! [B,D] :
( ( interior(B,D) != D
& open_subset(D,B) )
| ~ sP0_prd(D,B) ) ),
inference(miniscoping,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0,X1] :
( open_subset(X0,X1)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( interior(X1,X0) != X0
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f95,definition,
( sQ0_spl
<=> sP0_prd(sK9_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f96,plain,
( ~ sQ0_spl
| sP0_prd(sK9_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f95]) ).
fof(f98,definition,
( sQ1_spl
<=> interior(sK6_skl,sK8_skl) = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f99,plain,
( ~ sQ1_spl
| interior(sK6_skl,sK8_skl) = sK8_skl ),
inference(component_clause,[status(thm)],[f98]) ).
fof(f101,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f88,f95,f98]) ).
fof(f102,definition,
( sQ2_spl
<=> open_subset(sK8_skl,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f103,plain,
( ~ sQ2_spl
| open_subset(sK8_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f102]) ).
fof(f104,plain,
( sQ2_spl
| ~ open_subset(sK8_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f102]) ).
fof(f105,plain,
( ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f89,f95,f102]) ).
fof(f106,plain,
( ~ sQ0_spl
| interior(sK7_skl,sK9_skl) != sK9_skl ),
inference(resolution,[status(thm)],[f93,f96]) ).
fof(f108,plain,
! [X0] :
( interior(sK0_skl,X0) = subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,subset_complement(the_carrier(sK0_skl),X0)))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f28,f38]) ).
fof(f109,plain,
! [X0] :
( interior(sK7_skl,X0) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),X0)))
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f28,f85]) ).
fof(f110,plain,
! [X0] :
( interior(sK6_skl,X0) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),X0)))
| ~ element(X0,powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f28,f84]) ).
fof(f111,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl)
| interior(sK7_skl,interior(sK7_skl,X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0)))) ),
inference(resolution,[status(thm)],[f109,f30]) ).
fof(f112,plain,
interior(sK7_skl,sK9_skl) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl))),
inference(resolution,[status(thm)],[f109,f87]) ).
fof(f113,definition,
! [X0] :
( sQ3_spl
<=> ( ~ element(X0,powerset(the_carrier(sK7_skl)))
| interior(sK7_skl,interior(sK7_skl,X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0)))) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f114,plain,
! [X0] :
( ~ sQ3_spl
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| interior(sK7_skl,interior(sK7_skl,X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0)))) ),
inference(component_clause,[status(thm)],[f113]) ).
fof(f116,definition,
( sQ4_spl
<=> top_str(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f118,plain,
( sQ4_spl
| ~ top_str(sK7_skl) ),
inference(component_clause,[status(thm)],[f116]) ).
fof(f119,plain,
( ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f111,f113,f116]) ).
fof(f120,plain,
interior(sK7_skl,sK2_skl(powerset(the_carrier(sK7_skl)))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK2_skl(powerset(the_carrier(sK7_skl)))))),
inference(resolution,[status(thm)],[f42,f109]) ).
fof(f122,plain,
! [X0] : subset_complement(X0,subset_complement(X0,sK2_skl(powerset(X0)))) = sK2_skl(powerset(X0)),
inference(resolution,[status(thm)],[f52,f42]) ).
fof(f123,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| subset_complement(the_carrier(X0),subset_complement(the_carrier(X0),interior(X0,X1))) = interior(X0,X1) ),
inference(resolution,[status(thm)],[f52,f30]) ).
fof(f124,plain,
subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),sK9_skl)) = sK9_skl,
inference(resolution,[status(thm)],[f52,f87]) ).
fof(f125,plain,
subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK8_skl)) = sK8_skl,
inference(resolution,[status(thm)],[f52,f86]) ).
fof(f126,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| subset_complement(X0,subset_complement(X0,X1)) = X1 ),
inference(resolution,[status(thm)],[f52,f75]) ).
fof(f128,plain,
! [X0] : subset_complement(X0,subset_complement(X0,X0)) = X0,
inference(resolution,[status(thm)],[f126,f67]) ).
fof(f129,plain,
! [X0] :
( interior(sK7_skl,subset_complement(the_carrier(sK7_skl),X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),X0))))
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f32,f109]) ).
fof(f131,plain,
! [X0] :
( interior(sK7_skl,topstr_closure(sK7_skl,X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))))
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl) ),
inference(resolution,[status(thm)],[f34,f109]) ).
fof(f133,definition,
! [X0] :
( sQ5_spl
<=> ( interior(sK7_skl,topstr_closure(sK7_skl,X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))))
| ~ element(X0,powerset(the_carrier(sK7_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f134,plain,
! [X0] :
( ~ sQ5_spl
| interior(sK7_skl,topstr_closure(sK7_skl,X0)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))))
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f133]) ).
fof(f136,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f131,f116,f133]) ).
fof(f137,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f118,f85]) ).
fof(f138,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f137]) ).
fof(f139,plain,
( element(sK9_skl,powerset(the_carrier(sK7_skl)))
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl))) ),
inference(paramodulation,[status(thm)],[f124,f32]) ).
fof(f140,definition,
( sQ6_spl
<=> element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f141,plain,
( ~ sQ6_spl
| element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f142,plain,
( sQ6_spl
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f143,definition,
( sQ7_spl
<=> element(sK9_skl,powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f146,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f139,f140,f143]) ).
fof(f147,plain,
( element(sK8_skl,powerset(the_carrier(sK6_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f125,f32]) ).
fof(f148,definition,
( sQ8_spl
<=> element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f150,plain,
( sQ8_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f148]) ).
fof(f151,definition,
( sQ9_spl
<=> element(sK8_skl,powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f147,f148,f151]) ).
fof(f155,plain,
( sQ6_spl
| ~ element(sK9_skl,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f142,f32]) ).
fof(f157,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f155,f87]) ).
fof(f158,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f157]) ).
fof(f159,plain,
( sQ8_spl
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f150,f32]) ).
fof(f161,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f159,f86]) ).
fof(f162,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f161]) ).
fof(f163,plain,
( interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f125,f110]) ).
fof(f164,definition,
( sQ10_spl
<=> interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f165,plain,
( ~ sQ10_spl
| interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f164]) ).
fof(f167,plain,
( sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f163,f148,f164]) ).
fof(f168,plain,
( ~ sQ6_spl
| interior(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),sK9_skl)))) ),
inference(resolution,[status(thm)],[f141,f109]) ).
fof(f170,plain,
( ~ sQ6_spl
| interior(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f124,f168]) ).
fof(f172,plain,
( element(interior(sK7_skl,sK9_skl),powerset(the_carrier(sK7_skl)))
| ~ element(topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)),powerset(the_carrier(sK7_skl))) ),
inference(paramodulation,[status(thm)],[f112,f32]) ).
fof(f173,definition,
( sQ11_spl
<=> element(topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)),powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( ~ sQ11_spl
| element(topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)),powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f175,plain,
( sQ11_spl
| ~ element(topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)),powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f176,definition,
( sQ12_spl
<=> element(interior(sK7_skl,sK9_skl),powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f177,plain,
( ~ sQ12_spl
| element(interior(sK7_skl,sK9_skl),powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f176]) ).
fof(f179,plain,
( sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f172,f173,f176]) ).
fof(f180,plain,
( sQ11_spl
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl) ),
inference(resolution,[status(thm)],[f175,f34]) ).
fof(f182,plain,
( sQ11_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f180,f116,f140,f173]) ).
fof(f184,plain,
( ~ sQ12_spl
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl))) = interior(sK7_skl,sK9_skl) ),
inference(resolution,[status(thm)],[f177,f52]) ).
fof(f186,plain,
( ~ sQ11_spl
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)))) = topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) ),
inference(resolution,[status(thm)],[f174,f52]) ).
fof(f188,plain,
( ~ sQ11_spl
| subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl)) = topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f112,f186]) ).
fof(f189,plain,
( ~ sQ10_spl
| element(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),powerset(the_carrier(sK6_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(paramodulation,[status(thm)],[f165,f30]) ).
fof(f190,plain,
( ~ sQ10_spl
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl) ),
inference(paramodulation,[status(thm)],[f165,f50]) ).
fof(f191,definition,
( sQ13_spl
<=> top_str(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( sQ13_spl
| ~ top_str(sK6_skl) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
( sQ14_spl
<=> element(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( ~ sQ10_spl
| sQ14_spl
| ~ sQ8_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f189,f191,f148,f194,f164]) ).
fof(f198,definition,
( sQ15_spl
<=> topological_space(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f200,plain,
( sQ15_spl
| ~ topological_space(sK6_skl) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,definition,
( sQ16_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ16_spl
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),sK6_skl) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,plain,
( ~ sQ10_spl
| sQ16_spl
| ~ sQ8_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f190,f198,f191,f148,f201,f164]) ).
fof(f205,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f193,f84]) ).
fof(f206,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f205]) ).
fof(f207,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f200,f83]) ).
fof(f208,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f207]) ).
fof(f210,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK7_skl)))
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0))) = interior(sK7_skl,X0) ),
inference(resolution,[status(thm)],[f123,f85]) ).
fof(f211,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK6_skl)))
| subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),interior(sK6_skl,X0))) = interior(sK6_skl,X0) ),
inference(resolution,[status(thm)],[f123,f84]) ).
fof(f220,plain,
( interior(sK6_skl,subset_complement(the_carrier(sK6_skl),the_carrier(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,the_carrier(sK6_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),the_carrier(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f128,f110]) ).
fof(f222,definition,
( sQ19_spl
<=> element(subset_complement(the_carrier(sK6_skl),the_carrier(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( sQ19_spl
| ~ element(subset_complement(the_carrier(sK6_skl),the_carrier(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,definition,
( sQ20_spl
<=> interior(sK6_skl,subset_complement(the_carrier(sK6_skl),the_carrier(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f228,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f220,f222,f225]) ).
fof(f232,plain,
( element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f55,f83]) ).
fof(f233,definition,
( sQ21_spl
<=> element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ21_spl
| element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,plain,
( sQ21_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f232,f191,f233]) ).
fof(f237,plain,
( ~ sQ21_spl
| subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) = sK3_skl(sK6_skl) ),
inference(resolution,[status(thm)],[f234,f52]) ).
fof(f238,plain,
( element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f59,f83]) ).
fof(f239,definition,
( sQ22_spl
<=> element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f240,plain,
( ~ sQ22_spl
| element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f239]) ).
fof(f242,plain,
( sQ22_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f238,f191,f239]) ).
fof(f243,plain,
( ~ sQ22_spl
| subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) = sK4_skl(sK6_skl) ),
inference(resolution,[status(thm)],[f240,f52]) ).
fof(f244,plain,
( element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f64,f83]) ).
fof(f245,definition,
( sQ23_spl
<=> element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f246,plain,
( ~ sQ23_spl
| element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,plain,
( sQ23_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f244,f191,f245]) ).
fof(f249,plain,
( ~ sQ23_spl
| subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl))) = sK5_skl(sK6_skl) ),
inference(resolution,[status(thm)],[f246,f52]) ).
fof(f250,plain,
( interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK2_skl(powerset(the_carrier(sK6_skl))))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK2_skl(powerset(the_carrier(sK6_skl)))))
| ~ element(subset_complement(the_carrier(sK6_skl),sK2_skl(powerset(the_carrier(sK6_skl)))),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f122,f110]) ).
fof(f252,definition,
( sQ24_spl
<=> element(subset_complement(the_carrier(sK6_skl),sK2_skl(powerset(the_carrier(sK6_skl)))),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f254,plain,
( sQ24_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK2_skl(powerset(the_carrier(sK6_skl)))),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f255,definition,
( sQ25_spl
<=> interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK2_skl(powerset(the_carrier(sK6_skl))))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK2_skl(powerset(the_carrier(sK6_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f258,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f250,f252,f255]) ).
fof(f259,plain,
( sQ19_spl
| ~ element(the_carrier(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f224,f32]) ).
fof(f261,plain,
( sQ19_spl
| ~ subset(the_carrier(sK6_skl),the_carrier(sK6_skl)) ),
inference(resolution,[status(thm)],[f259,f75]) ).
fof(f262,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f261,f67]) ).
fof(f263,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f262]) ).
fof(f264,plain,
! [X0] :
( open_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ closed_subset(X0,sK6_skl)
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f46,f83]) ).
fof(f265,definition,
! [X0] :
( sQ26_spl
<=> ( open_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ closed_subset(X0,sK6_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f266,plain,
! [X0] :
( ~ sQ26_spl
| open_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ closed_subset(X0,sK6_skl) ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,plain,
( sQ26_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f264,f191,f265]) ).
fof(f269,plain,
! [X0] :
( closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ open_subset(X0,sK6_skl)
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f48,f83]) ).
fof(f270,definition,
! [X0] :
( sQ27_spl
<=> ( closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ open_subset(X0,sK6_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f271,plain,
! [X0] :
( ~ sQ27_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ open_subset(X0,sK6_skl) ),
inference(component_clause,[status(thm)],[f270]) ).
fof(f273,plain,
( sQ27_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f269,f191,f270]) ).
fof(f275,plain,
! [X0] :
( closed_subset(subset_complement(the_carrier(sK7_skl),X0),sK7_skl)
| ~ open_subset(X0,sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f70,f85]) ).
fof(f281,plain,
( ~ sQ21_spl
| interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK3_skl(sK6_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f237,f110]) ).
fof(f283,definition,
( sQ28_spl
<=> element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f285,plain,
( sQ28_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f283]) ).
fof(f286,definition,
( sQ29_spl
<=> interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK3_skl(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f289,plain,
( ~ sQ21_spl
| sQ29_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f281,f283,f286,f233]) ).
fof(f291,plain,
! [X0] :
( ~ sQ26_spl
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,X0)),sK6_skl)
| ~ element(topstr_closure(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f266,f44]) ).
fof(f292,plain,
( ~ sQ26_spl
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| open_subset(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),sK6_skl)
| ~ element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f266,f65]) ).
fof(f293,plain,
( ~ sQ26_spl
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| open_subset(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f266,f61]) ).
fof(f294,definition,
! [X0] :
( sQ30_spl
<=> ( ~ element(X0,powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,X0)),sK6_skl)
| ~ element(topstr_closure(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f295,plain,
! [X0] :
( ~ sQ30_spl
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,X0)),sK6_skl)
| ~ element(topstr_closure(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f294]) ).
fof(f297,plain,
( ~ sQ26_spl
| ~ sQ13_spl
| ~ sQ15_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f291,f294,f198,f191,f265]) ).
fof(f298,definition,
( sQ31_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f299,plain,
( ~ sQ31_spl
| open_subset(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),sK6_skl) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f301,plain,
( ~ sQ26_spl
| ~ sQ13_spl
| ~ sQ15_spl
| sQ31_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f292,f245,f298,f198,f191,f265]) ).
fof(f302,definition,
( sQ32_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f303,plain,
( ~ sQ32_spl
| open_subset(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),sK6_skl) ),
inference(component_clause,[status(thm)],[f302]) ).
fof(f305,plain,
( ~ sQ26_spl
| ~ sQ13_spl
| ~ sQ15_spl
| sQ32_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f293,f239,f302,f198,f191,f265]) ).
fof(f306,plain,
( sQ28_spl
| ~ element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f285,f32]) ).
fof(f308,plain,
( sQ28_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f306,f234]) ).
fof(f309,plain,
( sQ28_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f308]) ).
fof(f311,plain,
( ~ sQ22_spl
| interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK4_skl(sK6_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f243,f110]) ).
fof(f313,definition,
( sQ33_spl
<=> element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f315,plain,
( sQ33_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f313]) ).
fof(f316,definition,
( sQ34_spl
<=> interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK4_skl(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f319,plain,
( ~ sQ22_spl
| sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f311,f313,f316,f239]) ).
fof(f321,plain,
( sQ33_spl
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f315,f32]) ).
fof(f323,plain,
( sQ33_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f321,f240]) ).
fof(f324,plain,
( sQ33_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f323]) ).
fof(f326,plain,
( ~ sQ23_spl
| interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK5_skl(sK6_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f249,f110]) ).
fof(f328,definition,
( sQ35_spl
<=> element(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( sQ35_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f328]) ).
fof(f331,definition,
( sQ36_spl
<=> interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK5_skl(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( ~ sQ23_spl
| sQ36_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f326,f328,f331,f245]) ).
fof(f336,plain,
( ~ sQ32_spl
| ~ sQ27_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f271,f303]) ).
fof(f337,plain,
( ~ sQ31_spl
| ~ sQ27_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f271,f299]) ).
fof(f338,plain,
( ~ sQ16_spl
| ~ sQ27_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f271,f202]) ).
fof(f339,plain,
( ~ sQ27_spl
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| closed_subset(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f271,f60]) ).
fof(f340,plain,
( ~ sQ27_spl
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| closed_subset(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),sK6_skl)
| ~ element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f271,f56]) ).
fof(f341,plain,
! [X0] :
( ~ sQ27_spl
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,X0)),sK6_skl)
| ~ element(interior(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f271,f50]) ).
fof(f343,definition,
( sQ37_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f346,plain,
( ~ sQ32_spl
| ~ sQ27_spl
| sQ37_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f336,f313,f343,f270,f302]) ).
fof(f347,definition,
( sQ38_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK5_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f350,plain,
( ~ sQ31_spl
| ~ sQ27_spl
| sQ38_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f337,f328,f347,f270,f298]) ).
fof(f351,definition,
( sQ39_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f352,plain,
( ~ sQ39_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))),sK6_skl) ),
inference(component_clause,[status(thm)],[f351]) ).
fof(f354,plain,
( ~ sQ16_spl
| ~ sQ27_spl
| sQ39_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f338,f194,f351,f270,f201]) ).
fof(f355,definition,
( sQ40_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f356,plain,
( ~ sQ40_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),sK6_skl) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f358,plain,
( ~ sQ27_spl
| ~ sQ13_spl
| ~ sQ15_spl
| sQ40_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f339,f239,f355,f198,f191,f270]) ).
fof(f359,definition,
( sQ41_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f360,plain,
( ~ sQ41_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),sK6_skl) ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( ~ sQ27_spl
| ~ sQ13_spl
| ~ sQ15_spl
| sQ41_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f340,f233,f359,f198,f191,f270]) ).
fof(f363,definition,
! [X0] :
( sQ42_spl
<=> ( ~ element(X0,powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,X0)),sK6_skl)
| ~ element(interior(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f364,plain,
! [X0] :
( ~ sQ42_spl
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,X0)),sK6_skl)
| ~ element(interior(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f366,plain,
( ~ sQ27_spl
| ~ sQ13_spl
| ~ sQ15_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f341,f363,f198,f191,f270]) ).
fof(f371,plain,
! [X0] :
( ~ sP0_prd(X0,sK7_skl)
| closed_subset(subset_complement(the_carrier(sK7_skl),X0),sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f275,f92]) ).
fof(f395,plain,
( ~ sQ26_spl
| ~ sQ40_spl
| open_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f356,f266]) ).
fof(f396,definition,
( sQ49_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( ~ sQ26_spl
| ~ sQ40_spl
| sQ49_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f395,f313,f396,f355,f265]) ).
fof(f403,plain,
( ~ sQ26_spl
| ~ sQ41_spl
| open_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f360,f266]) ).
fof(f404,definition,
( sQ50_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f407,plain,
( ~ sQ26_spl
| ~ sQ41_spl
| sQ50_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f403,f283,f404,f359,f265]) ).
fof(f411,plain,
( sQ35_spl
| ~ element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f330,f32]) ).
fof(f413,plain,
( sQ35_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f246]) ).
fof(f414,plain,
( sQ35_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f413]) ).
fof(f420,plain,
! [X0] :
( topstr_closure(sK7_skl,X0) = X0
| ~ closed_subset(X0,sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f77,f85]) ).
fof(f421,plain,
! [X0] :
( topstr_closure(sK6_skl,X0) = X0
| ~ closed_subset(X0,sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f77,f84]) ).
fof(f446,plain,
! [X0] :
( closed_subset(subset_complement(the_carrier(sK7_skl),X0),sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ closed_subset(subset_complement(the_carrier(sK7_skl),X0),sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl) ),
inference(resolution,[status(thm)],[f71,f275]) ).
fof(f447,plain,
! [X0] :
( ~ sQ27_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f71,f271]) ).
fof(f448,definition,
! [X0] :
( sQ51_spl
<=> ( closed_subset(subset_complement(the_carrier(sK7_skl),X0),sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ closed_subset(subset_complement(the_carrier(sK7_skl),X0),sK7_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ51_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f446,f116,f448]) ).
fof(f452,definition,
! [X0] :
( sQ52_spl
<=> ( closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ closed_subset(subset_complement(the_carrier(sK6_skl),X0),sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ27_spl
| sQ52_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f447,f191,f452,f270]) ).
fof(f456,plain,
! [X0] :
( closed_subset(X0,sK6_skl)
| topstr_closure(sK6_skl,X0) != X0
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f78,f83]) ).
fof(f457,definition,
! [X0] :
( sQ53_spl
<=> ( closed_subset(X0,sK6_skl)
| topstr_closure(sK6_skl,X0) != X0
| ~ element(X0,powerset(the_carrier(sK6_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ53_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f456,f191,f457]) ).
fof(f461,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| interior(sK0_skl,topstr_closure(sK0_skl,X0)) = subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,X0)))) ),
inference(resolution,[status(thm)],[f108,f34]) ).
fof(f464,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| interior(sK0_skl,interior(sK0_skl,X0)) = subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,subset_complement(the_carrier(sK0_skl),interior(sK0_skl,X0)))) ),
inference(resolution,[status(thm)],[f108,f30]) ).
fof(f466,definition,
! [X0] :
( sQ54_spl
<=> ( ~ element(X0,powerset(the_carrier(sK0_skl)))
| interior(sK0_skl,topstr_closure(sK0_skl,X0)) = subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,X0)))) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f469,definition,
( sQ55_spl
<=> top_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ55_spl
| ~ top_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,plain,
( ~ sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f461,f466,f469]) ).
fof(f473,definition,
! [X0] :
( sQ56_spl
<=> ( ~ element(X0,powerset(the_carrier(sK0_skl)))
| interior(sK0_skl,interior(sK0_skl,X0)) = subset_complement(the_carrier(sK0_skl),topstr_closure(sK0_skl,subset_complement(the_carrier(sK0_skl),interior(sK0_skl,X0)))) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( ~ sQ55_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f464,f473,f469]) ).
fof(f477,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f471,f38]) ).
fof(f478,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f477]) ).
fof(f497,plain,
( ~ sQ41_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))
| ~ element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f421,f360]) ).
fof(f498,plain,
( ~ sQ40_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f421,f356]) ).
fof(f499,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| topstr_closure(sK6_skl,topstr_closure(sK6_skl,X0)) = topstr_closure(sK6_skl,X0)
| ~ element(topstr_closure(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f421,f44]) ).
fof(f501,plain,
( ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| topstr_closure(sK6_skl,sK5_skl(sK6_skl)) = sK5_skl(sK6_skl)
| ~ element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f421,f65]) ).
fof(f503,plain,
( ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl)
| topstr_closure(sK6_skl,sK4_skl(sK6_skl)) = sK4_skl(sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f421,f61]) ).
fof(f504,definition,
( sQ61_spl
<=> topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( ~ sQ61_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f507,plain,
( ~ sQ41_spl
| sQ61_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f497,f283,f504,f359]) ).
fof(f508,definition,
( sQ62_spl
<=> topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f509,plain,
( ~ sQ62_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) = subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( ~ sQ40_spl
| sQ62_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f498,f313,f508,f355]) ).
fof(f512,definition,
! [X0] :
( sQ63_spl
<=> ( ~ element(X0,powerset(the_carrier(sK6_skl)))
| topstr_closure(sK6_skl,topstr_closure(sK6_skl,X0)) = topstr_closure(sK6_skl,X0)
| ~ element(topstr_closure(sK6_skl,X0),powerset(the_carrier(sK6_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( ~ sQ13_spl
| ~ sQ15_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f499,f512,f198,f191]) ).
fof(f516,definition,
( sQ64_spl
<=> topstr_closure(sK6_skl,sK5_skl(sK6_skl)) = sK5_skl(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( ~ sQ64_spl
| topstr_closure(sK6_skl,sK5_skl(sK6_skl)) = sK5_skl(sK6_skl) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f520,plain,
( ~ sQ13_spl
| ~ sQ15_spl
| sQ64_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f501,f245,f516,f198,f191]) ).
fof(f521,definition,
( sQ65_spl
<=> topstr_closure(sK6_skl,sK4_skl(sK6_skl)) = sK4_skl(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f522,plain,
( ~ sQ65_spl
| topstr_closure(sK6_skl,sK4_skl(sK6_skl)) = sK4_skl(sK6_skl) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f525,plain,
( ~ sQ13_spl
| ~ sQ15_spl
| sQ65_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f503,f239,f521,f198,f191]) ).
fof(f526,plain,
( ~ sQ65_spl
| closed_subset(sK4_skl(sK6_skl),sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl) ),
inference(paramodulation,[status(thm)],[f522,f44]) ).
fof(f528,definition,
( sQ66_spl
<=> closed_subset(sK4_skl(sK6_skl),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( ~ sQ65_spl
| sQ66_spl
| ~ sQ22_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f526,f198,f191,f239,f528,f521]) ).
fof(f533,plain,
( ~ sQ64_spl
| closed_subset(sK5_skl(sK6_skl),sK6_skl)
| ~ element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl) ),
inference(paramodulation,[status(thm)],[f517,f44]) ).
fof(f535,definition,
( sQ67_spl
<=> closed_subset(sK5_skl(sK6_skl),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( ~ sQ64_spl
| sQ67_spl
| ~ sQ23_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f533,f198,f191,f245,f535,f516]) ).
fof(f543,plain,
( sQ24_spl
| ~ element(sK2_skl(powerset(the_carrier(sK6_skl))),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f254,f32]) ).
fof(f545,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f42]) ).
fof(f546,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f547,plain,
( ~ sQ39_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))
| ~ element(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f352,f421]) ).
fof(f548,plain,
( ~ sQ26_spl
| ~ sQ39_spl
| open_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f352,f266]) ).
fof(f549,definition,
( sQ68_spl
<=> element(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))),powerset(the_carrier(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f552,definition,
( sQ69_spl
<=> topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl))) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( ~ sQ39_spl
| sQ69_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f547,f549,f552,f351]) ).
fof(f556,definition,
( sQ70_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f559,plain,
( ~ sQ26_spl
| ~ sQ39_spl
| sQ70_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f548,f549,f556,f351,f265]) ).
fof(f562,plain,
( ~ sQ6_spl
| element(subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,sK9_skl)),powerset(the_carrier(sK7_skl)))
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl) ),
inference(paramodulation,[status(thm)],[f170,f30]) ).
fof(f564,definition,
( sQ71_spl
<=> element(subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,sK9_skl)),powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( sQ71_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f562,f116,f140,f564]) ).
fof(f576,definition,
( sQ73_spl
<=> element(subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl)),powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( ~ sQ11_spl
| element(subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl)),powerset(the_carrier(sK7_skl)))
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl) ),
inference(paramodulation,[status(thm)],[f188,f34]) ).
fof(f588,plain,
( ~ sQ11_spl
| sQ73_spl
| ~ sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f583,f116,f140,f576,f173]) ).
fof(f591,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl)
| interior(sK7_skl,subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))))) ),
inference(resolution,[status(thm)],[f129,f34]) ).
fof(f597,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl)
| interior(sK7_skl,subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0))))) ),
inference(resolution,[status(thm)],[f129,f30]) ).
fof(f600,definition,
! [X0] :
( sQ75_spl
<=> ( ~ element(X0,powerset(the_carrier(sK7_skl)))
| interior(sK7_skl,subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( ~ sQ4_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f591,f600,f116]) ).
fof(f609,definition,
! [X0] :
( sQ76_spl
<=> ( ~ element(X0,powerset(the_carrier(sK7_skl)))
| interior(sK7_skl,subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f612,plain,
( ~ sQ4_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f597,f609,f116]) ).
fof(f645,plain,
( ~ sQ62_spl
| interior(sK6_skl,sK4_skl(sK6_skl)) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)))
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f509,f110]) ).
fof(f648,definition,
( sQ83_spl
<=> interior(sK6_skl,sK4_skl(sK6_skl)) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ83_spl
| interior(sK6_skl,sK4_skl(sK6_skl)) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl))) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,plain,
( ~ sQ62_spl
| sQ83_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f645,f239,f648,f508]) ).
fof(f654,plain,
( ~ sQ83_spl
| ~ sQ22_spl
| interior(sK6_skl,sK4_skl(sK6_skl)) = sK4_skl(sK6_skl) ),
inference(forward_demodulation,[status(thm)],[f243,f649]) ).
fof(f656,plain,
( ~ sQ83_spl
| ~ sQ22_spl
| open_subset(sK4_skl(sK6_skl),sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl) ),
inference(paramodulation,[status(thm)],[f654,f50]) ).
fof(f658,definition,
( sQ84_spl
<=> open_subset(sK4_skl(sK6_skl),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f661,plain,
( ~ sQ83_spl
| sQ84_spl
| ~ sQ22_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f656,f198,f191,f239,f658,f648]) ).
fof(f662,plain,
( ~ sQ61_spl
| interior(sK6_skl,sK3_skl(sK6_skl)) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)))
| ~ element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f505,f110]) ).
fof(f665,definition,
( sQ85_spl
<=> interior(sK6_skl,sK3_skl(sK6_skl)) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f666,plain,
( ~ sQ85_spl
| interior(sK6_skl,sK3_skl(sK6_skl)) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl))) ),
inference(component_clause,[status(thm)],[f665]) ).
fof(f668,plain,
( ~ sQ61_spl
| sQ85_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f662,f233,f665,f504]) ).
fof(f671,plain,
( ~ sQ85_spl
| ~ sQ21_spl
| interior(sK6_skl,sK3_skl(sK6_skl)) = sK3_skl(sK6_skl) ),
inference(forward_demodulation,[status(thm)],[f237,f666]) ).
fof(f673,plain,
( ~ sQ85_spl
| ~ sQ21_spl
| open_subset(sK3_skl(sK6_skl),sK6_skl)
| ~ element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl) ),
inference(paramodulation,[status(thm)],[f671,f50]) ).
fof(f675,definition,
( sQ86_spl
<=> open_subset(sK3_skl(sK6_skl),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f678,plain,
( ~ sQ85_spl
| sQ86_spl
| ~ sQ21_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f673,f198,f191,f233,f675,f665]) ).
fof(f704,definition,
( sQ93_spl
<=> element(the_carrier(sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f706,plain,
( sQ93_spl
| ~ element(the_carrier(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f704]) ).
fof(f715,plain,
( ~ sQ6_spl
| ~ sQ3_spl
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl)))
| interior(sK7_skl,interior(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,sK9_skl))))) ),
inference(paramodulation,[status(thm)],[f170,f114]) ).
fof(f716,definition,
( sQ95_spl
<=> interior(sK7_skl,interior(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,sK9_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f715,f716,f140,f113]) ).
fof(f721,plain,
( ~ sQ5_spl
| interior(sK7_skl,topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK2_skl(powerset(the_carrier(sK7_skl)))))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,interior(sK7_skl,sK2_skl(powerset(the_carrier(sK7_skl))))))
| ~ element(subset_complement(the_carrier(sK7_skl),sK2_skl(powerset(the_carrier(sK7_skl)))),powerset(the_carrier(sK7_skl))) ),
inference(paramodulation,[status(thm)],[f120,f134]) ).
fof(f722,plain,
( ~ sQ11_spl
| ~ sQ5_spl
| interior(sK7_skl,topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl)))))
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl))) ),
inference(paramodulation,[status(thm)],[f188,f134]) ).
fof(f723,definition,
( sQ96_spl
<=> element(subset_complement(the_carrier(sK7_skl),sK2_skl(powerset(the_carrier(sK7_skl)))),powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f725,plain,
( sQ96_spl
| ~ element(subset_complement(the_carrier(sK7_skl),sK2_skl(powerset(the_carrier(sK7_skl)))),powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f726,definition,
( sQ97_spl
<=> interior(sK7_skl,topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK2_skl(powerset(the_carrier(sK7_skl)))))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,interior(sK7_skl,sK2_skl(powerset(the_carrier(sK7_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f729,plain,
( ~ sQ5_spl
| sQ97_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f721,f723,f726,f133]) ).
fof(f730,definition,
( sQ98_spl
<=> interior(sK7_skl,topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl))) = subset_complement(the_carrier(sK7_skl),topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f733,plain,
( ~ sQ11_spl
| ~ sQ5_spl
| sQ98_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f722,f140,f730,f133,f173]) ).
fof(f737,plain,
( sQ96_spl
| ~ element(sK2_skl(powerset(the_carrier(sK7_skl))),powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f725,f32]) ).
fof(f739,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f42]) ).
fof(f740,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f739]) ).
fof(f749,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl)
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,topstr_closure(sK7_skl,X0)))) = interior(sK7_skl,topstr_closure(sK7_skl,X0)) ),
inference(resolution,[status(thm)],[f210,f34]) ).
fof(f757,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl)
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,interior(sK7_skl,X0)))) = interior(sK7_skl,interior(sK7_skl,X0)) ),
inference(resolution,[status(thm)],[f210,f30]) ).
fof(f760,definition,
! [X0] :
( sQ99_spl
<=> ( ~ element(X0,powerset(the_carrier(sK7_skl)))
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,topstr_closure(sK7_skl,X0)))) = interior(sK7_skl,topstr_closure(sK7_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ4_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f749,f760,f116]) ).
fof(f766,definition,
! [X0] :
( sQ100_spl
<=> ( ~ element(X0,powerset(the_carrier(sK7_skl)))
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),interior(sK7_skl,interior(sK7_skl,X0)))) = interior(sK7_skl,interior(sK7_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ4_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f757,f766,f116]) ).
fof(f770,plain,
( ~ sQ0_spl
| closed_subset(subset_complement(the_carrier(sK7_skl),sK9_skl),sK7_skl)
| ~ element(sK9_skl,powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f371,f96]) ).
fof(f772,definition,
( sQ101_spl
<=> closed_subset(subset_complement(the_carrier(sK7_skl),sK9_skl),sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f773,plain,
( ~ sQ101_spl
| closed_subset(subset_complement(the_carrier(sK7_skl),sK9_skl),sK7_skl) ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f775,plain,
( ~ sQ0_spl
| sQ101_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f770,f143,f772,f95]) ).
fof(f776,plain,
( ~ sQ101_spl
| topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) = subset_complement(the_carrier(sK7_skl),sK9_skl)
| ~ element(subset_complement(the_carrier(sK7_skl),sK9_skl),powerset(the_carrier(sK7_skl))) ),
inference(resolution,[status(thm)],[f773,f420]) ).
fof(f777,definition,
( sQ102_spl
<=> topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) = subset_complement(the_carrier(sK7_skl),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( ~ sQ102_spl
| topstr_closure(sK7_skl,subset_complement(the_carrier(sK7_skl),sK9_skl)) = subset_complement(the_carrier(sK7_skl),sK9_skl) ),
inference(component_clause,[status(thm)],[f777]) ).
fof(f780,plain,
( ~ sQ101_spl
| sQ102_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f776,f140,f777,f772]) ).
fof(f781,plain,
( ~ sQ102_spl
| ~ sQ11_spl
| subset_complement(the_carrier(sK7_skl),interior(sK7_skl,sK9_skl)) = subset_complement(the_carrier(sK7_skl),sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f188,f778]) ).
fof(f782,plain,
( sQ2_spl
| ~ closed_subset(subset_complement(the_carrier(sK6_skl),sK8_skl),sK6_skl)
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl) ),
inference(resolution,[status(thm)],[f104,f71]) ).
fof(f784,definition,
( sQ103_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),sK8_skl),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f785,plain,
( ~ sQ103_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),sK8_skl),sK6_skl) ),
inference(component_clause,[status(thm)],[f784]) ).
fof(f787,plain,
( sQ2_spl
| ~ sQ103_spl
| ~ sQ9_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f782,f191,f151,f784,f102]) ).
fof(f802,plain,
( ~ sQ1_spl
| open_subset(sK8_skl,sK6_skl)
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ topological_space(sK6_skl) ),
inference(paramodulation,[status(thm)],[f99,f50]) ).
fof(f804,plain,
( ~ sQ1_spl
| sQ2_spl
| ~ sQ9_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f802,f198,f191,f151,f102,f98]) ).
fof(f808,plain,
( ~ sQ27_spl
| ~ sQ2_spl
| closed_subset(subset_complement(the_carrier(sK6_skl),sK8_skl),sK6_skl)
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f103,f271]) ).
fof(f809,plain,
( ~ sQ27_spl
| ~ sQ2_spl
| sQ103_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f808,f151,f784,f102,f270]) ).
fof(f827,definition,
( sQ107_spl
<=> element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f829,plain,
( sQ107_spl
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f827]) ).
fof(f834,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f42]) ).
fof(f835,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f834]) ).
fof(f840,plain,
( sQ93_spl
| ~ subset(the_carrier(sK0_skl),the_carrier(sK0_skl)) ),
inference(resolution,[status(thm)],[f706,f75]) ).
fof(f841,plain,
( sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f840,f67]) ).
fof(f842,plain,
sQ93_spl,
inference(contradiction_clause,[status(thm)],[f841]) ).
fof(f845,plain,
( ~ sQ103_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) = subset_complement(the_carrier(sK6_skl),sK8_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl))) ),
inference(resolution,[status(thm)],[f785,f421]) ).
fof(f847,definition,
( sQ109_spl
<=> topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) = subset_complement(the_carrier(sK6_skl),sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f848,plain,
( ~ sQ109_spl
| topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) = subset_complement(the_carrier(sK6_skl),sK8_skl) ),
inference(component_clause,[status(thm)],[f847]) ).
fof(f850,plain,
( ~ sQ103_spl
| sQ109_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f845,f148,f847,f784]) ).
fof(f873,plain,
( ~ sQ10_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl)))
| subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))) = interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) ),
inference(paramodulation,[status(thm)],[f165,f211]) ).
fof(f876,definition,
( sQ112_spl
<=> subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)))) = interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f879,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f873,f876,f148,f164]) ).
fof(f881,plain,
! [X0] :
( ~ sQ30_spl
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,X0)),sK6_skl) ),
inference(resolution,[status(thm)],[f295,f34]) ).
fof(f883,plain,
( ~ sQ61_spl
| ~ sQ30_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f505,f295]) ).
fof(f884,plain,
( ~ sQ62_spl
| ~ sQ30_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f509,f295]) ).
fof(f885,plain,
( ~ sQ64_spl
| ~ sQ30_spl
| ~ element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK5_skl(sK6_skl))),sK6_skl)
| ~ element(sK5_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f517,f295]) ).
fof(f886,plain,
( ~ sQ65_spl
| ~ sQ30_spl
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK4_skl(sK6_skl))),sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f522,f295]) ).
fof(f887,definition,
! [X0] :
( sQ113_spl
<=> ( ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,X0)),sK6_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( ~ sQ30_spl
| ~ sQ13_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f881,f887,f191,f294]) ).
fof(f891,definition,
( sQ114_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK3_skl(sK6_skl)))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f894,plain,
( ~ sQ61_spl
| ~ sQ30_spl
| sQ114_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f883,f283,f891,f294,f504]) ).
fof(f895,definition,
( sQ115_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,subset_complement(the_carrier(sK6_skl),sK4_skl(sK6_skl)))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f898,plain,
( ~ sQ62_spl
| ~ sQ30_spl
| sQ115_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f884,f313,f895,f294,f508]) ).
fof(f899,definition,
( sQ116_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK5_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f902,plain,
( ~ sQ64_spl
| ~ sQ30_spl
| sQ116_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f885,f245,f899,f294,f516]) ).
fof(f903,definition,
( sQ117_spl
<=> open_subset(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK4_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f906,plain,
( ~ sQ65_spl
| ~ sQ30_spl
| sQ117_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f886,f239,f903,f294,f521]) ).
fof(f919,plain,
( ~ sQ109_spl
| interior(sK6_skl,sK8_skl) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK8_skl))
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f848,f110]) ).
fof(f923,definition,
( sQ118_spl
<=> interior(sK6_skl,sK8_skl) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f924,plain,
( ~ sQ118_spl
| interior(sK6_skl,sK8_skl) = subset_complement(the_carrier(sK6_skl),subset_complement(the_carrier(sK6_skl),sK8_skl)) ),
inference(component_clause,[status(thm)],[f923]) ).
fof(f926,plain,
( ~ sQ109_spl
| sQ118_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f919,f151,f923,f847]) ).
fof(f933,plain,
( ~ sQ118_spl
| interior(sK6_skl,sK8_skl) = sK8_skl ),
inference(forward_demodulation,[status(thm)],[f125,f924]) ).
fof(f942,plain,
! [X0] :
( ~ sQ42_spl
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ top_str(sK6_skl)
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,X0)),sK6_skl) ),
inference(resolution,[status(thm)],[f364,f30]) ).
fof(f944,plain,
( ~ sQ118_spl
| ~ sQ42_spl
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,sK8_skl)),sK6_skl)
| ~ element(sK8_skl,powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f933,f364]) ).
fof(f945,plain,
( ~ sQ85_spl
| ~ sQ21_spl
| ~ sQ42_spl
| ~ element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,sK3_skl(sK6_skl))),sK6_skl)
| ~ element(sK3_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f671,f364]) ).
fof(f946,plain,
( ~ sQ83_spl
| ~ sQ22_spl
| ~ sQ42_spl
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,sK4_skl(sK6_skl))),sK6_skl)
| ~ element(sK4_skl(sK6_skl),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f654,f364]) ).
fof(f947,plain,
( ~ sQ10_spl
| ~ sQ42_spl
| ~ element(subset_complement(the_carrier(sK6_skl),sK8_skl),powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl))),sK6_skl)
| ~ element(subset_complement(the_carrier(sK6_skl),topstr_closure(sK6_skl,sK8_skl)),powerset(the_carrier(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f165,f364]) ).
fof(f948,definition,
! [X0] :
( sQ120_spl
<=> ( ~ element(X0,powerset(the_carrier(sK6_skl)))
| ~ element(X0,powerset(the_carrier(sK6_skl)))
| closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,X0)),sK6_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( ~ sQ42_spl
| ~ sQ13_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f942,f948,f191,f363]) ).
fof(f952,definition,
( sQ121_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,sK8_skl)),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f955,plain,
( ~ sQ118_spl
| ~ sQ42_spl
| sQ121_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f944,f151,f952,f363,f923]) ).
fof(f956,definition,
( sQ122_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,sK3_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f959,plain,
( ~ sQ85_spl
| ~ sQ42_spl
| sQ122_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f945,f233,f956,f363,f665]) ).
fof(f960,definition,
( sQ123_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,sK4_skl(sK6_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f963,plain,
( ~ sQ83_spl
| ~ sQ42_spl
| sQ123_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f946,f239,f960,f363,f648]) ).
fof(f964,definition,
( sQ124_spl
<=> closed_subset(subset_complement(the_carrier(sK6_skl),interior(sK6_skl,subset_complement(the_carrier(sK6_skl),sK8_skl))),sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( ~ sQ10_spl
| ~ sQ42_spl
| ~ sQ8_spl
| sQ124_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f947,f194,f964,f148,f363,f164]) ).
fof(f985,plain,
( ~ sQ12_spl
| ~ sQ102_spl
| ~ sQ11_spl
| subset_complement(the_carrier(sK7_skl),subset_complement(the_carrier(sK7_skl),sK9_skl)) = interior(sK7_skl,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f781,f184]) ).
fof(f986,plain,
( ~ sQ12_spl
| ~ sQ102_spl
| ~ sQ11_spl
| sK9_skl = interior(sK7_skl,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f124,f985]) ).
fof(f987,plain,
( ~ sQ12_spl
| ~ sQ102_spl
| ~ sQ11_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f986,f106]) ).
fof(f988,plain,
( ~ sQ12_spl
| ~ sQ102_spl
| ~ sQ11_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f987]) ).
fof(f989,plain,
$false,
inference(sat_refutation,[status(thm)],[f101,f105,f119,f136,f138,f146,f154,f158,f162,f167,f179,f182,f197,f204,f206,f208,f228,f236,f242,f248,f258,f263,f268,f273,f289,f297,f301,f305,f309,f319,f324,f334,f346,f350,f354,f358,f362,f366,f399,f407,f414,f451,f455,f460,f472,f476,f478,f507,f511,f515,f520,f525,f531,f538,f546,f555,f559,f567,f588,f603,f612,f651,f661,f668,f678,f719,f729,f733,f740,f763,f769,f775,f780,f787,f804,f809,f835,f842,f850,f879,f890,f894,f898,f902,f906,f926,f951,f955,f959,f963,f967,f988]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU324+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n011.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 06:11:46 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 0.15/5.41 % Refutation found
% 0.15/5.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/5.43 % Elapsed time: 0.052176 seconds
% 0.15/5.43 % CPU time: 0.183902 seconds
% 0.15/5.43 % Total memory used: 71.066 MB
% 0.15/5.43 % Net memory used: 70.851 MB
%------------------------------------------------------------------------------