%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU314+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 : n017.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:08 PM UTC 2026
% Result : Theorem 0.19s 0.65s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 71
% Syntax : Number of formulae : 298 ( 14 unt; 65 def)
% Number of atoms : 1446 ( 200 equ)
% Maximal formula atoms : 24 ( 4 avg)
% Number of connectives : 1910 ( 762 ~; 924 |; 146 &)
% ( 70 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 74 ( 72 usr; 65 prp; 0-5 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-5 aty)
% Number of variables : 321 ( 265 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( ? [E] :
( subset(B,D)
& closed_subset(E,A)
& E = D
& element(E,powerset(the_carrier(A))) )
& in(D,powerset(the_carrier(A))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( ? [E] :
( subset(B,D)
& closed_subset(E,A)
& E = D
& element(E,powerset(the_carrier(A))) )
& in(D,powerset(the_carrier(A))) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f20,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,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(f30,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> ( ! [C,D,E] :
( ( ? [G] :
( subset(B,E)
& closed_subset(G,A)
& G = E
& element(G,powerset(the_carrier(A))) )
& C = E
& ? [F] :
( subset(B,D)
& closed_subset(F,A)
& F = D
& element(F,powerset(the_carrier(A))) )
& C = D )
=> D = E )
=> ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( subset(B,D)
& closed_subset(H,A)
& H = D
& element(H,powerset(the_carrier(A))) )
& E = D
& in(E,powerset(the_carrier(A))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,plain,
? [A,B] :
( ! [C] :
? [D] :
( in(D,C)
<~> ( ? [E] :
( subset(B,D)
& closed_subset(E,A)
& E = D
& element(E,powerset(the_carrier(A))) )
& in(D,powerset(the_carrier(A))) ) )
& element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
? [A,B] :
( ! [C] :
? [D] :
( ( ! [E] :
( ~ subset(B,D)
| ~ closed_subset(E,A)
| E != D
| ~ element(E,powerset(the_carrier(A))) )
| ~ in(D,powerset(the_carrier(A)))
| ~ in(D,C) )
& ( ( ? [E] :
( subset(B,D)
& closed_subset(E,A)
& E = D
& element(E,powerset(the_carrier(A))) )
& in(D,powerset(the_carrier(A))) )
| in(D,C) ) )
& element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f33,plain,
? [A,B] :
( ! [C] :
? [D] :
( ( ~ subset(B,D)
| ! [E] :
( ~ closed_subset(E,A)
| E != D
| ~ element(E,powerset(the_carrier(A))) )
| ~ in(D,powerset(the_carrier(A)))
| ~ in(D,C) )
& ( ( subset(B,D)
& ? [E] :
( closed_subset(E,A)
& E = D
& element(E,powerset(the_carrier(A))) )
& in(D,powerset(the_carrier(A))) )
| in(D,C) ) )
& element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f34,plain,
( ! [C] :
( ( ~ subset(sK1_skl,sK2_skl(C))
| ! [E] :
( ~ closed_subset(E,sK0_skl)
| E != sK2_skl(C)
| ~ element(E,powerset(the_carrier(sK0_skl))) )
| ~ in(sK2_skl(C),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(C),C) )
& ( ( subset(sK1_skl,sK2_skl(C))
& closed_subset(sK3_skl(C),sK0_skl)
& sK3_skl(C) = sK2_skl(C)
& element(sK3_skl(C),powerset(the_carrier(sK0_skl)))
& in(sK2_skl(C),powerset(the_carrier(sK0_skl))) )
| in(sK2_skl(C),C) ) )
& element(sK1_skl,powerset(the_carrier(sK0_skl)))
& top_str(sK0_skl)
& topological_space(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C)),skolemize(E,sK3_skl(C))],[f33]) ).
fof(f35,plain,
topological_space(sK0_skl),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
top_str(sK0_skl),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f37,plain,
element(sK1_skl,powerset(the_carrier(sK0_skl))),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f38,plain,
! [X0] :
( in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f39,plain,
! [X0] :
( element(sK3_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f40,plain,
! [X0] :
( sK3_skl(X0) = sK2_skl(X0)
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f41,plain,
! [X0] :
( closed_subset(sK3_skl(X0),sK0_skl)
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f42,plain,
! [X0] :
( subset(sK1_skl,sK2_skl(X0))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f43,plain,
! [X0,X1] :
( ~ subset(sK1_skl,sK2_skl(X0))
| ~ closed_subset(X1,sK0_skl)
| X1 != sK2_skl(X0)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f103,plain,
! [A] :
( empty(sK6_skl(A))
& element(sK6_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f20]) ).
fof(f104,plain,
! [X0] : element(sK6_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f112,plain,
! [A] : subset(A,A),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f113,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f115,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f118,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)],[f28]) ).
fof(f119,plain,
! [A] :
( ( closed_subset(sK7_skl(A),A)
& element(sK7_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f118]) ).
fof(f120,plain,
! [X0] :
( element(sK7_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [X0] :
( closed_subset(sK7_skl(X0),X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f123,plain,
! [A,B] :
( ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( subset(B,D)
& closed_subset(H,A)
& H = D
& element(H,powerset(the_carrier(A))) )
& E = D
& in(E,powerset(the_carrier(A))) ) )
| ? [C,D,E] :
( D != E
& ? [G] :
( subset(B,E)
& closed_subset(G,A)
& G = E
& element(G,powerset(the_carrier(A))) )
& C = E
& ? [F] :
( subset(B,D)
& closed_subset(F,A)
& F = D
& element(F,powerset(the_carrier(A))) )
& C = D )
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f124,definition,
! [A,B,C,D,E] :
( sP0_prd(E,D,C,B,A)
<=> ( D != E
& ? [G] :
( subset(B,E)
& closed_subset(G,A)
& G = E
& element(G,powerset(the_carrier(A))) )
& C = E
& ? [F] :
( subset(B,D)
& closed_subset(F,A)
& F = D
& element(F,powerset(the_carrier(A))) )
& C = D ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f125,plain,
! [A,B] :
( ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( subset(B,D)
& closed_subset(H,A)
& H = D
& element(H,powerset(the_carrier(A))) )
& E = D
& in(E,powerset(the_carrier(A))) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(formula_renaming,[status(thm)],[f123,f124]) ).
fof(f126,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ! [H] :
( ~ subset(B,D)
| ~ closed_subset(H,A)
| H != D
| ~ element(H,powerset(the_carrier(A))) )
| E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,C) )
& ( ? [E] :
( ? [H] :
( subset(B,D)
& closed_subset(H,A)
& H = D
& element(H,powerset(the_carrier(A))) )
& E = D
& in(E,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(NNF_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ subset(B,D)
| ! [H] :
( ~ closed_subset(H,A)
| H != D
| ~ element(H,powerset(the_carrier(A))) )
| ! [E] :
( E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,C) )
& ! [D] :
( ( subset(B,D)
& ? [H] :
( closed_subset(H,A)
& H = D
& element(H,powerset(the_carrier(A))) )
& ? [E] :
( E = D
& in(E,powerset(the_carrier(A))) ) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
! [A,B] :
( ( ! [D] :
( ~ subset(B,D)
| ! [H] :
( ~ closed_subset(H,A)
| H != D
| ~ element(H,powerset(the_carrier(A))) )
| ! [E] :
( E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,sK11_skl(B,A)) )
& ! [D] :
( ( subset(B,D)
& closed_subset(sK13_skl(D,B,A),A)
& sK13_skl(D,B,A) = D
& element(sK13_skl(D,B,A),powerset(the_carrier(A)))
& sK12_skl(D,B,A) = D
& in(sK12_skl(D,B,A),powerset(the_carrier(A))) )
| ~ in(D,sK11_skl(B,A)) ) )
| sP0_prd(sK10_skl(B,A),sK9_skl(B,A),sK8_skl(B,A),B,A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(C,sK8_skl(B,A)),skolemize(D,sK9_skl(B,A)),skolemize(E,sK10_skl(B,A)),skolemize(C,sK11_skl(B,A)),skolemize(E,sK12_skl(D,B,A)),skolemize(H,sK13_skl(D,B,A))],[f127]) ).
fof(f129,plain,
! [X0,X1,X2] :
( in(sK12_skl(X2,X1,X0),powerset(the_carrier(X0)))
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0,X1,X2] :
( sK12_skl(X2,X1,X0) = X2
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
! [X0,X1,X2] :
( element(sK13_skl(X2,X1,X0),powerset(the_carrier(X0)))
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f132,plain,
! [X0,X1,X2] :
( sK13_skl(X2,X1,X0) = X2
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f133,plain,
! [X0,X1,X2] :
( closed_subset(sK13_skl(X2,X1,X0),X0)
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f134,plain,
! [X0,X1,X2] :
( subset(X1,X2)
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f135,plain,
! [X0,X1,X2,X3,X4] :
( ~ subset(X1,X2)
| ~ closed_subset(X4,X0)
| X4 != X2
| ~ element(X4,powerset(the_carrier(X0)))
| X3 != X2
| ~ in(X3,powerset(the_carrier(X0)))
| in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f136,plain,
! [A,B,C,D,E] :
( ( D = E
| ! [G] :
( ~ subset(B,E)
| ~ closed_subset(G,A)
| G != E
| ~ element(G,powerset(the_carrier(A))) )
| C != E
| ! [F] :
( ~ subset(B,D)
| ~ closed_subset(F,A)
| F != D
| ~ element(F,powerset(the_carrier(A))) )
| C != D
| sP0_prd(E,D,C,B,A) )
& ( ( D != E
& ? [G] :
( subset(B,E)
& closed_subset(G,A)
& G = E
& element(G,powerset(the_carrier(A))) )
& C = E
& ? [F] :
( subset(B,D)
& closed_subset(F,A)
& F = D
& element(F,powerset(the_carrier(A))) )
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f124]) ).
fof(f137,plain,
( ! [A,B,C,D,E] :
( D = E
| ~ subset(B,E)
| ! [G] :
( ~ closed_subset(G,A)
| G != E
| ~ element(G,powerset(the_carrier(A))) )
| C != E
| ~ subset(B,D)
| ! [F] :
( ~ closed_subset(F,A)
| F != D
| ~ element(F,powerset(the_carrier(A))) )
| C != D
| sP0_prd(E,D,C,B,A) )
& ! [A,B,C,D,E] :
( ( D != E
& subset(B,E)
& ? [G] :
( closed_subset(G,A)
& G = E
& element(G,powerset(the_carrier(A))) )
& C = E
& subset(B,D)
& ? [F] :
( closed_subset(F,A)
& F = D
& element(F,powerset(the_carrier(A))) )
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f138,plain,
( ! [A,B,C,D,E] :
( D = E
| ~ subset(B,E)
| ! [G] :
( ~ closed_subset(G,A)
| G != E
| ~ element(G,powerset(the_carrier(A))) )
| C != E
| ~ subset(B,D)
| ! [F] :
( ~ closed_subset(F,A)
| F != D
| ~ element(F,powerset(the_carrier(A))) )
| C != D
| sP0_prd(E,D,C,B,A) )
& ! [A,B,C,D,E] :
( ( D != E
& subset(B,E)
& closed_subset(sK15_skl(E,D,C,B,A),A)
& sK15_skl(E,D,C,B,A) = E
& element(sK15_skl(E,D,C,B,A),powerset(the_carrier(A)))
& C = E
& subset(B,D)
& closed_subset(sK14_skl(E,D,C,B,A),A)
& sK14_skl(E,D,C,B,A) = D
& element(sK14_skl(E,D,C,B,A),powerset(the_carrier(A)))
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(F,sK14_skl(E,D,C,B,A)),skolemize(G,sK15_skl(E,D,C,B,A))],[f137]) ).
fof(f139,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X1
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4] :
( sK14_skl(X0,X1,X2,X3,X4) = X1
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4] :
( element(sK15_skl(X0,X1,X2,X3,X4),powerset(the_carrier(X4)))
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f146,plain,
! [X0,X1,X2,X3,X4] :
( sK15_skl(X0,X1,X2,X3,X4) = X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4] :
( closed_subset(sK15_skl(X0,X1,X2,X3,X4),X4)
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4] :
( X1 != X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f151,plain,
! [X0,X1,X2] :
( ~ subset(X1,X2)
| ~ closed_subset(X2,X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X2,powerset(the_carrier(X0)))
| in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f135]) ).
fof(f152,plain,
! [X0,X1,X2,X3] : ~ sP0_prd(X0,X0,X1,X2,X3),
inference(destructive_equality_resolution,[status(thm)],[f149]) ).
fof(f156,plain,
! [X0,X1,X2] :
( ~ in(powerset(the_carrier(X0)),sK12_skl(X2,X1,X0))
| ~ in(X2,sK11_skl(X1,X0))
| sP0_prd(sK10_skl(X1,X0),sK9_skl(X1,X0),sK8_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f129,f115]) ).
fof(f157,plain,
! [X0,X1] :
( sK12_skl(X1,X0,sK0_skl) = X1
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f130,f35]) ).
fof(f158,definition,
( sQ0_spl
<=> top_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f160,plain,
( sQ0_spl
| ~ top_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f158]) ).
fof(f161,definition,
! [X0,X1] :
( sQ1_spl
<=> ( sK12_skl(X1,X0,sK0_skl) = X1
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f162,plain,
! [X0,X1] :
( ~ sQ1_spl
| sK12_skl(X1,X0,sK0_skl) = X1
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f161]) ).
fof(f164,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f157,f158,f161]) ).
fof(f165,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f160,f36]) ).
fof(f166,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f165]) ).
fof(f167,plain,
! [X0] :
( ~ sQ1_spl
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f162,f40]) ).
fof(f172,plain,
! [X0] :
( ~ sQ1_spl
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| sK14_skl(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl) = sK9_skl(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f141,f167]) ).
fof(f173,plain,
! [X0] :
( ~ sQ1_spl
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| sK15_skl(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl) = sK10_skl(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f146,f167]) ).
fof(f174,plain,
! [X0,X1] :
( sK13_skl(X1,X0,sK0_skl) = X1
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f132,f35]) ).
fof(f175,definition,
! [X0,X1] :
( sQ2_spl
<=> ( sK13_skl(X1,X0,sK0_skl) = X1
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f176,plain,
! [X0,X1] :
( ~ sQ2_spl
| sK13_skl(X1,X0,sK0_skl) = X1
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,plain,
( sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f174,f158,f175]) ).
fof(f179,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f134,f35]) ).
fof(f180,definition,
! [X0,X1] :
( sQ3_spl
<=> ( subset(X0,X1)
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f181,plain,
! [X0,X1] :
( ~ sQ3_spl
| subset(X0,X1)
| ~ in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f179,f158,f180]) ).
fof(f184,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ~ closed_subset(X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f151,f35]) ).
fof(f185,definition,
! [X0,X1] :
( sQ4_spl
<=> ( ~ subset(X0,X1)
| ~ closed_subset(X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f186,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ subset(X0,X1)
| ~ closed_subset(X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f185]) ).
fof(f188,plain,
( sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f184,f158,f185]) ).
fof(f190,plain,
! [X0] :
( ~ sQ2_spl
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f176,f40]) ).
fof(f191,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ in(X1,sK11_skl(X2,sK0_skl))
| sP0_prd(sK10_skl(X2,sK0_skl),sK9_skl(X2,sK0_skl),sK8_skl(X2,sK0_skl),X2,sK0_skl)
| ~ element(X2,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| ~ subset(X0,sK12_skl(X1,X2,sK0_skl))
| ~ closed_subset(sK12_skl(X1,X2,sK0_skl),sK0_skl)
| ~ element(sK12_skl(X1,X2,sK0_skl),powerset(the_carrier(sK0_skl)))
| in(sK12_skl(X1,X2,sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f186,f129]) ).
fof(f192,plain,
! [X0,X1] :
( ~ sQ4_spl
| in(sK2_skl(X1),X1)
| ~ subset(X0,sK2_skl(X1))
| ~ closed_subset(sK2_skl(X1),sK0_skl)
| ~ element(sK2_skl(X1),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X1),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f186,f38]) ).
fof(f194,definition,
! [X0,X1,X2] :
( sQ5_spl
<=> ( ~ in(X1,sK11_skl(X2,sK0_skl))
| sP0_prd(sK10_skl(X2,sK0_skl),sK9_skl(X2,sK0_skl),sK8_skl(X2,sK0_skl),X2,sK0_skl)
| ~ element(X2,powerset(the_carrier(sK0_skl)))
| ~ subset(X0,sK12_skl(X1,X2,sK0_skl))
| ~ closed_subset(sK12_skl(X1,X2,sK0_skl),sK0_skl)
| ~ element(sK12_skl(X1,X2,sK0_skl),powerset(the_carrier(sK0_skl)))
| in(sK12_skl(X1,X2,sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f195,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ in(X1,sK11_skl(X2,sK0_skl))
| sP0_prd(sK10_skl(X2,sK0_skl),sK9_skl(X2,sK0_skl),sK8_skl(X2,sK0_skl),X2,sK0_skl)
| ~ element(X2,powerset(the_carrier(sK0_skl)))
| ~ subset(X0,sK12_skl(X1,X2,sK0_skl))
| ~ closed_subset(sK12_skl(X1,X2,sK0_skl),sK0_skl)
| ~ element(sK12_skl(X1,X2,sK0_skl),powerset(the_carrier(sK0_skl)))
| in(sK12_skl(X1,X2,sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,definition,
( sQ6_spl
<=> topological_space(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( sQ6_spl
| ~ topological_space(sK0_skl) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f200,plain,
( ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f191,f194,f197,f158,f185]) ).
fof(f201,definition,
! [X0] :
( sQ7_spl
<=> ( ~ subset(X0,sK2_skl(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f202,plain,
! [X0] :
( ~ sQ7_spl
| ~ subset(X0,sK2_skl(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,definition,
( sQ8_spl
<=> element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f207,definition,
( sQ9_spl
<=> closed_subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f216,definition,
( sQ11_spl
<=> in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( ~ sQ11_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f221,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ11_spl
| ~ subset(X0,sK2_skl(powerset(the_carrier(sK0_skl))))
| ~ closed_subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f217,f186]) ).
fof(f223,plain,
( ~ sQ4_spl
| ~ sQ11_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f221,f201,f204,f207,f216,f185]) ).
fof(f224,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f199,f35]) ).
fof(f225,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f224]) ).
fof(f227,definition,
( sQ12_spl
<=> element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f229,plain,
( sQ12_spl
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f227]) ).
fof(f230,definition,
( sQ13_spl
<=> sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( ~ sQ13_spl
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f233,definition,
( sQ14_spl
<=> sK3_skl(sK11_skl(sK1_skl,sK0_skl)) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ14_spl
| sK3_skl(sK11_skl(sK1_skl,sK0_skl)) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,definition,
( sQ15_spl
<=> in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f237,plain,
( ~ sQ15_spl
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f238,plain,
( sQ15_spl
| ~ in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f239,definition,
( sQ16_spl
<=> in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f242,definition,
! [X0] :
( sQ17_spl
<=> ( ~ closed_subset(X0,sK0_skl)
| X0 != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f243,plain,
! [X0] :
( ~ sQ17_spl
| ~ closed_subset(X0,sK0_skl)
| X0 != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f246,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f229,f37]) ).
fof(f247,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f246]) ).
fof(f248,plain,
! [X0] :
( ~ sQ2_spl
| sK15_skl(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl) = sK10_skl(X0,sK0_skl)
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f190,f146]) ).
fof(f249,plain,
! [X0] :
( ~ sQ2_spl
| sK14_skl(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl) = sK9_skl(X0,sK0_skl)
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f190,f141]) ).
fof(f250,plain,
! [X0] :
( ~ sQ2_spl
| sK8_skl(X0,sK0_skl) = sK10_skl(X0,sK0_skl)
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f190,f144]) ).
fof(f251,plain,
! [X0] :
( ~ sQ2_spl
| sK8_skl(X0,sK0_skl) = sK9_skl(X0,sK0_skl)
| sK3_skl(sK11_skl(X0,sK0_skl)) = sK2_skl(sK11_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK11_skl(X0,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f190,f139]) ).
fof(f255,plain,
( sQ15_spl
| sK3_skl(sK11_skl(sK1_skl,sK0_skl)) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f238,f40]) ).
fof(f256,plain,
( ~ sQ7_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f202,f42]) ).
fof(f257,plain,
( ~ sQ7_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f202,f113]) ).
fof(f258,definition,
( sQ18_spl
<=> in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f259,plain,
( ~ sQ18_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f261,plain,
( ~ sQ7_spl
| sQ11_spl
| sQ18_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f256,f227,f230,f258,f216,f201]) ).
fof(f262,definition,
( sQ19_spl
<=> sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( ~ sQ19_spl
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f264,plain,
( sQ19_spl
| ~ sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,definition,
( sQ20_spl
<=> in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( ~ sQ20_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,plain,
( ~ sQ7_spl
| sQ20_spl
| sQ19_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f257,f204,f262,f265,f201]) ).
fof(f271,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK14_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f172,f131]) ).
fof(f277,definition,
! [X0,X1] :
( sQ21_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK14_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f280,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f271,f277,f197,f158,f161]) ).
fof(f317,definition,
( sQ33_spl
<=> sK12_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f318,plain,
( ~ sQ33_spl
| sK12_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f317]) ).
fof(f323,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK15_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f173,f131]) ).
fof(f329,definition,
! [X0,X1] :
( sQ34_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK15_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f332,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f323,f329,f197,f158,f161]) ).
fof(f350,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK13_skl(X0,X1,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK13_skl(X0,X1,sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f243,f133]) ).
fof(f352,plain,
( ~ sQ17_spl
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK7_skl(sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK7_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f243,f121]) ).
fof(f355,definition,
! [X0,X1] :
( sQ39_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK13_skl(X0,X1,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK13_skl(X0,X1,sK0_skl),powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f356,plain,
! [X0,X1] :
( ~ sQ39_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK13_skl(X0,X1,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK13_skl(X0,X1,sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f358,plain,
( ~ sQ17_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f350,f355,f197,f158,f242]) ).
fof(f360,definition,
( sQ40_spl
<=> element(sK7_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( sQ40_spl
| ~ element(sK7_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f360]) ).
fof(f363,definition,
( sQ41_spl
<=> sK7_skl(sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f366,plain,
( ~ sQ17_spl
| ~ sQ0_spl
| ~ sQ6_spl
| ~ sQ41_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f352,f360,f363,f197,f158,f242]) ).
fof(f368,plain,
( ~ sQ14_spl
| closed_subset(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK0_skl)
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f234,f41]) ).
fof(f369,plain,
( ~ sQ14_spl
| element(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f234,f39]) ).
fof(f370,definition,
( sQ42_spl
<=> closed_subset(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f371,plain,
( ~ sQ42_spl
| closed_subset(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK0_skl) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f373,plain,
( ~ sQ14_spl
| sQ42_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f368,f236,f370,f233]) ).
fof(f374,definition,
( sQ43_spl
<=> element(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( ~ sQ14_spl
| sQ43_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f369,f236,f374,f233]) ).
fof(f380,plain,
( ~ sQ13_spl
| sK8_skl(sK1_skl,sK0_skl) = sK10_skl(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f231,f144]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK15_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ),
inference(resolution,[status(thm)],[f248,f131]) ).
fof(f392,definition,
! [X0,X1] :
( sQ44_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK15_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f395,plain,
( ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f386,f392,f197,f158,f175]) ).
fof(f408,definition,
( sQ48_spl
<=> sK13_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( ~ sQ48_spl
| sK13_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f408]) ).
fof(f414,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK14_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ),
inference(resolution,[status(thm)],[f249,f131]) ).
fof(f420,definition,
! [X0,X1] :
( sQ49_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK14_skl(sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f423,plain,
( ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f414,f420,f197,f158,f175]) ).
fof(f430,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ),
inference(resolution,[status(thm)],[f250,f131]) ).
fof(f436,definition,
! [X0,X1] :
( sQ50_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK10_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f430,f436,f197,f158,f175]) ).
fof(f458,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ),
inference(resolution,[status(thm)],[f251,f131]) ).
fof(f464,definition,
! [X0,X1] :
( sQ55_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK8_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK9_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)
| sK3_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)),sK13_skl(X0,X1,sK0_skl),sK0_skl) = sK2_skl(sK11_skl(sK13_skl(X0,X1,sK0_skl),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f458,f464,f197,f158,f175]) ).
fof(f484,plain,
( sQ40_spl
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f362,f120]) ).
fof(f485,plain,
( sQ40_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f484,f197,f158,f360]) ).
fof(f486,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ42_spl
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl))
| ~ subset(X0,sK2_skl(sK11_skl(sK1_skl,sK0_skl)))
| ~ element(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f371,f192]) ).
fof(f487,definition,
! [X0] :
( sQ60_spl
<=> ( ~ subset(X0,sK2_skl(sK11_skl(sK1_skl,sK0_skl)))
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f488,plain,
! [X0] :
( ~ sQ60_spl
| ~ subset(X0,sK2_skl(sK11_skl(sK1_skl,sK0_skl)))
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,plain,
( ~ sQ4_spl
| ~ sQ42_spl
| sQ15_spl
| ~ sQ43_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f486,f487,f374,f236,f370,f185]) ).
fof(f491,plain,
( ~ sQ2_spl
| ~ sQ20_spl
| sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl)))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f266,f176]) ).
fof(f492,plain,
( ~ sQ3_spl
| ~ sQ20_spl
| subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f266,f181]) ).
fof(f493,plain,
( ~ sQ1_spl
| ~ sQ20_spl
| sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl)))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f266,f162]) ).
fof(f495,definition,
( sQ61_spl
<=> sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f496,plain,
( ~ sQ61_spl
| sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f495]) ).
fof(f498,plain,
( ~ sQ2_spl
| ~ sQ20_spl
| sQ61_spl
| sQ19_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f491,f204,f262,f495,f265,f175]) ).
fof(f499,definition,
( sQ62_spl
<=> subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( ~ sQ3_spl
| ~ sQ20_spl
| sQ62_spl
| sQ19_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f492,f204,f262,f499,f265,f180]) ).
fof(f503,definition,
( sQ63_spl
<=> sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( ~ sQ63_spl
| sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f503]) ).
fof(f506,plain,
( ~ sQ1_spl
| ~ sQ20_spl
| sQ63_spl
| sQ19_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f493,f204,f262,f503,f265,f161]) ).
fof(f507,plain,
( ~ sQ19_spl
| sK15_skl(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
inference(resolution,[status(thm)],[f263,f146]) ).
fof(f513,plain,
( ~ sQ2_spl
| ~ sQ18_spl
| sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl)))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f259,f176]) ).
fof(f514,plain,
( ~ sQ3_spl
| ~ sQ18_spl
| subset(sK1_skl,sK2_skl(powerset(the_carrier(sK0_skl))))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f259,f181]) ).
fof(f515,plain,
( ~ sQ1_spl
| ~ sQ18_spl
| sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl)))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f259,f162]) ).
fof(f517,definition,
( sQ64_spl
<=> sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( ~ sQ64_spl
| sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f520,plain,
( ~ sQ2_spl
| ~ sQ18_spl
| sQ64_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f513,f227,f230,f517,f258,f175]) ).
fof(f521,definition,
( sQ65_spl
<=> subset(sK1_skl,sK2_skl(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f522,plain,
( ~ sQ65_spl
| subset(sK1_skl,sK2_skl(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,plain,
( ~ sQ3_spl
| ~ sQ18_spl
| sQ65_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f514,f227,f230,f521,f258,f180]) ).
fof(f525,definition,
( sQ66_spl
<=> sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f526,plain,
( ~ sQ66_spl
| sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f528,plain,
( ~ sQ1_spl
| ~ sQ18_spl
| sQ66_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f515,f227,f230,f525,f258,f161]) ).
fof(f534,plain,
( ~ sQ13_spl
| sP0_prd(sK8_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f380,f231]) ).
fof(f554,plain,
( ~ sQ2_spl
| ~ sQ15_spl
| sK13_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f237,f176]) ).
fof(f555,plain,
( ~ sQ3_spl
| ~ sQ15_spl
| subset(sK1_skl,sK2_skl(sK11_skl(sK1_skl,sK0_skl)))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f237,f181]) ).
fof(f556,plain,
( ~ sQ1_spl
| ~ sQ15_spl
| sK12_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f237,f162]) ).
fof(f558,plain,
( ~ sQ2_spl
| ~ sQ15_spl
| sQ48_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f554,f227,f230,f408,f236,f175]) ).
fof(f559,definition,
( sQ70_spl
<=> subset(sK1_skl,sK2_skl(sK11_skl(sK1_skl,sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( ~ sQ70_spl
| subset(sK1_skl,sK2_skl(sK11_skl(sK1_skl,sK0_skl))) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,plain,
( ~ sQ3_spl
| ~ sQ15_spl
| sQ70_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f555,f227,f230,f559,f236,f180]) ).
fof(f563,plain,
( ~ sQ1_spl
| ~ sQ15_spl
| sQ33_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f556,f227,f230,f317,f236,f161]) ).
fof(f642,plain,
! [X0] :
( ~ sQ65_spl
| ~ closed_subset(X0,sK0_skl)
| X0 != sK2_skl(powerset(the_carrier(sK0_skl)))
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f522,f43]) ).
fof(f643,definition,
! [X0] :
( sQ81_spl
<=> ( ~ closed_subset(X0,sK0_skl)
| X0 != sK2_skl(powerset(the_carrier(sK0_skl)))
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f646,plain,
( ~ sQ65_spl
| sQ81_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f642,f216,f643,f521]) ).
fof(f653,plain,
( ~ sQ13_spl
| sK8_skl(sK1_skl,sK0_skl) = sK9_skl(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f534,f139]) ).
fof(f697,plain,
( ~ sQ33_spl
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f318,f129]) ).
fof(f709,plain,
( ~ sQ33_spl
| sQ16_spl
| ~ sQ15_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f697,f197,f158,f227,f230,f236,f239,f317]) ).
fof(f713,plain,
( sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f255,f233,f236]) ).
fof(f737,plain,
! [X0] :
( ~ sQ70_spl
| ~ closed_subset(X0,sK0_skl)
| X0 != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(X0,powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f560,f43]) ).
fof(f738,plain,
( ~ sQ70_spl
| sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f737,f236,f239,f242,f559]) ).
fof(f759,plain,
( ~ sQ13_spl
| sP0_prd(sK8_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f653,f534]) ).
fof(f766,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f152]) ).
fof(f767,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f766]) ).
fof(f828,definition,
( sQ104_spl
<=> element(sK6_skl(the_carrier(sK0_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f830,plain,
( sQ104_spl
| ~ element(sK6_skl(the_carrier(sK0_skl)),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f843,plain,
( sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f830,f104]) ).
fof(f844,plain,
sQ104_spl,
inference(contradiction_clause,[status(thm)],[f843]) ).
fof(f1036,plain,
! [X0,X1] :
( ~ sQ39_spl
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK13_skl(X0,X1,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f356,f131]) ).
fof(f1037,definition,
! [X0,X1] :
( sQ144_spl
<=> ( ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X0,sK11_skl(X1,sK0_skl))
| sP0_prd(sK10_skl(X1,sK0_skl),sK9_skl(X1,sK0_skl),sK8_skl(X1,sK0_skl),X1,sK0_skl)
| ~ element(X1,powerset(the_carrier(sK0_skl)))
| sK13_skl(X0,X1,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( ~ sQ39_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f1036,f1037,f197,f158,f355]) ).
fof(f1083,plain,
( ~ sQ48_spl
| ~ sQ39_spl
| ~ in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| sK13_skl(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f409,f356]) ).
fof(f1085,plain,
( ~ sQ48_spl
| element(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f409,f131]) ).
fof(f1086,plain,
( ~ sQ39_spl
| ~ sQ15_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ48_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1083,f374,f408,f227,f230,f236,f355]) ).
fof(f1088,plain,
( ~ sQ48_spl
| sQ43_spl
| ~ sQ15_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1085,f197,f158,f227,f230,f236,f374,f408]) ).
fof(f1338,plain,
! [X0] :
( ~ sQ63_spl
| ~ sQ5_spl
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ subset(X0,sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| ~ closed_subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),powerset(the_carrier(sK0_skl)))
| in(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f504,f195]) ).
fof(f1339,plain,
( ~ sQ63_spl
| ~ in(powerset(the_carrier(sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))))
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f504,f156]) ).
fof(f1341,definition,
! [X0] :
( sQ177_spl
<=> ( ~ subset(X0,sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| in(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1344,definition,
( sQ178_spl
<=> element(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1347,plain,
( ~ sQ63_spl
| ~ sQ5_spl
| ~ sQ20_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ178_spl
| sQ177_spl ),
inference(split_clause,[status(thm)],[f1338,f1341,f1344,f207,f204,f262,f265,f194,f503]) ).
fof(f1348,definition,
( sQ179_spl
<=> in(powerset(the_carrier(sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1351,plain,
( ~ sQ63_spl
| ~ sQ179_spl
| ~ sQ20_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1339,f197,f158,f204,f262,f265,f1348,f503]) ).
fof(f1440,plain,
( ~ sQ2_spl
| sQ19_spl
| sK3_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sK13_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f264,f190]) ).
fof(f1441,plain,
( ~ sQ1_spl
| sQ19_spl
| sK3_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f264,f167]) ).
fof(f1442,definition,
( sQ195_spl
<=> sK13_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1443,plain,
( ~ sQ195_spl
| sK13_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
inference(component_clause,[status(thm)],[f1442]) ).
fof(f1445,definition,
( sQ196_spl
<=> sK3_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1446,plain,
( ~ sQ196_spl
| sK3_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
inference(component_clause,[status(thm)],[f1445]) ).
fof(f1448,plain,
( ~ sQ2_spl
| sQ19_spl
| sQ196_spl
| sQ195_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1440,f204,f1442,f1445,f262,f175]) ).
fof(f1449,definition,
( sQ197_spl
<=> sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f1450,plain,
( ~ sQ197_spl
| sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
inference(component_clause,[status(thm)],[f1449]) ).
fof(f1452,plain,
( ~ sQ1_spl
| sQ19_spl
| sQ196_spl
| sQ197_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1441,f204,f1449,f1445,f262,f161]) ).
fof(f1453,plain,
( ~ sQ61_spl
| ~ sQ39_spl
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f496,f356]) ).
fof(f1454,plain,
( ~ sQ61_spl
| closed_subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f496,f133]) ).
fof(f1456,definition,
( sQ198_spl
<=> sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1459,plain,
( ~ sQ61_spl
| ~ sQ39_spl
| ~ sQ20_spl
| sQ19_spl
| ~ sQ198_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1453,f204,f1456,f262,f265,f355,f495]) ).
fof(f1460,plain,
( ~ sQ61_spl
| sQ9_spl
| ~ sQ20_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1454,f197,f158,f204,f262,f265,f207,f495]) ).
fof(f1462,plain,
! [X0] :
( ~ sQ66_spl
| ~ sQ5_spl
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ subset(X0,sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl))
| ~ closed_subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))
| in(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f526,f195]) ).
fof(f1463,plain,
( ~ sQ66_spl
| ~ in(powerset(the_carrier(sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))))
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f526,f156]) ).
fof(f1464,plain,
( ~ sQ66_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f526,f129]) ).
fof(f1465,definition,
! [X0] :
( sQ199_spl
<=> ( ~ subset(X0,sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl))
| in(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1468,definition,
( sQ200_spl
<=> element(sK12_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f1471,plain,
( ~ sQ66_spl
| ~ sQ5_spl
| ~ sQ18_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ9_spl
| ~ sQ200_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f1462,f1465,f1468,f207,f227,f230,f258,f194,f525]) ).
fof(f1472,plain,
( ~ sQ66_spl
| ~ sQ179_spl
| ~ sQ18_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1463,f197,f158,f227,f230,f258,f1348,f525]) ).
fof(f1473,plain,
( ~ sQ66_spl
| sQ11_spl
| ~ sQ18_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1464,f197,f158,f227,f230,f258,f216,f525]) ).
fof(f1474,plain,
( ~ sQ64_spl
| ~ sQ39_spl
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f518,f356]) ).
fof(f1475,plain,
( ~ sQ64_spl
| closed_subset(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f518,f133]) ).
fof(f1476,plain,
( ~ sQ64_spl
| element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(powerset(the_carrier(sK0_skl))),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f518,f131]) ).
fof(f1477,definition,
( sQ201_spl
<=> sK13_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK1_skl,sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1480,plain,
( ~ sQ64_spl
| ~ sQ39_spl
| ~ sQ18_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ201_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1474,f204,f1477,f227,f230,f258,f355,f517]) ).
fof(f1481,plain,
( ~ sQ64_spl
| sQ9_spl
| ~ sQ18_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1475,f197,f158,f227,f230,f258,f207,f517]) ).
fof(f1482,plain,
( ~ sQ64_spl
| sQ8_spl
| ~ sQ18_spl
| sQ13_spl
| ~ sQ12_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1476,f197,f158,f227,f230,f258,f204,f517]) ).
fof(f1524,plain,
( ~ sQ196_spl
| closed_subset(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK0_skl)
| in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1446,f41]) ).
fof(f1525,plain,
( ~ sQ196_spl
| element(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1446,f39]) ).
fof(f1526,definition,
( sQ209_spl
<=> in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1529,definition,
( sQ210_spl
<=> closed_subset(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f1532,plain,
( ~ sQ196_spl
| sQ210_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f1524,f1526,f1529,f1445]) ).
fof(f1533,definition,
( sQ211_spl
<=> element(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f1536,plain,
( ~ sQ196_spl
| sQ211_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f1525,f1526,f1533,f1445]) ).
fof(f1576,plain,
! [X0] :
( ~ sQ197_spl
| ~ sQ5_spl
| ~ in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ subset(X0,sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| ~ closed_subset(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK0_skl)
| ~ element(sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),powerset(the_carrier(sK0_skl)))
| in(sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f1450,f195]) ).
fof(f1577,plain,
( ~ sQ197_spl
| ~ in(powerset(the_carrier(sK0_skl)),sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1450,f156]) ).
fof(f1578,plain,
( ~ sQ197_spl
| in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1450,f129]) ).
fof(f1579,definition,
! [X0] :
( sQ220_spl
<=> ( ~ subset(X0,sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| in(sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK11_skl(X0,sK0_skl))
| sP0_prd(sK10_skl(X0,sK0_skl),sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f1582,definition,
( sQ221_spl
<=> element(sK12_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f1585,plain,
( ~ sQ197_spl
| ~ sQ5_spl
| ~ sQ209_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ210_spl
| ~ sQ221_spl
| sQ220_spl ),
inference(split_clause,[status(thm)],[f1576,f1579,f1582,f1529,f204,f262,f1526,f194,f1449]) ).
fof(f1586,definition,
( sQ222_spl
<=> in(powerset(the_carrier(sK0_skl)),sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f1589,plain,
( ~ sQ197_spl
| ~ sQ222_spl
| ~ sQ209_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1577,f197,f158,f204,f262,f1526,f1586,f1449]) ).
fof(f1590,definition,
( sQ223_spl
<=> in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( ~ sQ197_spl
| sQ223_spl
| ~ sQ209_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1578,f197,f158,f204,f262,f1526,f1590,f1449]) ).
fof(f1624,plain,
( ~ sQ195_spl
| ~ sQ39_spl
| ~ in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| sK13_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) != sK2_skl(sK11_skl(sK1_skl,sK0_skl))
| ~ element(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),powerset(the_carrier(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f1443,f356]) ).
fof(f1625,plain,
( ~ sQ195_spl
| closed_subset(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK0_skl)
| ~ in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1443,f133]) ).
fof(f1626,plain,
( ~ sQ195_spl
| element(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl))
| sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)
| ~ element(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1443,f131]) ).
fof(f1627,definition,
( sQ224_spl
<=> sK13_skl(sK2_skl(sK11_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl)),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) = sK2_skl(sK11_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f1630,plain,
( ~ sQ195_spl
| ~ sQ39_spl
| ~ sQ209_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ224_spl
| ~ sQ211_spl ),
inference(split_clause,[status(thm)],[f1624,f1533,f1627,f204,f262,f1526,f355,f1442]) ).
fof(f1631,plain,
( ~ sQ195_spl
| sQ210_spl
| ~ sQ209_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1625,f197,f158,f204,f262,f1526,f1529,f1442]) ).
fof(f1632,plain,
( ~ sQ195_spl
| sQ211_spl
| ~ sQ209_spl
| sQ19_spl
| ~ sQ8_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1626,f197,f158,f204,f262,f1526,f1533,f1442]) ).
fof(f1684,plain,
( ~ sQ19_spl
| closed_subset(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK0_skl)
| ~ sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
inference(paramodulation,[status(thm)],[f507,f147]) ).
fof(f1685,plain,
( ~ sQ19_spl
| element(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),powerset(the_carrier(sK0_skl)))
| ~ sP0_prd(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK9_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK8_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl) ),
inference(paramodulation,[status(thm)],[f507,f145]) ).
fof(f1686,definition,
( sQ232_spl
<=> closed_subset(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f1689,plain,
( sQ232_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1684,f262,f1686]) ).
fof(f1690,definition,
( sQ233_spl
<=> element(sK10_skl(sK2_skl(powerset(the_carrier(sK0_skl))),sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f1693,plain,
( sQ233_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1685,f262,f1690]) ).
fof(f1698,plain,
( ~ sQ60_spl
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl))
| in(sK2_skl(sK11_skl(sK1_skl,sK0_skl)),sK11_skl(sK1_skl,sK0_skl))
| sP0_prd(sK10_skl(sK1_skl,sK0_skl),sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f488,f42]) ).
fof(f1701,plain,
( ~ sQ60_spl
| sQ15_spl
| sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1698,f227,f230,f236,f487]) ).
fof(f1710,plain,
$false,
inference(sat_refutation,[status(thm)],[f164,f166,f178,f183,f188,f200,f223,f225,f247,f261,f268,f280,f332,f358,f366,f373,f377,f395,f423,f439,f467,f485,f490,f498,f502,f506,f520,f524,f528,f558,f562,f563,f646,f709,f713,f738,f767,f844,f1040,f1086,f1088,f1347,f1351,f1448,f1452,f1459,f1460,f1471,f1472,f1473,f1480,f1481,f1482,f1532,f1536,f1585,f1589,f1593,f1630,f1631,f1632,f1689,f1693,f1701]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU314+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n017.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 21 06:06:11 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.19/0.43 % Drodi V4.1.1
% 0.19/0.65 % Refutation found
% 0.19/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/0.70 % Elapsed time: 0.269074 seconds
% 0.19/0.70 % CPU time: 1.480566 seconds
% 0.19/0.70 % Total memory used: 110.437 MB
% 0.19/0.70 % Net memory used: 109.629 MB
%------------------------------------------------------------------------------