Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SEU388+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n020.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 02:22:30 PM UTC 2026

% Result   : Theorem 0.07s 0.47s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SEU388+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.36  % Computer : n020.cluster.edu
% 0.07/0.36  % Model    : x86_64 x86_64
% 0.07/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36  % Memory   : 8046.5625MB
% 0.07/0.36  % OS       : Linux 6.8.0-71-generic
% 0.07/0.36  % CPULimit : 300
% 0.07/0.36  % WCLimit  : 300
% 0.07/0.36  % DateTime : Mon Sep 21 06:19:19 UTC 2026
% 0.07/0.36  % CPUTime  : 
% 0.07/0.38  % Drodi V4.1.1
% 0.07/0.47  % Refutation found
% 0.07/0.47  % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.47  % SZS output start CNFRefutation for theBenchmark
% 0.07/0.47  fof(f1,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( strict_rel_str(A)=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f3,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( ( ~ empty_carrier(A)& reflexive_relstr(A)& complete_relstr(A) )=> ( ~ empty_carrier(A)& reflexive_relstr(A)& up_complete_relstr(A)& join_complete_relstr(A) ) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f12,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( empty(B)=> ( open_subset(B,A)& closed_subset(B,A) ) ) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f13,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( ( ~ empty_carrier(A)& complete_relstr(A) )=> ( ~ empty_carrier(A)& with_suprema_relstr(A)& with_infima_relstr(A) ) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f14,axiom,(
% 0.07/0.47    (! [A] :( finite(A)=> (! [B] :( element(B,powerset(A))=> finite(B) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f16,axiom,(
% 0.07/0.47    (! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( empty(B)=> boundary_set(B,A) ) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f18,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( empty(B)=> nowhere_dense(B,A) ) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f19,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( ( ~ empty_carrier(A)& complete_relstr(A) )=> ( ~ empty_carrier(A)& bounded_relstr(A) ) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f20,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( nowhere_dense(B,A)=> boundary_set(B,A) ) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f21,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( bounded_relstr(A)=> ( lower_bounded_relstr(A)& upper_bounded_relstr(A) ) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f22,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( ( closed_subset(B,A)& boundary_set(B,A) )=> ( boundary_set(B,A)& nowhere_dense(B,A) ) ) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f24,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( ( lower_bounded_relstr(A)& upper_bounded_relstr(A) )=> bounded_relstr(A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f25,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( ( open_subset(B,A)& nowhere_dense(B,A) )=> ( empty(B)& open_subset(B,A)& closed_subset(B,A)& v1_membered(B)& v2_membered(B)& v3_membered(B)& v4_membered(B)& v5_membered(B)& boundary_set(B,A)& nowhere_dense(B,A) ) ) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f26,axiom,(
% 0.07/0.47    (! [A] :( rel_str(A)=> ( ( reflexive_relstr(A)& with_suprema_relstr(A)& up_complete_relstr(A) )=> ( ~ empty_carrier(A)& reflexive_relstr(A)& with_suprema_relstr(A)& upper_bounded_relstr(A) ) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f27,axiom,(
% 0.07/0.47    (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( element(B,the_carrier(A))=> neighborhood_system(A,B) = a_2_0_yellow19(A,B) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f30,axiom,(
% 0.07/0.47    (! [A,B] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A)& element(B,the_carrier(A)) )=> element(neighborhood_system(A,B),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f32,axiom,(
% 0.07/0.47    (! [A] :( one_sorted_str(A)=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f36,axiom,(
% 0.07/0.47    (! [A] :( top_str(A)=> one_sorted_str(A) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f38,axiom,(
% 0.07/0.47    (! [A,B] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A)& element(B,the_carrier(A)) )=> (! [C] :( point_neighbourhood(C,A,B)=> element(C,powerset(the_carrier(A))) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f45,axiom,(
% 0.07/0.47    (? [A] : top_str(A) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f47,axiom,(
% 0.07/0.47    (! [A,B] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A)& element(B,the_carrier(A)) )=> (? [C] : point_neighbourhood(C,A,B) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f49,axiom,(
% 0.07/0.47    (! [A] :(? [B] : element(B,A) ))),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f53,axiom,(
% 0.07/0.47    (! [A] :( ( ~ empty_carrier(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& lower_relstr_subset(cast_as_carrier_subset(A),A)& upper_relstr_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f55,axiom,(
% 0.07/0.47    (! [A] : ~ empty(powerset(A)) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f56,axiom,(
% 0.07/0.47    (! [A] :( ~ empty_carrier(boole_POSet(A))& strict_rel_str(boole_POSet(A))& reflexive_relstr(boole_POSet(A))& transitive_relstr(boole_POSet(A))& antisymmetric_relstr(boole_POSet(A))& lower_bounded_relstr(boole_POSet(A))& upper_bounded_relstr(boole_POSet(A))& bounded_relstr(boole_POSet(A))& up_complete_relstr(boole_POSet(A))& join_complete_relstr(boole_POSet(A))& ~ v1_yellow_3(boole_POSet(A))& distributive_relstr(boole_POSet(A))& heyting_relstr(boole_POSet(A))& complemented_relstr(boole_POSet(A))& boolean_relstr(boole_POSet(A))& with_suprema_relstr(boole_POSet(A))& with_infima_relstr(boole_POSet(A))& complete_relstr(boole_POSet(A)) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f58,axiom,(
% 0.07/0.47    (! [A] :( ( with_suprema_relstr(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& directed_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f61,axiom,(
% 0.07/0.47    (! [A] :( ( ~ empty_carrier(A)& upper_bounded_relstr(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& directed_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f64,axiom,(
% 0.07/0.47    (! [A] :( ( with_infima_relstr(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& filtered_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f65,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> closed_subset(cast_as_carrier_subset(A),A) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f66,axiom,(
% 0.07/0.47    (! [A] :( ( ~ empty_carrier(A)& lower_bounded_relstr(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& filtered_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f68,axiom,(
% 0.07/0.47    (! [A] :( ( topological_space(A)& top_str(A) )=> ( open_subset(cast_as_carrier_subset(A),A)& closed_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f72,axiom,(
% 0.07/0.47    (! [A,B,C] :( ( ~ empty_carrier(B)& topological_space(B)& top_str(B)& element(C,the_carrier(B)) )=> ( in(A,a_2_0_yellow19(B,C))<=> (? [D] :( point_neighbourhood(D,B,C)& A = D ) )) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f74,axiom,(
% 0.07/0.47    (! [A] :( ( ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& rel_str(A) )=> (? [B] :( element(B,powerset(the_carrier(A)))& ~ empty(B)& filtered_subset(B,A)& upper_relstr_subset(B,A) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f75,axiom,(
% 0.07/0.47    (! [A] :( ( reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& with_suprema_relstr(A)& with_infima_relstr(A)& rel_str(A) )=> (? [B] :( element(B,powerset(the_carrier(A)))& ~ empty(B)& directed_subset(B,A)& filtered_subset(B,A)& lower_relstr_subset(B,A)& upper_relstr_subset(B,A) ) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f76,axiom,(
% 0.07/0.47    (? [A] :( rel_str(A)& ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& connected_relstr(A) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f77,axiom,(
% 0.07/0.47    (? [A] :( rel_str(A)& ~ empty_carrier(A)& strict_rel_str(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& with_suprema_relstr(A)& with_infima_relstr(A)& complete_relstr(A)& lower_bounded_relstr(A)& upper_bounded_relstr(A)& bounded_relstr(A)& up_complete_relstr(A)& join_complete_relstr(A) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f79,axiom,(
% 0.07/0.47    (? [A] :( rel_str(A)& ~ empty_carrier(A)& strict_rel_str(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& complete_relstr(A) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f84,axiom,(
% 0.07/0.47    (? [A] :( rel_str(A)& ~ empty_carrier(A)& ~ trivial_carrier(A)& strict_rel_str(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& upper_bounded_relstr(A)& bounded_relstr(A)& ~ v1_yellow_3(A)& distributive_relstr(A)& heyting_relstr(A)& complemented_relstr(A)& boolean_relstr(A)& with_suprema_relstr(A)& with_infima_relstr(A) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f111,axiom,(
% 0.07/0.47    (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f114,conjecture,(
% 0.07/0.47    (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( in(C,neighborhood_system(A,B))<=> point_neighbourhood(C,A,B) ) )) )) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f115,negated_conjecture,(
% 0.07/0.47    ~((! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( in(C,neighborhood_system(A,B))<=> point_neighbourhood(C,A,B) ) )) )) ))),
% 0.07/0.47    inference(negated_conjecture,[status(cth)],[f114])).
% 0.07/0.47  fof(f116,axiom,(
% 0.07/0.47    (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f117,axiom,(
% 0.07/0.47    (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f119,axiom,(
% 0.07/0.47    (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 0.07/0.47    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.47  fof(f121,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|(~strict_rel_str(A)|A=rel_str_of(the_carrier(A),the_InternalRel(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.07/0.47  fof(f122,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|~strict_rel_str(X0)|X0=rel_str_of(the_carrier(X0),the_InternalRel(X0)))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f121])).
% 0.07/0.47  fof(f125,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|(((empty_carrier(A)|~reflexive_relstr(A))|~complete_relstr(A))|(((~empty_carrier(A)&reflexive_relstr(A))&up_complete_relstr(A))&join_complete_relstr(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.07/0.47  fof(f128,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|empty_carrier(X0)|~reflexive_relstr(X0)|~complete_relstr(X0)|up_complete_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f125])).
% 0.07/0.47  fof(f129,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|empty_carrier(X0)|~reflexive_relstr(X0)|~complete_relstr(X0)|join_complete_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f125])).
% 0.07/0.47  fof(f165,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|(~empty(B)|(open_subset(B,A)&closed_subset(B,A))))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.07/0.47  fof(f166,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~empty(X1)|open_subset(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f165])).
% 0.07/0.47  fof(f167,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~empty(X1)|closed_subset(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f165])).
% 0.07/0.47  fof(f168,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|((empty_carrier(A)|~complete_relstr(A))|((~empty_carrier(A)&with_suprema_relstr(A))&with_infima_relstr(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.07/0.47  fof(f170,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|empty_carrier(X0)|~complete_relstr(X0)|with_suprema_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f168])).
% 0.07/0.47  fof(f171,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|empty_carrier(X0)|~complete_relstr(X0)|with_infima_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f168])).
% 0.07/0.47  fof(f172,plain,(
% 0.07/0.47    ![A]: (~finite(A)|(![B]: (~element(B,powerset(A))|finite(B))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.07/0.47  fof(f173,plain,(
% 0.07/0.47    ![X0,X1]: (~finite(X0)|~element(X1,powerset(X0))|finite(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f172])).
% 0.07/0.47  fof(f176,plain,(
% 0.07/0.47    ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|(~empty(B)|boundary_set(B,A)))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.07/0.47  fof(f177,plain,(
% 0.07/0.47    ![X0,X1]: (~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~empty(X1)|boundary_set(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f176])).
% 0.07/0.47  fof(f184,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|(~empty(B)|nowhere_dense(B,A)))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.07/0.47  fof(f185,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~empty(X1)|nowhere_dense(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f184])).
% 0.07/0.47  fof(f186,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|((empty_carrier(A)|~complete_relstr(A))|(~empty_carrier(A)&bounded_relstr(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.07/0.47  fof(f188,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|empty_carrier(X0)|~complete_relstr(X0)|bounded_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f186])).
% 0.07/0.47  fof(f189,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|(~nowhere_dense(B,A)|boundary_set(B,A)))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.07/0.47  fof(f190,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~nowhere_dense(X1,X0)|boundary_set(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f189])).
% 0.07/0.47  fof(f191,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|(~bounded_relstr(A)|(lower_bounded_relstr(A)&upper_bounded_relstr(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.07/0.47  fof(f193,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|~bounded_relstr(X0)|upper_bounded_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f191])).
% 0.07/0.47  fof(f194,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|((~closed_subset(B,A)|~boundary_set(B,A))|(boundary_set(B,A)&nowhere_dense(B,A))))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.07/0.47  fof(f196,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~closed_subset(X1,X0)|~boundary_set(X1,X0)|nowhere_dense(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f194])).
% 0.07/0.47  fof(f201,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|((~lower_bounded_relstr(A)|~upper_bounded_relstr(A))|bounded_relstr(A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.07/0.47  fof(f202,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|~lower_bounded_relstr(X0)|~upper_bounded_relstr(X0)|bounded_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f201])).
% 0.07/0.47  fof(f203,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|((~open_subset(B,A)|~nowhere_dense(B,A))|(((((((((empty(B)&open_subset(B,A))&closed_subset(B,A))&v1_membered(B))&v2_membered(B))&v3_membered(B))&v4_membered(B))&v5_membered(B))&boundary_set(B,A))&nowhere_dense(B,A))))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.07/0.47  fof(f204,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|empty(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f206,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|closed_subset(X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f207,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|v1_membered(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f208,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|v2_membered(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f209,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|v3_membered(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f210,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|v4_membered(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f211,plain,(
% 0.07/0.47    ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~open_subset(X1,X0)|~nowhere_dense(X1,X0)|v5_membered(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f203])).
% 0.07/0.47  fof(f214,plain,(
% 0.07/0.47    ![A]: (~rel_str(A)|(((~reflexive_relstr(A)|~with_suprema_relstr(A))|~up_complete_relstr(A))|(((~empty_carrier(A)&reflexive_relstr(A))&with_suprema_relstr(A))&upper_bounded_relstr(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.07/0.47  fof(f218,plain,(
% 0.07/0.47    ![X0]: (~rel_str(X0)|~reflexive_relstr(X0)|~with_suprema_relstr(X0)|~up_complete_relstr(X0)|upper_bounded_relstr(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f214])).
% 0.07/0.47  fof(f219,plain,(
% 0.07/0.47    ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: (~element(B,the_carrier(A))|neighborhood_system(A,B)=a_2_0_yellow19(A,B))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.07/0.47  fof(f220,plain,(
% 0.07/0.47    ![X0,X1]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|neighborhood_system(X0,X1)=a_2_0_yellow19(X0,X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f219])).
% 0.07/0.47  fof(f224,plain,(
% 0.07/0.47    ![A,B]: ((((empty_carrier(A)|~topological_space(A))|~top_str(A))|~element(B,the_carrier(A)))|element(neighborhood_system(A,B),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.07/0.47  fof(f225,plain,(
% 0.07/0.47    ![X0,X1]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|element(neighborhood_system(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f224])).
% 0.07/0.47  fof(f226,plain,(
% 0.07/0.47    ![A]: (~one_sorted_str(A)|element(cast_as_carrier_subset(A),powerset(the_carrier(A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.07/0.47  fof(f227,plain,(
% 0.07/0.47    ![X0]: (~one_sorted_str(X0)|element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f226])).
% 0.07/0.47  fof(f233,plain,(
% 0.07/0.47    ![A]: (~top_str(A)|one_sorted_str(A))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.07/0.47  fof(f234,plain,(
% 0.07/0.47    ![X0]: (~top_str(X0)|one_sorted_str(X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f233])).
% 0.07/0.47  fof(f235,plain,(
% 0.07/0.47    ![A,B]: ((((empty_carrier(A)|~topological_space(A))|~top_str(A))|~element(B,the_carrier(A)))|(![C]: (~point_neighbourhood(C,A,B)|element(C,powerset(the_carrier(A))))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.07/0.47  fof(f236,plain,(
% 0.07/0.47    ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|~point_neighbourhood(X2,X0,X1)|element(X2,powerset(the_carrier(X0))))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f235])).
% 0.07/0.47  fof(f243,plain,(
% 0.07/0.47    top_str(sK1_skl)),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f45])).
% 0.07/0.47  fof(f244,plain,(
% 0.07/0.47    top_str(sK1_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f243])).
% 0.07/0.47  fof(f247,plain,(
% 0.07/0.47    ![A,B]: ((((empty_carrier(A)|~topological_space(A))|~top_str(A))|~element(B,the_carrier(A)))|(?[C]: point_neighbourhood(C,A,B)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.07/0.47  fof(f248,plain,(
% 0.07/0.47    ![A,B]: ((((empty_carrier(A)|~topological_space(A))|~top_str(A))|~element(B,the_carrier(A)))|point_neighbourhood(sK3_skl(B,A),A,B))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f247])).
% 0.07/0.47  fof(f249,plain,(
% 0.07/0.47    ![X0,X1]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|point_neighbourhood(sK3_skl(X1,X0),X0,X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f248])).
% 0.07/0.47  fof(f252,plain,(
% 0.07/0.47    ![A]: element(sK5_skl(A),A)),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B,sK5_skl(A))],[f49])).
% 0.07/0.47  fof(f253,plain,(
% 0.07/0.47    ![X0]: (element(sK5_skl(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.47  fof(f261,plain,(
% 0.07/0.47    ![A]: ((empty_carrier(A)|~rel_str(A))|((~empty(cast_as_carrier_subset(A))&lower_relstr_subset(cast_as_carrier_subset(A),A))&upper_relstr_subset(cast_as_carrier_subset(A),A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.07/0.47  fof(f263,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~rel_str(X0)|lower_relstr_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f261])).
% 0.07/0.47  fof(f264,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~rel_str(X0)|upper_relstr_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f261])).
% 0.07/0.47  fof(f267,plain,(
% 0.07/0.47    ![X0]: (~empty(powerset(X0)))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f55])).
% 0.07/0.47  fof(f268,plain,(
% 0.07/0.47    (((((((((((((((((![A]: ~empty_carrier(boole_POSet(A)))&(![A]: strict_rel_str(boole_POSet(A))))&(![A]: reflexive_relstr(boole_POSet(A))))&(![A]: transitive_relstr(boole_POSet(A))))&(![A]: antisymmetric_relstr(boole_POSet(A))))&(![A]: lower_bounded_relstr(boole_POSet(A))))&(![A]: upper_bounded_relstr(boole_POSet(A))))&(![A]: bounded_relstr(boole_POSet(A))))&(![A]: up_complete_relstr(boole_POSet(A))))&(![A]: join_complete_relstr(boole_POSet(A))))&(![A]: ~v1_yellow_3(boole_POSet(A))))&(![A]: distributive_relstr(boole_POSet(A))))&(![A]: heyting_relstr(boole_POSet(A))))&(![A]: complemented_relstr(boole_POSet(A))))&(![A]: boolean_relstr(boole_POSet(A))))&(![A]: with_suprema_relstr(boole_POSet(A))))&(![A]: with_infima_relstr(boole_POSet(A))))&(![A]: complete_relstr(boole_POSet(A)))),
% 0.07/0.47    inference(miniscoping,[status(thm)],[f56])).
% 0.07/0.47  fof(f269,plain,(
% 0.07/0.47    ![X0]: (~empty_carrier(boole_POSet(X0)))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f268])).
% 0.07/0.47  fof(f289,plain,(
% 0.07/0.47    ![A]: ((~with_suprema_relstr(A)|~rel_str(A))|(~empty(cast_as_carrier_subset(A))&directed_subset(cast_as_carrier_subset(A),A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.07/0.47  fof(f291,plain,(
% 0.07/0.47    ![X0]: (~with_suprema_relstr(X0)|~rel_str(X0)|directed_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f289])).
% 0.07/0.47  fof(f314,plain,(
% 0.07/0.47    ![A]: (((empty_carrier(A)|~upper_bounded_relstr(A))|~rel_str(A))|(~empty(cast_as_carrier_subset(A))&directed_subset(cast_as_carrier_subset(A),A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.07/0.47  fof(f316,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~upper_bounded_relstr(X0)|~rel_str(X0)|directed_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f314])).
% 0.07/0.47  fof(f321,plain,(
% 0.07/0.47    ![A]: ((~with_infima_relstr(A)|~rel_str(A))|(~empty(cast_as_carrier_subset(A))&filtered_subset(cast_as_carrier_subset(A),A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.07/0.47  fof(f323,plain,(
% 0.07/0.47    ![X0]: (~with_infima_relstr(X0)|~rel_str(X0)|filtered_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f321])).
% 0.07/0.47  fof(f324,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|closed_subset(cast_as_carrier_subset(A),A))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f65])).
% 0.07/0.47  fof(f325,plain,(
% 0.07/0.47    ![X0]: (~topological_space(X0)|~top_str(X0)|closed_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f324])).
% 0.07/0.47  fof(f326,plain,(
% 0.07/0.47    ![A]: (((empty_carrier(A)|~lower_bounded_relstr(A))|~rel_str(A))|(~empty(cast_as_carrier_subset(A))&filtered_subset(cast_as_carrier_subset(A),A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f66])).
% 0.07/0.47  fof(f328,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~lower_bounded_relstr(X0)|~rel_str(X0)|filtered_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f326])).
% 0.07/0.47  fof(f335,plain,(
% 0.07/0.47    ![A]: ((~topological_space(A)|~top_str(A))|(open_subset(cast_as_carrier_subset(A),A)&closed_subset(cast_as_carrier_subset(A),A)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.07/0.47  fof(f336,plain,(
% 0.07/0.47    ![X0]: (~topological_space(X0)|~top_str(X0)|open_subset(cast_as_carrier_subset(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f335])).
% 0.07/0.47  fof(f368,plain,(
% 0.07/0.47    ![A,B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|(in(A,a_2_0_yellow19(B,C))<=>(?[D]: (point_neighbourhood(D,B,C)&A=D))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f72])).
% 0.07/0.47  fof(f369,plain,(
% 0.07/0.47    ![A,B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|((~in(A,a_2_0_yellow19(B,C))|(?[D]: (point_neighbourhood(D,B,C)&A=D)))&(in(A,a_2_0_yellow19(B,C))|(![D]: (~point_neighbourhood(D,B,C)|~A=D)))))),
% 0.07/0.47    inference(NNF_transformation,[status(thm)],[f368])).
% 0.07/0.47  fof(f370,plain,(
% 0.07/0.47    ![B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|((![A]: (~in(A,a_2_0_yellow19(B,C))|(?[D]: (point_neighbourhood(D,B,C)&A=D))))&(![A]: (in(A,a_2_0_yellow19(B,C))|(![D]: (~point_neighbourhood(D,B,C)|~A=D))))))),
% 0.07/0.47    inference(miniscoping,[status(thm)],[f369])).
% 0.07/0.47  fof(f371,plain,(
% 0.07/0.47    ![B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|((![A]: (~in(A,a_2_0_yellow19(B,C))|(point_neighbourhood(sK7_skl(A,C,B),B,C)&A=sK7_skl(A,C,B))))&(![A]: (in(A,a_2_0_yellow19(B,C))|(![D]: (~point_neighbourhood(D,B,C)|~A=D))))))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(D,sK7_skl(A,C,B))],[f370])).
% 0.07/0.47  fof(f372,plain,(
% 0.07/0.47    ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|~in(X2,a_2_0_yellow19(X0,X1))|point_neighbourhood(sK7_skl(X2,X1,X0),X0,X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f371])).
% 0.07/0.47  fof(f373,plain,(
% 0.07/0.47    ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|~in(X2,a_2_0_yellow19(X0,X1))|X2=sK7_skl(X2,X1,X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f371])).
% 0.07/0.47  fof(f374,plain,(
% 0.07/0.47    ![X0,X1,X2,X3]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|in(X2,a_2_0_yellow19(X0,X1))|~point_neighbourhood(X3,X0,X1)|~X2=X3)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f371])).
% 0.07/0.47  fof(f378,plain,(
% 0.07/0.47    ![A]: ((((empty_carrier(A)|~reflexive_relstr(A))|~transitive_relstr(A))|~rel_str(A))|(?[B]: (((element(B,powerset(the_carrier(A)))&~empty(B))&filtered_subset(B,A))&upper_relstr_subset(B,A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.07/0.47  fof(f379,plain,(
% 0.07/0.47    ![A]: ((((empty_carrier(A)|~reflexive_relstr(A))|~transitive_relstr(A))|~rel_str(A))|(((element(sK8_skl(A),powerset(the_carrier(A)))&~empty(sK8_skl(A)))&filtered_subset(sK8_skl(A),A))&upper_relstr_subset(sK8_skl(A),A)))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f378])).
% 0.07/0.47  fof(f380,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~rel_str(X0)|element(sK8_skl(X0),powerset(the_carrier(X0))))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f379])).
% 0.07/0.47  fof(f382,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~rel_str(X0)|filtered_subset(sK8_skl(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f379])).
% 0.07/0.47  fof(f383,plain,(
% 0.07/0.47    ![X0]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~rel_str(X0)|upper_relstr_subset(sK8_skl(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f379])).
% 0.07/0.47  fof(f384,plain,(
% 0.07/0.47    ![A]: ((((((~reflexive_relstr(A)|~transitive_relstr(A))|~antisymmetric_relstr(A))|~with_suprema_relstr(A))|~with_infima_relstr(A))|~rel_str(A))|(?[B]: (((((element(B,powerset(the_carrier(A)))&~empty(B))&directed_subset(B,A))&filtered_subset(B,A))&lower_relstr_subset(B,A))&upper_relstr_subset(B,A))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.07/0.47  fof(f385,plain,(
% 0.07/0.47    ![A]: ((((((~reflexive_relstr(A)|~transitive_relstr(A))|~antisymmetric_relstr(A))|~with_suprema_relstr(A))|~with_infima_relstr(A))|~rel_str(A))|(((((element(sK9_skl(A),powerset(the_carrier(A)))&~empty(sK9_skl(A)))&directed_subset(sK9_skl(A),A))&filtered_subset(sK9_skl(A),A))&lower_relstr_subset(sK9_skl(A),A))&upper_relstr_subset(sK9_skl(A),A)))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f384])).
% 0.07/0.47  fof(f386,plain,(
% 0.07/0.47    ![X0]: (~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~with_suprema_relstr(X0)|~with_infima_relstr(X0)|~rel_str(X0)|element(sK9_skl(X0),powerset(the_carrier(X0))))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f385])).
% 0.07/0.47  fof(f388,plain,(
% 0.07/0.47    ![X0]: (~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~with_suprema_relstr(X0)|~with_infima_relstr(X0)|~rel_str(X0)|directed_subset(sK9_skl(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f385])).
% 0.07/0.47  fof(f389,plain,(
% 0.07/0.47    ![X0]: (~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~with_suprema_relstr(X0)|~with_infima_relstr(X0)|~rel_str(X0)|filtered_subset(sK9_skl(X0),X0))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f385])).
% 0.07/0.47  fof(f392,plain,(
% 0.07/0.47    (((((rel_str(sK10_skl)&~empty_carrier(sK10_skl))&reflexive_relstr(sK10_skl))&transitive_relstr(sK10_skl))&antisymmetric_relstr(sK10_skl))&connected_relstr(sK10_skl))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f76])).
% 0.07/0.47  fof(f393,plain,(
% 0.07/0.47    rel_str(sK10_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f392])).
% 0.07/0.47  fof(f394,plain,(
% 0.07/0.47    ~empty_carrier(sK10_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f392])).
% 0.07/0.47  fof(f395,plain,(
% 0.07/0.47    reflexive_relstr(sK10_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f392])).
% 0.07/0.47  fof(f396,plain,(
% 0.07/0.47    transitive_relstr(sK10_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f392])).
% 0.07/0.47  fof(f399,plain,(
% 0.07/0.47    (((((((((((((rel_str(sK11_skl)&~empty_carrier(sK11_skl))&strict_rel_str(sK11_skl))&reflexive_relstr(sK11_skl))&transitive_relstr(sK11_skl))&antisymmetric_relstr(sK11_skl))&with_suprema_relstr(sK11_skl))&with_infima_relstr(sK11_skl))&complete_relstr(sK11_skl))&lower_bounded_relstr(sK11_skl))&upper_bounded_relstr(sK11_skl))&bounded_relstr(sK11_skl))&up_complete_relstr(sK11_skl))&join_complete_relstr(sK11_skl))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f77])).
% 0.07/0.47  fof(f400,plain,(
% 0.07/0.47    rel_str(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f401,plain,(
% 0.07/0.47    ~empty_carrier(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f402,plain,(
% 0.07/0.47    strict_rel_str(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f403,plain,(
% 0.07/0.47    reflexive_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f404,plain,(
% 0.07/0.47    transitive_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f405,plain,(
% 0.07/0.47    antisymmetric_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f406,plain,(
% 0.07/0.47    with_suprema_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f407,plain,(
% 0.07/0.47    with_infima_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f408,plain,(
% 0.07/0.47    complete_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f409,plain,(
% 0.07/0.47    lower_bounded_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f411,plain,(
% 0.07/0.47    bounded_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f412,plain,(
% 0.07/0.47    up_complete_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f413,plain,(
% 0.07/0.47    join_complete_relstr(sK11_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f399])).
% 0.07/0.47  fof(f417,plain,(
% 0.07/0.47    ((((((rel_str(sK13_skl)&~empty_carrier(sK13_skl))&strict_rel_str(sK13_skl))&reflexive_relstr(sK13_skl))&transitive_relstr(sK13_skl))&antisymmetric_relstr(sK13_skl))&complete_relstr(sK13_skl))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f79])).
% 0.07/0.47  fof(f418,plain,(
% 0.07/0.47    rel_str(sK13_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f417])).
% 0.07/0.47  fof(f419,plain,(
% 0.07/0.47    ~empty_carrier(sK13_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f417])).
% 0.07/0.47  fof(f420,plain,(
% 0.07/0.47    strict_rel_str(sK13_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f417])).
% 0.07/0.47  fof(f421,plain,(
% 0.07/0.47    reflexive_relstr(sK13_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f417])).
% 0.07/0.47  fof(f422,plain,(
% 0.07/0.47    transitive_relstr(sK13_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f417])).
% 0.07/0.47  fof(f424,plain,(
% 0.07/0.47    complete_relstr(sK13_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f417])).
% 0.07/0.47  fof(f441,plain,(
% 0.07/0.47    ((((((((((((((((rel_str(sK18_skl)&~empty_carrier(sK18_skl))&~trivial_carrier(sK18_skl))&strict_rel_str(sK18_skl))&reflexive_relstr(sK18_skl))&transitive_relstr(sK18_skl))&antisymmetric_relstr(sK18_skl))&lower_bounded_relstr(sK18_skl))&upper_bounded_relstr(sK18_skl))&bounded_relstr(sK18_skl))&~v1_yellow_3(sK18_skl))&distributive_relstr(sK18_skl))&heyting_relstr(sK18_skl))&complemented_relstr(sK18_skl))&boolean_relstr(sK18_skl))&with_suprema_relstr(sK18_skl))&with_infima_relstr(sK18_skl))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f84])).
% 0.07/0.47  fof(f442,plain,(
% 0.07/0.47    rel_str(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f443,plain,(
% 0.07/0.47    ~empty_carrier(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f445,plain,(
% 0.07/0.47    strict_rel_str(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f446,plain,(
% 0.07/0.47    reflexive_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f447,plain,(
% 0.07/0.47    transitive_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f448,plain,(
% 0.07/0.47    antisymmetric_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f449,plain,(
% 0.07/0.47    lower_bounded_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f450,plain,(
% 0.07/0.47    upper_bounded_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f451,plain,(
% 0.07/0.47    bounded_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f457,plain,(
% 0.07/0.47    with_suprema_relstr(sK18_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f441])).
% 0.07/0.47  fof(f608,plain,(
% 0.07/0.47    ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f111])).
% 0.07/0.47  fof(f609,plain,(
% 0.07/0.47    ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f608])).
% 0.07/0.47  fof(f619,plain,(
% 0.07/0.47    (?[A]: (((~empty_carrier(A)&topological_space(A))&top_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (in(C,neighborhood_system(A,B))<~>point_neighbourhood(C,A,B)))))))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f115])).
% 0.07/0.47  fof(f620,plain,(
% 0.07/0.47    ?[A]: (((~empty_carrier(A)&topological_space(A))&top_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: ((in(C,neighborhood_system(A,B))|point_neighbourhood(C,A,B))&(~in(C,neighborhood_system(A,B))|~point_neighbourhood(C,A,B)))))))),
% 0.07/0.47    inference(NNF_transformation,[status(thm)],[f619])).
% 0.07/0.47  fof(f621,plain,(
% 0.07/0.47    (((~empty_carrier(sK43_skl)&topological_space(sK43_skl))&top_str(sK43_skl))&(element(sK44_skl,the_carrier(sK43_skl))&((in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|point_neighbourhood(sK45_skl,sK43_skl,sK44_skl))&(~in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|~point_neighbourhood(sK45_skl,sK43_skl,sK44_skl)))))),
% 0.07/0.47    inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl,sK44_skl,sK45_skl]),skolemize(A,sK43_skl),skolemize(B,sK44_skl),skolemize(C,sK45_skl)],[f620])).
% 0.07/0.47  fof(f622,plain,(
% 0.07/0.47    ~empty_carrier(sK43_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f621])).
% 0.07/0.47  fof(f623,plain,(
% 0.07/0.47    topological_space(sK43_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f621])).
% 0.07/0.47  fof(f624,plain,(
% 0.07/0.47    top_str(sK43_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f621])).
% 0.07/0.47  fof(f625,plain,(
% 0.07/0.47    element(sK44_skl,the_carrier(sK43_skl))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f621])).
% 0.07/0.47  fof(f626,plain,(
% 0.07/0.47    in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|point_neighbourhood(sK45_skl,sK43_skl,sK44_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f621])).
% 0.07/0.47  fof(f627,plain,(
% 0.07/0.47    ~in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|~point_neighbourhood(sK45_skl,sK43_skl,sK44_skl)),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f621])).
% 0.07/0.47  fof(f628,plain,(
% 0.07/0.47    ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f116])).
% 0.07/0.47  fof(f629,plain,(
% 0.07/0.47    ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 0.07/0.47    inference(miniscoping,[status(thm)],[f628])).
% 0.07/0.47  fof(f630,plain,(
% 0.07/0.47    ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f629])).
% 0.07/0.47  fof(f631,plain,(
% 0.07/0.47    ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f117])).
% 0.07/0.47  fof(f632,plain,(
% 0.07/0.47    ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 0.07/0.47    inference(miniscoping,[status(thm)],[f631])).
% 0.07/0.47  fof(f633,plain,(
% 0.07/0.47    ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f632])).
% 0.07/0.47  fof(f636,plain,(
% 0.07/0.47    ![A,B]: (~in(A,B)|~empty(B))),
% 0.07/0.47    inference(pre_NNF_transformation,[status(thm)],[f119])).
% 0.07/0.47  fof(f637,plain,(
% 0.07/0.47    ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 0.07/0.47    inference(miniscoping,[status(thm)],[f636])).
% 0.07/0.47  fof(f638,plain,(
% 0.07/0.47    ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 0.07/0.47    inference(cnf_transformation,[status(thm)],[f637])).
% 0.07/0.47  fof(f642,definition,(
% 0.07/0.47    sQ0_spl <=> (in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f643,plain,(
% 0.07/0.47    in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|~sQ0_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f642])).
% 0.07/0.47  fof(f644,plain,(
% 0.07/0.47    ~in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|sQ0_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f642])).
% 0.07/0.47  fof(f645,definition,(
% 0.07/0.47    sQ1_spl <=> (point_neighbourhood(sK45_skl,sK43_skl,sK44_skl))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f646,plain,(
% 0.07/0.47    point_neighbourhood(sK45_skl,sK43_skl,sK44_skl)|~sQ1_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f645])).
% 0.07/0.47  fof(f648,plain,(
% 0.07/0.47    sQ0_spl|sQ1_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f626,f642,f645])).
% 0.07/0.47  fof(f649,plain,(
% 0.07/0.47    ~sQ0_spl|~sQ1_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f627,f642,f645])).
% 0.07/0.47  fof(f654,plain,(
% 0.07/0.47    ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|in(X2,a_2_0_yellow19(X0,X1))|~point_neighbourhood(X2,X0,X1))),
% 0.07/0.47    inference(destructive_equality_resolution,[status(thm)],[f374])).
% 0.07/0.47  fof(f655,plain,(
% 0.07/0.47    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|element(neighborhood_system(sK43_skl,sK44_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))),
% 0.07/0.47    inference(resolution,[status(thm)],[f625,f225])).
% 0.07/0.47  fof(f656,plain,(
% 0.07/0.47    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|neighborhood_system(sK43_skl,sK44_skl)=a_2_0_yellow19(sK43_skl,sK44_skl)),
% 0.07/0.47    inference(resolution,[status(thm)],[f625,f220])).
% 0.07/0.47  fof(f657,definition,(
% 0.07/0.47    sQ2_spl <=> (empty_carrier(sK43_skl))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f658,plain,(
% 0.07/0.47    empty_carrier(sK43_skl)|~sQ2_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f657])).
% 0.07/0.47  fof(f660,definition,(
% 0.07/0.47    sQ3_spl <=> (topological_space(sK43_skl))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f662,plain,(
% 0.07/0.47    ~topological_space(sK43_skl)|sQ3_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f660])).
% 0.07/0.47  fof(f663,definition,(
% 0.07/0.47    sQ4_spl <=> (top_str(sK43_skl))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f665,plain,(
% 0.07/0.47    ~top_str(sK43_skl)|sQ4_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f663])).
% 0.07/0.47  fof(f666,definition,(
% 0.07/0.47    sQ5_spl <=> (element(neighborhood_system(sK43_skl,sK44_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f667,plain,(
% 0.07/0.47    element(neighborhood_system(sK43_skl,sK44_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|~sQ5_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f666])).
% 0.07/0.47  fof(f669,plain,(
% 0.07/0.47    sQ2_spl|~sQ3_spl|~sQ4_spl|sQ5_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f655,f657,f660,f663,f666])).
% 0.07/0.47  fof(f670,definition,(
% 0.07/0.47    sQ6_spl <=> (neighborhood_system(sK43_skl,sK44_skl)=a_2_0_yellow19(sK43_skl,sK44_skl))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f671,plain,(
% 0.07/0.47    neighborhood_system(sK43_skl,sK44_skl)=a_2_0_yellow19(sK43_skl,sK44_skl)|~sQ6_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f670])).
% 0.07/0.47  fof(f673,plain,(
% 0.07/0.47    sQ2_spl|~sQ3_spl|~sQ4_spl|sQ6_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f656,f657,f660,f663,f670])).
% 0.07/0.47  fof(f674,plain,(
% 0.07/0.47    $false|sQ4_spl),
% 0.07/0.47    inference(forward_subsumption_resolution,[status(thm)],[f665,f624])).
% 0.07/0.47  fof(f675,plain,(
% 0.07/0.47    sQ4_spl),
% 0.07/0.47    inference(contradiction_clause,[status(thm)],[f674])).
% 0.07/0.47  fof(f676,plain,(
% 0.07/0.47    $false|sQ3_spl),
% 0.07/0.47    inference(forward_subsumption_resolution,[status(thm)],[f662,f623])).
% 0.07/0.47  fof(f677,plain,(
% 0.07/0.47    sQ3_spl),
% 0.07/0.47    inference(contradiction_clause,[status(thm)],[f676])).
% 0.07/0.47  fof(f678,plain,(
% 0.07/0.47    $false|~sQ2_spl),
% 0.07/0.47    inference(forward_subsumption_resolution,[status(thm)],[f658,f622])).
% 0.07/0.47  fof(f679,plain,(
% 0.07/0.47    ~sQ2_spl),
% 0.07/0.47    inference(contradiction_clause,[status(thm)],[f678])).
% 0.07/0.47  fof(f684,plain,(
% 0.07/0.47    empty(the_carrier(sK43_skl))|in(sK44_skl,the_carrier(sK43_skl))),
% 0.07/0.47    inference(resolution,[status(thm)],[f609,f625])).
% 0.07/0.47  fof(f685,definition,(
% 0.07/0.47    sQ7_spl <=> (empty(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f689,definition,(
% 0.07/0.47    sQ8_spl <=> (empty(the_carrier(sK43_skl)))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f690,plain,(
% 0.07/0.47    empty(the_carrier(sK43_skl))|~sQ8_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f689])).
% 0.07/0.47  fof(f692,definition,(
% 0.07/0.47    sQ9_spl <=> (in(sK44_skl,the_carrier(sK43_skl)))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f693,plain,(
% 0.07/0.47    in(sK44_skl,the_carrier(sK43_skl))|~sQ9_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f692])).
% 0.07/0.47  fof(f695,plain,(
% 0.07/0.47    sQ8_spl|sQ9_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f684,f689,f692])).
% 0.07/0.47  fof(f696,plain,(
% 0.07/0.47    ![X0]: (~in(X0,neighborhood_system(sK43_skl,sK44_skl))|~empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))|~sQ5_spl)),
% 0.07/0.47    inference(resolution,[status(thm)],[f667,f633])).
% 0.07/0.47  fof(f698,plain,(
% 0.07/0.47    empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|in(neighborhood_system(sK43_skl,sK44_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|~sQ5_spl),
% 0.07/0.47    inference(resolution,[status(thm)],[f667,f609])).
% 0.07/0.47  fof(f699,definition,(
% 0.07/0.47    ![X0]: (sQ10_spl <=> (~in(X0,neighborhood_system(sK43_skl,sK44_skl))))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f700,plain,(
% 0.07/0.47    ![X0]: (~in(X0,neighborhood_system(sK43_skl,sK44_skl))|~sQ10_spl)),
% 0.07/0.47    inference(component_clause,[status(thm)],[f699])).
% 0.07/0.47  fof(f702,definition,(
% 0.07/0.47    sQ11_spl <=> (empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f705,plain,(
% 0.07/0.47    sQ10_spl|~sQ11_spl|~sQ5_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f696,f699,f702,f666])).
% 0.07/0.47  fof(f706,definition,(
% 0.07/0.47    sQ12_spl <=> (empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f707,plain,(
% 0.07/0.47    empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|~sQ12_spl),
% 0.07/0.47    inference(component_clause,[status(thm)],[f706])).
% 0.07/0.47  fof(f709,definition,(
% 0.07/0.47    sQ13_spl <=> (in(neighborhood_system(sK43_skl,sK44_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))))),
% 0.07/0.47    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.07/0.47  fof(f712,plain,(
% 0.07/0.47    sQ12_spl|sQ13_spl|~sQ5_spl),
% 0.07/0.47    inference(split_clause,[status(thm)],[f698,f706,f709,f666])).
% 0.07/0.47  fof(f713,plain,(
% 0.07/0.47    $false|~sQ10_spl|~sQ0_spl),
% 0.07/0.47    inference(backward_subsumption_resolution,[status(thm)],[f643,f700])).
% 0.07/0.47  fof(f714,plain,(
% 0.07/0.47    $false|~sQ12_spl),
% 0.07/0.47    inference(forward_subsumption_resolution,[status(thm)],[f707,f267])).
% 0.07/0.47  fof(f715,plain,(
% 0.07/0.47    ~sQ12_spl),
% 0.07/0.47    inference(contradiction_clause,[status(thm)],[f714])).
% 0.07/0.47  fof(f716,plain,(
% 0.07/0.47    ~sQ10_spl|~sQ0_spl),
% 0.07/0.47    inference(contradiction_clause,[status(thm)],[f713])).
% 0.07/0.47  fof(f719,plain,(
% 0.07/0.47    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~empty(neighborhood_system(sK43_skl,sK44_skl))|open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~sQ5_spl),
% 0.07/0.47    inference(resolution,[status(thm)],[f166,f667])).
% 0.07/0.47  fof(f720,definition,(
% 0.07/0.47    sQ14_spl <=> (topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f723,definition,(
% 0.07/0.48    sQ15_spl <=> (top_str(boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f726,definition,(
% 0.07/0.48    sQ16_spl <=> (open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f729,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ7_spl|sQ16_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f719,f720,f723,f685,f726,f666])).
% 0.07/0.48  fof(f730,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~empty(neighborhood_system(sK43_skl,sK44_skl))|closed_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f167,f667])).
% 0.07/0.48  fof(f731,definition,(
% 0.07/0.48    sQ17_spl <=> (closed_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f734,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ7_spl|sQ17_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f730,f720,f723,f685,f731,f666])).
% 0.07/0.48  fof(f742,plain,(
% 0.07/0.48    ~finite(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))|finite(neighborhood_system(sK43_skl,sK44_skl))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f173,f667])).
% 0.07/0.48  fof(f743,definition,(
% 0.07/0.48    sQ18_spl <=> (finite(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f746,definition,(
% 0.07/0.48    sQ19_spl <=> (finite(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f749,plain,(
% 0.07/0.48    ~sQ18_spl|sQ19_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f742,f743,f746,f666])).
% 0.07/0.48  fof(f750,plain,(
% 0.07/0.48    ~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~empty(neighborhood_system(sK43_skl,sK44_skl))|boundary_set(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f177,f667])).
% 0.07/0.48  fof(f751,definition,(
% 0.07/0.48    sQ20_spl <=> (boundary_set(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f754,plain,(
% 0.07/0.48    ~sQ15_spl|~sQ7_spl|sQ20_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f750,f723,f685,f751,f666])).
% 0.07/0.48  fof(f762,definition,(
% 0.07/0.48    sQ21_spl <=> (empty_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f763,plain,(
% 0.07/0.48    empty_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~sQ21_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f762])).
% 0.07/0.48  fof(f777,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK44_skl,the_carrier(sK43_skl))|element(sK45_skl,powerset(the_carrier(sK43_skl)))|~sQ1_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f646,f236])).
% 0.07/0.48  fof(f778,definition,(
% 0.07/0.48    sQ25_spl <=> (element(sK44_skl,the_carrier(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f780,plain,(
% 0.07/0.48    ~element(sK44_skl,the_carrier(sK43_skl))|sQ25_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f778])).
% 0.07/0.48  fof(f781,definition,(
% 0.07/0.48    sQ26_spl <=> (element(sK45_skl,powerset(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f782,plain,(
% 0.07/0.48    element(sK45_skl,powerset(the_carrier(sK43_skl)))|~sQ26_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f781])).
% 0.07/0.48  fof(f784,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ25_spl|sQ26_spl|~sQ1_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f777,f657,f660,f663,f778,f781,f645])).
% 0.07/0.48  fof(f785,plain,(
% 0.07/0.48    $false|sQ25_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f780,f625])).
% 0.07/0.48  fof(f786,plain,(
% 0.07/0.48    sQ25_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f785])).
% 0.07/0.48  fof(f787,plain,(
% 0.07/0.48    ~top_str(sK43_skl)|~empty(sK45_skl)|boundary_set(sK45_skl,sK43_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f177])).
% 0.07/0.48  fof(f788,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~empty(sK45_skl)|closed_subset(sK45_skl,sK43_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f167])).
% 0.07/0.48  fof(f789,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~empty(sK45_skl)|open_subset(sK45_skl,sK43_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f166])).
% 0.07/0.48  fof(f790,plain,(
% 0.07/0.48    ~finite(the_carrier(sK43_skl))|finite(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f173])).
% 0.07/0.48  fof(f791,plain,(
% 0.07/0.48    ![X0]: (~in(X0,sK45_skl)|~empty(the_carrier(sK43_skl))|~sQ26_spl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f633])).
% 0.07/0.48  fof(f792,plain,(
% 0.07/0.48    ![X0]: (~in(X0,sK45_skl)|element(X0,the_carrier(sK43_skl))|~sQ26_spl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f630])).
% 0.07/0.48  fof(f793,plain,(
% 0.07/0.48    empty(powerset(the_carrier(sK43_skl)))|in(sK45_skl,powerset(the_carrier(sK43_skl)))|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f782,f609])).
% 0.07/0.48  fof(f794,definition,(
% 0.07/0.48    sQ27_spl <=> (empty(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f796,plain,(
% 0.07/0.48    ~empty(sK45_skl)|sQ27_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f794])).
% 0.07/0.48  fof(f797,definition,(
% 0.07/0.48    sQ28_spl <=> (boundary_set(sK45_skl,sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f800,plain,(
% 0.07/0.48    ~sQ4_spl|~sQ27_spl|sQ28_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f787,f663,f794,f797,f781])).
% 0.07/0.48  fof(f801,definition,(
% 0.07/0.48    sQ29_spl <=> (closed_subset(sK45_skl,sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f804,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ27_spl|sQ29_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f788,f660,f663,f794,f801,f781])).
% 0.07/0.48  fof(f805,definition,(
% 0.07/0.48    sQ30_spl <=> (open_subset(sK45_skl,sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f808,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ27_spl|sQ30_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f789,f660,f663,f794,f805,f781])).
% 0.07/0.48  fof(f809,definition,(
% 0.07/0.48    sQ31_spl <=> (finite(the_carrier(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f812,definition,(
% 0.07/0.48    sQ32_spl <=> (finite(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f815,plain,(
% 0.07/0.48    ~sQ31_spl|sQ32_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f790,f809,f812,f781])).
% 0.07/0.48  fof(f816,definition,(
% 0.07/0.48    ![X0]: (sQ33_spl <=> (~in(X0,sK45_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f817,plain,(
% 0.07/0.48    ![X0]: (~in(X0,sK45_skl)|~sQ33_spl)),
% 0.07/0.48    inference(component_clause,[status(thm)],[f816])).
% 0.07/0.48  fof(f819,plain,(
% 0.07/0.48    sQ33_spl|~sQ8_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f791,f816,f689,f781])).
% 0.07/0.48  fof(f820,definition,(
% 0.07/0.48    sQ34_spl <=> (empty(powerset(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f821,plain,(
% 0.07/0.48    empty(powerset(the_carrier(sK43_skl)))|~sQ34_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f820])).
% 0.07/0.48  fof(f823,definition,(
% 0.07/0.48    sQ35_spl <=> (in(sK45_skl,powerset(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f826,plain,(
% 0.07/0.48    sQ34_spl|sQ35_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f793,f820,f823,f781])).
% 0.07/0.48  fof(f827,plain,(
% 0.07/0.48    $false|~sQ34_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f821,f267])).
% 0.07/0.48  fof(f828,plain,(
% 0.07/0.48    ~sQ34_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f827])).
% 0.07/0.48  fof(f831,plain,(
% 0.07/0.48    ~empty(the_carrier(sK43_skl))|~sQ9_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f693,f638])).
% 0.07/0.48  fof(f833,definition,(
% 0.07/0.48    sQ36_spl <=> (rel_str(sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f835,plain,(
% 0.07/0.48    ~rel_str(sK10_skl)|sQ36_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f833])).
% 0.07/0.48  fof(f836,definition,(
% 0.07/0.48    sQ37_spl <=> (empty_carrier(sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f837,plain,(
% 0.07/0.48    empty_carrier(sK10_skl)|~sQ37_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f836])).
% 0.07/0.48  fof(f839,definition,(
% 0.07/0.48    sQ38_spl <=> (reflexive_relstr(sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f841,plain,(
% 0.07/0.48    ~reflexive_relstr(sK10_skl)|sQ38_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f839])).
% 0.07/0.48  fof(f849,plain,(
% 0.07/0.48    $false|~sQ21_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f763,f269])).
% 0.07/0.48  fof(f850,plain,(
% 0.07/0.48    ~sQ21_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f849])).
% 0.07/0.48  fof(f853,definition,(
% 0.07/0.48    sQ41_spl <=> (nowhere_dense(sK45_skl,sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f857,definition,(
% 0.07/0.48    sQ42_spl <=> (nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f861,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|boundary_set(sK45_skl,sK43_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f190,f782])).
% 0.07/0.48  fof(f863,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ41_spl|sQ28_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f861,f660,f663,f853,f797,f781])).
% 0.07/0.48  fof(f868,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|sK11_skl=rel_str_of(the_carrier(sK11_skl),the_InternalRel(sK11_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f402,f122])).
% 0.07/0.48  fof(f869,definition,(
% 0.07/0.48    sQ43_spl <=> (rel_str(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f871,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|sQ43_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f869])).
% 0.07/0.48  fof(f872,definition,(
% 0.07/0.48    sQ44_spl <=> (sK11_skl=rel_str_of(the_carrier(sK11_skl),the_InternalRel(sK11_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f875,plain,(
% 0.07/0.48    ~sQ43_spl|sQ44_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f868,f869,f872])).
% 0.07/0.48  fof(f876,plain,(
% 0.07/0.48    $false|sQ43_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f871,f400])).
% 0.07/0.48  fof(f877,plain,(
% 0.07/0.48    sQ43_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f876])).
% 0.07/0.48  fof(f880,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~closed_subset(sK45_skl,sK43_skl)|~boundary_set(sK45_skl,sK43_skl)|nowhere_dense(sK45_skl,sK43_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f196,f782])).
% 0.07/0.48  fof(f881,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~closed_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~boundary_set(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f196,f667])).
% 0.07/0.48  fof(f882,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ29_spl|~sQ28_spl|sQ41_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f880,f660,f663,f801,f797,f853,f781])).
% 0.07/0.48  fof(f883,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ17_spl|~sQ20_spl|sQ42_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f881,f720,f723,f731,f751,f857,f666])).
% 0.07/0.48  fof(f888,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK45_skl,sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|empty(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f204,f782])).
% 0.07/0.48  fof(f890,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ30_spl|~sQ41_spl|sQ27_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f888,f660,f663,f805,f853,f794,f781])).
% 0.07/0.48  fof(f896,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK45_skl,sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|v1_membered(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f207,f782])).
% 0.07/0.48  fof(f897,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|v1_membered(neighborhood_system(sK43_skl,sK44_skl))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f207,f667])).
% 0.07/0.48  fof(f898,definition,(
% 0.07/0.48    sQ45_spl <=> (v1_membered(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f901,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ30_spl|~sQ41_spl|sQ45_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f896,f660,f663,f805,f853,f898,f781])).
% 0.07/0.48  fof(f902,definition,(
% 0.07/0.48    sQ46_spl <=> (v1_membered(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f905,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ42_spl|sQ46_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f897,f720,f723,f726,f857,f902,f666])).
% 0.07/0.48  fof(f906,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK45_skl,sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|v2_membered(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f208,f782])).
% 0.07/0.48  fof(f907,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|v2_membered(neighborhood_system(sK43_skl,sK44_skl))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f208,f667])).
% 0.07/0.48  fof(f908,definition,(
% 0.07/0.48    sQ47_spl <=> (v2_membered(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f911,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ30_spl|~sQ41_spl|sQ47_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f906,f660,f663,f805,f853,f908,f781])).
% 0.07/0.48  fof(f912,definition,(
% 0.07/0.48    sQ48_spl <=> (v2_membered(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f915,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ42_spl|sQ48_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f907,f720,f723,f726,f857,f912,f666])).
% 0.07/0.48  fof(f917,definition,(
% 0.07/0.48    sQ49_spl <=> (empty_carrier(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f918,plain,(
% 0.07/0.48    empty_carrier(sK11_skl)|~sQ49_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f917])).
% 0.07/0.48  fof(f920,definition,(
% 0.07/0.48    sQ50_spl <=> (reflexive_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f922,plain,(
% 0.07/0.48    ~reflexive_relstr(sK11_skl)|sQ50_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f920])).
% 0.07/0.48  fof(f923,definition,(
% 0.07/0.48    sQ51_spl <=> (join_complete_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f925,plain,(
% 0.07/0.48    ~join_complete_relstr(sK11_skl)|sQ51_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f923])).
% 0.07/0.48  fof(f926,definition,(
% 0.07/0.48    sQ52_spl <=> (with_infima_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f930,plain,(
% 0.07/0.48    $false|sQ51_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f925,f413])).
% 0.07/0.48  fof(f931,plain,(
% 0.07/0.48    sQ51_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f930])).
% 0.07/0.48  fof(f932,plain,(
% 0.07/0.48    $false|sQ50_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f922,f403])).
% 0.07/0.48  fof(f933,plain,(
% 0.07/0.48    sQ50_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f932])).
% 0.07/0.48  fof(f934,plain,(
% 0.07/0.48    $false|~sQ49_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f918,f401])).
% 0.07/0.48  fof(f935,plain,(
% 0.07/0.48    ~sQ49_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f934])).
% 0.07/0.48  fof(f940,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK45_skl,sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|v3_membered(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f209,f782])).
% 0.07/0.48  fof(f941,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|v3_membered(neighborhood_system(sK43_skl,sK44_skl))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f209,f667])).
% 0.07/0.48  fof(f942,definition,(
% 0.07/0.48    sQ53_spl <=> (v3_membered(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f945,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ30_spl|~sQ41_spl|sQ53_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f940,f660,f663,f805,f853,f942,f781])).
% 0.07/0.48  fof(f946,definition,(
% 0.07/0.48    sQ54_spl <=> (v3_membered(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f949,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ42_spl|sQ54_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f941,f720,f723,f726,f857,f946,f666])).
% 0.07/0.48  fof(f950,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK45_skl,sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|v4_membered(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f210,f782])).
% 0.07/0.48  fof(f951,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|v4_membered(neighborhood_system(sK43_skl,sK44_skl))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f210,f667])).
% 0.07/0.48  fof(f952,definition,(
% 0.07/0.48    sQ55_spl <=> (v4_membered(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f955,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ30_spl|~sQ41_spl|sQ55_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f950,f660,f663,f805,f853,f952,f781])).
% 0.07/0.48  fof(f956,definition,(
% 0.07/0.48    sQ56_spl <=> (v4_membered(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f959,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ42_spl|sQ56_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f951,f720,f723,f726,f857,f956,f666])).
% 0.07/0.48  fof(f960,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK45_skl,sK43_skl)|~nowhere_dense(sK45_skl,sK43_skl)|v5_membered(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f211,f782])).
% 0.07/0.48  fof(f961,plain,(
% 0.07/0.48    ~topological_space(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~open_subset(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~nowhere_dense(neighborhood_system(sK43_skl,sK44_skl),boole_POSet(cast_as_carrier_subset(sK43_skl)))|v5_membered(neighborhood_system(sK43_skl,sK44_skl))|~sQ5_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f211,f667])).
% 0.07/0.48  fof(f962,definition,(
% 0.07/0.48    sQ57_spl <=> (v5_membered(sK45_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f965,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ30_spl|~sQ41_spl|sQ57_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f960,f660,f663,f805,f853,f962,f781])).
% 0.07/0.48  fof(f966,definition,(
% 0.07/0.48    sQ58_spl <=> (v5_membered(neighborhood_system(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f969,plain,(
% 0.07/0.48    ~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ42_spl|sQ58_spl|~sQ5_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f961,f720,f723,f726,f857,f966,f666])).
% 0.07/0.48  fof(f975,definition,(
% 0.07/0.48    sQ59_spl <=> (with_suprema_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f977,plain,(
% 0.07/0.48    ~with_suprema_relstr(sK11_skl)|sQ59_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f975])).
% 0.07/0.48  fof(f978,definition,(
% 0.07/0.48    sQ60_spl <=> (up_complete_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f980,plain,(
% 0.07/0.48    ~up_complete_relstr(sK11_skl)|sQ60_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f978])).
% 0.07/0.48  fof(f981,definition,(
% 0.07/0.48    sQ61_spl <=> (upper_bounded_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f997,plain,(
% 0.07/0.48    $false|sQ60_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f980,f412])).
% 0.07/0.48  fof(f998,plain,(
% 0.07/0.48    sQ60_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f997])).
% 0.07/0.48  fof(f999,plain,(
% 0.07/0.48    $false|sQ36_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f835,f393])).
% 0.07/0.48  fof(f1000,plain,(
% 0.07/0.48    sQ36_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f999])).
% 0.07/0.48  fof(f1001,plain,(
% 0.07/0.48    $false|sQ59_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f977,f406])).
% 0.07/0.48  fof(f1002,plain,(
% 0.07/0.48    sQ59_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1001])).
% 0.07/0.48  fof(f1003,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|empty_carrier(sK11_skl)|bounded_relstr(sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f408,f188])).
% 0.07/0.48  fof(f1004,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|empty_carrier(sK11_skl)|with_infima_relstr(sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f408,f171])).
% 0.07/0.48  fof(f1008,definition,(
% 0.07/0.48    sQ65_spl <=> (bounded_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1011,plain,(
% 0.07/0.48    ~sQ43_spl|sQ49_spl|sQ65_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1003,f869,f917,f1008])).
% 0.07/0.48  fof(f1012,plain,(
% 0.07/0.48    ~sQ43_spl|sQ49_spl|sQ52_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1004,f869,f917,f926])).
% 0.07/0.48  fof(f1020,definition,(
% 0.07/0.48    sQ66_spl <=> (lower_bounded_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1022,plain,(
% 0.07/0.48    ~lower_bounded_relstr(sK11_skl)|sQ66_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1020])).
% 0.07/0.48  fof(f1024,definition,(
% 0.07/0.48    sQ67_spl <=> (antisymmetric_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1026,plain,(
% 0.07/0.48    ~antisymmetric_relstr(sK11_skl)|sQ67_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1024])).
% 0.07/0.48  fof(f1028,plain,(
% 0.07/0.48    $false|sQ66_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1022,f409])).
% 0.07/0.48  fof(f1029,plain,(
% 0.07/0.48    sQ66_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1028])).
% 0.07/0.48  fof(f1038,plain,(
% 0.07/0.48    one_sorted_str(sK43_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f234,f624])).
% 0.07/0.48  fof(f1039,plain,(
% 0.07/0.48    element(cast_as_carrier_subset(sK43_skl),powerset(the_carrier(sK43_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1038,f227])).
% 0.07/0.48  fof(f1040,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)|v5_membered(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f211])).
% 0.07/0.48  fof(f1041,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)|v4_membered(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f210])).
% 0.07/0.48  fof(f1042,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)|v3_membered(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f209])).
% 0.07/0.48  fof(f1043,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)|v2_membered(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f208])).
% 0.07/0.48  fof(f1044,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)|v1_membered(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f207])).
% 0.07/0.48  fof(f1046,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)|empty(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f204])).
% 0.07/0.48  fof(f1047,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~closed_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)|~boundary_set(cast_as_carrier_subset(sK43_skl),sK43_skl)|nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f196])).
% 0.07/0.48  fof(f1050,plain,(
% 0.07/0.48    ~top_str(sK43_skl)|~empty(cast_as_carrier_subset(sK43_skl))|boundary_set(cast_as_carrier_subset(sK43_skl),sK43_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f177])).
% 0.07/0.48  fof(f1053,plain,(
% 0.07/0.48    ~finite(the_carrier(sK43_skl))|finite(cast_as_carrier_subset(sK43_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f173])).
% 0.07/0.48  fof(f1054,plain,(
% 0.07/0.48    ![X0]: (~in(X0,cast_as_carrier_subset(sK43_skl))|~empty(the_carrier(sK43_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f633])).
% 0.07/0.48  fof(f1056,plain,(
% 0.07/0.48    empty(powerset(the_carrier(sK43_skl)))|in(cast_as_carrier_subset(sK43_skl),powerset(the_carrier(sK43_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1039,f609])).
% 0.07/0.48  fof(f1057,definition,(
% 0.07/0.48    sQ68_spl <=> (open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1060,definition,(
% 0.07/0.48    sQ69_spl <=> (nowhere_dense(cast_as_carrier_subset(sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1063,definition,(
% 0.07/0.48    sQ70_spl <=> (v5_membered(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1066,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ68_spl|~sQ69_spl|sQ70_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1040,f660,f663,f1057,f1060,f1063])).
% 0.07/0.48  fof(f1067,definition,(
% 0.07/0.48    sQ71_spl <=> (v4_membered(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1070,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ68_spl|~sQ69_spl|sQ71_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1041,f660,f663,f1057,f1060,f1067])).
% 0.07/0.48  fof(f1071,definition,(
% 0.07/0.48    sQ72_spl <=> (v3_membered(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1074,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ68_spl|~sQ69_spl|sQ72_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1042,f660,f663,f1057,f1060,f1071])).
% 0.07/0.48  fof(f1075,definition,(
% 0.07/0.48    sQ73_spl <=> (v2_membered(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1078,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ68_spl|~sQ69_spl|sQ73_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1043,f660,f663,f1057,f1060,f1075])).
% 0.07/0.48  fof(f1079,definition,(
% 0.07/0.48    sQ74_spl <=> (v1_membered(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1082,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ68_spl|~sQ69_spl|sQ74_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1044,f660,f663,f1057,f1060,f1079])).
% 0.07/0.48  fof(f1083,definition,(
% 0.07/0.48    sQ75_spl <=> (closed_subset(cast_as_carrier_subset(sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1087,definition,(
% 0.07/0.48    sQ76_spl <=> (empty(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1089,plain,(
% 0.07/0.48    ~empty(cast_as_carrier_subset(sK43_skl))|sQ76_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1087])).
% 0.07/0.48  fof(f1090,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ68_spl|~sQ69_spl|sQ76_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1046,f660,f663,f1057,f1060,f1087])).
% 0.07/0.48  fof(f1091,definition,(
% 0.07/0.48    sQ77_spl <=> (boundary_set(cast_as_carrier_subset(sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1094,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ75_spl|~sQ77_spl|sQ69_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1047,f660,f663,f1083,f1091,f1060])).
% 0.07/0.48  fof(f1097,plain,(
% 0.07/0.48    ~sQ4_spl|~sQ76_spl|sQ77_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1050,f663,f1087,f1091])).
% 0.07/0.48  fof(f1100,definition,(
% 0.07/0.48    sQ78_spl <=> (finite(cast_as_carrier_subset(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1103,plain,(
% 0.07/0.48    ~sQ31_spl|sQ78_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1053,f809,f1100])).
% 0.07/0.48  fof(f1104,definition,(
% 0.07/0.48    ![X0]: (sQ79_spl <=> (~in(X0,cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1105,plain,(
% 0.07/0.48    ![X0]: (~in(X0,cast_as_carrier_subset(sK43_skl))|~sQ79_spl)),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1104])).
% 0.07/0.48  fof(f1107,plain,(
% 0.07/0.48    sQ79_spl|~sQ8_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1054,f1104,f689])).
% 0.07/0.48  fof(f1108,definition,(
% 0.07/0.48    sQ80_spl <=> (in(cast_as_carrier_subset(sK43_skl),powerset(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1111,plain,(
% 0.07/0.48    sQ34_spl|sQ80_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1056,f820,f1108])).
% 0.07/0.48  fof(f1112,plain,(
% 0.07/0.48    $false|~sQ9_spl|~sQ8_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f690,f831])).
% 0.07/0.48  fof(f1113,plain,(
% 0.07/0.48    ~sQ9_spl|~sQ8_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1112])).
% 0.07/0.48  fof(f1117,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|upper_bounded_relstr(sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f411,f193])).
% 0.07/0.48  fof(f1119,plain,(
% 0.07/0.48    ~sQ43_spl|sQ61_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1117,f869,f981])).
% 0.07/0.48  fof(f1129,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|point_neighbourhood(sK3_skl(sK44_skl,sK43_skl),sK43_skl,sK44_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f249,f625])).
% 0.07/0.48  fof(f1130,definition,(
% 0.07/0.48    sQ81_spl <=> (point_neighbourhood(sK3_skl(sK44_skl,sK43_skl),sK43_skl,sK44_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1131,plain,(
% 0.07/0.48    point_neighbourhood(sK3_skl(sK44_skl,sK43_skl),sK43_skl,sK44_skl)|~sQ81_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1130])).
% 0.07/0.48  fof(f1133,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|sQ81_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1129,f657,f660,f663,f1130])).
% 0.07/0.48  fof(f1154,plain,(
% 0.07/0.48    ![X0]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|element(neighborhood_system(X0,sK5_skl(the_carrier(X0))),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))))),
% 0.07/0.48    inference(resolution,[status(thm)],[f253,f225])).
% 0.07/0.48  fof(f1155,plain,(
% 0.07/0.48    ![X0]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|neighborhood_system(X0,sK5_skl(the_carrier(X0)))=a_2_0_yellow19(X0,sK5_skl(the_carrier(X0))))),
% 0.07/0.48    inference(resolution,[status(thm)],[f253,f220])).
% 0.07/0.48  fof(f1156,plain,(
% 0.07/0.48    ![X0]: (empty(X0)|in(sK5_skl(X0),X0))),
% 0.07/0.48    inference(resolution,[status(thm)],[f253,f609])).
% 0.07/0.48  fof(f1159,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK44_skl,the_carrier(sK43_skl))|element(sK3_skl(sK44_skl,sK43_skl),powerset(the_carrier(sK43_skl)))|~sQ81_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1131,f236])).
% 0.07/0.48  fof(f1160,definition,(
% 0.07/0.48    sQ82_spl <=> (element(sK3_skl(sK44_skl,sK43_skl),powerset(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1161,plain,(
% 0.07/0.48    element(sK3_skl(sK44_skl,sK43_skl),powerset(the_carrier(sK43_skl)))|~sQ82_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1160])).
% 0.07/0.48  fof(f1163,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ25_spl|sQ82_spl|~sQ81_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1159,f657,f660,f663,f778,f1160,f1130])).
% 0.07/0.48  fof(f1164,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|v5_membered(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f211])).
% 0.07/0.48  fof(f1165,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|v4_membered(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f210])).
% 0.07/0.48  fof(f1166,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|v3_membered(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f209])).
% 0.07/0.48  fof(f1167,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|v2_membered(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f208])).
% 0.07/0.48  fof(f1168,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|v1_membered(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f207])).
% 0.07/0.48  fof(f1169,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|closed_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f206])).
% 0.07/0.48  fof(f1170,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|empty(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f204])).
% 0.07/0.48  fof(f1171,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~closed_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~boundary_set(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f196])).
% 0.07/0.48  fof(f1172,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|boundary_set(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f190])).
% 0.07/0.48  fof(f1173,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~empty(sK3_skl(sK44_skl,sK43_skl))|nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f185])).
% 0.07/0.48  fof(f1175,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~empty(sK3_skl(sK44_skl,sK43_skl))|closed_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f167])).
% 0.07/0.48  fof(f1176,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|~top_str(sK43_skl)|~empty(sK3_skl(sK44_skl,sK43_skl))|open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl)|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f166])).
% 0.07/0.48  fof(f1177,plain,(
% 0.07/0.48    ~finite(the_carrier(sK43_skl))|finite(sK3_skl(sK44_skl,sK43_skl))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f173])).
% 0.07/0.48  fof(f1178,plain,(
% 0.07/0.48    ![X0]: (~in(X0,sK3_skl(sK44_skl,sK43_skl))|~empty(the_carrier(sK43_skl))|~sQ82_spl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f633])).
% 0.07/0.48  fof(f1180,plain,(
% 0.07/0.48    empty(powerset(the_carrier(sK43_skl)))|in(sK3_skl(sK44_skl,sK43_skl),powerset(the_carrier(sK43_skl)))|~sQ82_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1161,f609])).
% 0.07/0.48  fof(f1181,definition,(
% 0.07/0.48    sQ83_spl <=> (open_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1184,definition,(
% 0.07/0.48    sQ84_spl <=> (nowhere_dense(sK3_skl(sK44_skl,sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1187,definition,(
% 0.07/0.48    sQ85_spl <=> (v5_membered(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1190,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ85_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1164,f660,f663,f1181,f1184,f1187,f1160])).
% 0.07/0.48  fof(f1191,definition,(
% 0.07/0.48    sQ86_spl <=> (v4_membered(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1194,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ86_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1165,f660,f663,f1181,f1184,f1191,f1160])).
% 0.07/0.48  fof(f1195,definition,(
% 0.07/0.48    sQ87_spl <=> (v3_membered(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1198,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ87_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1166,f660,f663,f1181,f1184,f1195,f1160])).
% 0.07/0.48  fof(f1199,definition,(
% 0.07/0.48    sQ88_spl <=> (v2_membered(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1202,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ88_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1167,f660,f663,f1181,f1184,f1199,f1160])).
% 0.07/0.48  fof(f1203,definition,(
% 0.07/0.48    sQ89_spl <=> (v1_membered(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1206,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ89_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1168,f660,f663,f1181,f1184,f1203,f1160])).
% 0.07/0.48  fof(f1207,definition,(
% 0.07/0.48    sQ90_spl <=> (closed_subset(sK3_skl(sK44_skl,sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1210,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ90_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1169,f660,f663,f1181,f1184,f1207,f1160])).
% 0.07/0.48  fof(f1211,definition,(
% 0.07/0.48    sQ91_spl <=> (empty(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1213,plain,(
% 0.07/0.48    ~empty(sK3_skl(sK44_skl,sK43_skl))|sQ91_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1211])).
% 0.07/0.48  fof(f1214,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ83_spl|~sQ84_spl|sQ91_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1170,f660,f663,f1181,f1184,f1211,f1160])).
% 0.07/0.48  fof(f1215,definition,(
% 0.07/0.48    sQ92_spl <=> (boundary_set(sK3_skl(sK44_skl,sK43_skl),sK43_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1218,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ90_spl|~sQ92_spl|sQ84_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1171,f660,f663,f1207,f1215,f1184,f1160])).
% 0.07/0.48  fof(f1219,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ84_spl|sQ92_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1172,f660,f663,f1184,f1215,f1160])).
% 0.07/0.48  fof(f1220,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ91_spl|sQ84_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1173,f660,f663,f1211,f1184,f1160])).
% 0.07/0.48  fof(f1222,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ91_spl|sQ90_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1175,f660,f663,f1211,f1207,f1160])).
% 0.07/0.48  fof(f1223,plain,(
% 0.07/0.48    ~sQ3_spl|~sQ4_spl|~sQ91_spl|sQ83_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1176,f660,f663,f1211,f1181,f1160])).
% 0.07/0.48  fof(f1224,definition,(
% 0.07/0.48    sQ93_spl <=> (finite(sK3_skl(sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1227,plain,(
% 0.07/0.48    ~sQ31_spl|sQ93_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1177,f809,f1224,f1160])).
% 0.07/0.48  fof(f1228,definition,(
% 0.07/0.48    ![X0]: (sQ94_spl <=> (~in(X0,sK3_skl(sK44_skl,sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1229,plain,(
% 0.07/0.48    ![X0]: (~in(X0,sK3_skl(sK44_skl,sK43_skl))|~sQ94_spl)),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1228])).
% 0.07/0.48  fof(f1231,plain,(
% 0.07/0.48    sQ94_spl|~sQ8_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1178,f1228,f689,f1160])).
% 0.07/0.48  fof(f1232,definition,(
% 0.07/0.48    sQ95_spl <=> (in(sK3_skl(sK44_skl,sK43_skl),powerset(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1235,plain,(
% 0.07/0.48    sQ34_spl|sQ95_spl|~sQ82_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1180,f820,f1232,f1160])).
% 0.07/0.48  fof(f1237,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|element(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1154,f624])).
% 0.07/0.48  fof(f1248,definition,(
% 0.07/0.48    sQ99_spl <=> (element(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1249,plain,(
% 0.07/0.48    element(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|~sQ99_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1248])).
% 0.07/0.48  fof(f1251,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|sQ99_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1237,f657,f660,f1248])).
% 0.07/0.48  fof(f1253,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl)))=a_2_0_yellow19(sK43_skl,sK5_skl(the_carrier(sK43_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f1155,f624])).
% 0.07/0.48  fof(f1258,definition,(
% 0.07/0.48    sQ101_spl <=> (neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl)))=a_2_0_yellow19(sK43_skl,sK5_skl(the_carrier(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1259,plain,(
% 0.07/0.48    neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl)))=a_2_0_yellow19(sK43_skl,sK5_skl(the_carrier(sK43_skl)))|~sQ101_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1258])).
% 0.07/0.48  fof(f1261,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|sQ101_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1253,f657,f660,f1258])).
% 0.07/0.48  fof(f1265,plain,(
% 0.07/0.48    empty_carrier(sK13_skl)|lower_relstr_subset(cast_as_carrier_subset(sK13_skl),sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f263,f418])).
% 0.07/0.48  fof(f1267,plain,(
% 0.07/0.48    empty_carrier(sK11_skl)|lower_relstr_subset(cast_as_carrier_subset(sK11_skl),sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f263,f400])).
% 0.07/0.48  fof(f1268,plain,(
% 0.07/0.48    empty_carrier(sK10_skl)|lower_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f263,f393])).
% 0.07/0.48  fof(f1270,definition,(
% 0.07/0.48    sQ102_spl <=> (empty_carrier(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1271,plain,(
% 0.07/0.48    empty_carrier(sK13_skl)|~sQ102_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1270])).
% 0.07/0.48  fof(f1273,definition,(
% 0.07/0.48    sQ103_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK13_skl),sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1276,plain,(
% 0.07/0.48    sQ102_spl|sQ103_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1265,f1270,f1273])).
% 0.07/0.48  fof(f1278,definition,(
% 0.07/0.48    sQ104_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK11_skl),sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1281,plain,(
% 0.07/0.48    sQ49_spl|sQ104_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1267,f917,f1278])).
% 0.07/0.48  fof(f1282,definition,(
% 0.07/0.48    sQ105_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1285,plain,(
% 0.07/0.48    sQ37_spl|sQ105_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1268,f836,f1282])).
% 0.07/0.48  fof(f1293,plain,(
% 0.07/0.48    $false|~sQ37_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f837,f394])).
% 0.07/0.48  fof(f1294,plain,(
% 0.07/0.48    ~sQ37_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1293])).
% 0.07/0.48  fof(f1295,plain,(
% 0.07/0.48    $false|~sQ102_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1271,f419])).
% 0.07/0.48  fof(f1296,plain,(
% 0.07/0.48    ~sQ102_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1295])).
% 0.07/0.48  fof(f1297,plain,(
% 0.07/0.48    empty_carrier(sK13_skl)|upper_relstr_subset(cast_as_carrier_subset(sK13_skl),sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f264,f418])).
% 0.07/0.48  fof(f1299,plain,(
% 0.07/0.48    empty_carrier(sK11_skl)|upper_relstr_subset(cast_as_carrier_subset(sK11_skl),sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f264,f400])).
% 0.07/0.48  fof(f1300,plain,(
% 0.07/0.48    empty_carrier(sK10_skl)|upper_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f264,f393])).
% 0.07/0.48  fof(f1302,definition,(
% 0.07/0.48    sQ108_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK13_skl),sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1305,plain,(
% 0.07/0.48    sQ102_spl|sQ108_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1297,f1270,f1302])).
% 0.07/0.48  fof(f1307,definition,(
% 0.07/0.48    sQ109_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK11_skl),sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1310,plain,(
% 0.07/0.48    sQ49_spl|sQ109_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1299,f917,f1307])).
% 0.07/0.48  fof(f1311,definition,(
% 0.07/0.48    sQ110_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1314,plain,(
% 0.07/0.48    sQ37_spl|sQ110_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1300,f836,f1311])).
% 0.07/0.48  fof(f1329,plain,(
% 0.07/0.48    ~top_str(boole_POSet(cast_as_carrier_subset(sK43_skl)))|~empty(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|boundary_set(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),boole_POSet(cast_as_carrier_subset(sK43_skl)))|~sQ99_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1249,f177])).
% 0.07/0.48  fof(f1332,plain,(
% 0.07/0.48    ~finite(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))|finite(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|~sQ99_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1249,f173])).
% 0.07/0.48  fof(f1333,plain,(
% 0.07/0.48    ![X0]: (~in(X0,neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|~empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))|~sQ99_spl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f1249,f633])).
% 0.07/0.48  fof(f1335,plain,(
% 0.07/0.48    empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|in(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl)))))|~sQ99_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1249,f609])).
% 0.07/0.48  fof(f1366,definition,(
% 0.07/0.48    sQ120_spl <=> (empty(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl)))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1370,definition,(
% 0.07/0.48    sQ121_spl <=> (boundary_set(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),boole_POSet(cast_as_carrier_subset(sK43_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1376,plain,(
% 0.07/0.48    ~sQ15_spl|~sQ120_spl|sQ121_spl|~sQ99_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1329,f723,f1366,f1370,f1248])).
% 0.07/0.48  fof(f1379,definition,(
% 0.07/0.48    sQ122_spl <=> (finite(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl)))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1382,plain,(
% 0.07/0.48    ~sQ18_spl|sQ122_spl|~sQ99_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1332,f743,f1379,f1248])).
% 0.07/0.48  fof(f1383,definition,(
% 0.07/0.48    ![X0]: (sQ123_spl <=> (~in(X0,neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1386,plain,(
% 0.07/0.48    sQ123_spl|~sQ11_spl|~sQ99_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1333,f1383,f702,f1248])).
% 0.07/0.48  fof(f1387,definition,(
% 0.07/0.48    sQ124_spl <=> (in(neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK43_skl))))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1390,plain,(
% 0.07/0.48    sQ12_spl|sQ124_spl|~sQ99_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1335,f706,f1387,f1248])).
% 0.07/0.48  fof(f1406,plain,(
% 0.07/0.48    empty(cast_as_carrier_subset(sK43_skl))|~sQ79_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1156,f1105])).
% 0.07/0.48  fof(f1407,plain,(
% 0.07/0.48    empty(sK45_skl)|~sQ33_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1156,f817])).
% 0.07/0.48  fof(f1411,plain,(
% 0.07/0.48    $false|sQ76_spl|~sQ79_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1406,f1089])).
% 0.07/0.48  fof(f1412,plain,(
% 0.07/0.48    sQ76_spl|~sQ79_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1411])).
% 0.07/0.48  fof(f1413,plain,(
% 0.07/0.48    $false|sQ27_spl|~sQ33_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1407,f796])).
% 0.07/0.48  fof(f1414,plain,(
% 0.07/0.48    sQ27_spl|~sQ33_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1413])).
% 0.07/0.48  fof(f1495,definition,(
% 0.07/0.48    sQ144_spl <=> (empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK1_skl))))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1496,plain,(
% 0.07/0.48    empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK1_skl)))))|~sQ144_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1495])).
% 0.07/0.48  fof(f1502,plain,(
% 0.07/0.48    $false|~sQ144_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1496,f267])).
% 0.07/0.48  fof(f1503,plain,(
% 0.07/0.48    ~sQ144_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1502])).
% 0.07/0.48  fof(f1504,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|sK13_skl=rel_str_of(the_carrier(sK13_skl),the_InternalRel(sK13_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f420,f122])).
% 0.07/0.48  fof(f1505,definition,(
% 0.07/0.48    sQ146_spl <=> (rel_str(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1507,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|sQ146_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1505])).
% 0.07/0.48  fof(f1508,definition,(
% 0.07/0.48    sQ147_spl <=> (sK13_skl=rel_str_of(the_carrier(sK13_skl),the_InternalRel(sK13_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1511,plain,(
% 0.07/0.48    ~sQ146_spl|sQ147_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1504,f1505,f1508])).
% 0.07/0.48  fof(f1512,plain,(
% 0.07/0.48    $false|sQ146_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1507,f418])).
% 0.07/0.48  fof(f1513,plain,(
% 0.07/0.48    sQ146_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1512])).
% 0.07/0.48  fof(f1514,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|~with_suprema_relstr(sK13_skl)|~up_complete_relstr(sK13_skl)|upper_bounded_relstr(sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f421,f218])).
% 0.07/0.48  fof(f1515,definition,(
% 0.07/0.48    sQ148_spl <=> (with_suprema_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1518,definition,(
% 0.07/0.48    sQ149_spl <=> (up_complete_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1521,definition,(
% 0.07/0.48    sQ150_spl <=> (upper_bounded_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1524,plain,(
% 0.07/0.48    ~sQ146_spl|~sQ148_spl|~sQ149_spl|sQ150_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1514,f1505,f1515,f1518,f1521])).
% 0.07/0.48  fof(f1533,definition,(
% 0.07/0.48    sQ151_spl <=> (reflexive_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1535,plain,(
% 0.07/0.48    ~reflexive_relstr(sK13_skl)|sQ151_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1533])).
% 0.07/0.48  fof(f1536,definition,(
% 0.07/0.48    sQ152_spl <=> (join_complete_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1539,definition,(
% 0.07/0.48    sQ153_spl <=> (with_infima_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1543,plain,(
% 0.07/0.48    $false|sQ151_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1535,f421])).
% 0.07/0.48  fof(f1544,plain,(
% 0.07/0.48    sQ151_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1543])).
% 0.07/0.48  fof(f1545,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|empty_carrier(sK13_skl)|bounded_relstr(sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f424,f188])).
% 0.07/0.48  fof(f1546,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|empty_carrier(sK13_skl)|with_infima_relstr(sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f424,f171])).
% 0.07/0.48  fof(f1547,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|empty_carrier(sK13_skl)|with_suprema_relstr(sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f424,f170])).
% 0.07/0.48  fof(f1548,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|empty_carrier(sK13_skl)|~reflexive_relstr(sK13_skl)|join_complete_relstr(sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f424,f129])).
% 0.07/0.48  fof(f1549,plain,(
% 0.07/0.48    ~rel_str(sK13_skl)|empty_carrier(sK13_skl)|~reflexive_relstr(sK13_skl)|up_complete_relstr(sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f424,f128])).
% 0.07/0.48  fof(f1550,definition,(
% 0.07/0.48    sQ154_spl <=> (bounded_relstr(sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1553,plain,(
% 0.07/0.48    ~sQ146_spl|sQ102_spl|sQ154_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1545,f1505,f1270,f1550])).
% 0.07/0.48  fof(f1554,plain,(
% 0.07/0.48    ~sQ146_spl|sQ102_spl|sQ153_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1546,f1505,f1270,f1539])).
% 0.07/0.48  fof(f1555,plain,(
% 0.07/0.48    ~sQ146_spl|sQ102_spl|sQ148_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1547,f1505,f1270,f1515])).
% 0.07/0.48  fof(f1556,plain,(
% 0.07/0.48    ~sQ146_spl|sQ102_spl|~sQ151_spl|sQ152_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1548,f1505,f1270,f1533,f1536])).
% 0.07/0.48  fof(f1557,plain,(
% 0.07/0.48    ~sQ146_spl|sQ102_spl|~sQ151_spl|sQ149_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1549,f1505,f1270,f1533,f1518])).
% 0.07/0.48  fof(f1588,plain,(
% 0.07/0.48    element(sK5_skl(sK45_skl),the_carrier(sK43_skl))|empty(sK45_skl)|~sQ26_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f792,f1156])).
% 0.07/0.48  fof(f1589,definition,(
% 0.07/0.48    sQ156_spl <=> (element(sK5_skl(sK45_skl),the_carrier(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1592,plain,(
% 0.07/0.48    sQ156_spl|sQ27_spl|~sQ26_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1588,f1589,f794,f781])).
% 0.07/0.48  fof(f1596,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|upper_relstr_subset(cast_as_carrier_subset(sK18_skl),sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f442,f264])).
% 0.07/0.48  fof(f1597,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|lower_relstr_subset(cast_as_carrier_subset(sK18_skl),sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f442,f263])).
% 0.07/0.48  fof(f1600,definition,(
% 0.07/0.48    sQ157_spl <=> (empty_carrier(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1601,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|~sQ157_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1600])).
% 0.07/0.48  fof(f1603,definition,(
% 0.07/0.48    sQ158_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK18_skl),sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1606,plain,(
% 0.07/0.48    sQ157_spl|sQ158_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1596,f1600,f1603])).
% 0.07/0.48  fof(f1607,definition,(
% 0.07/0.48    sQ159_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK18_skl),sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1610,plain,(
% 0.07/0.48    sQ157_spl|sQ159_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1597,f1600,f1607])).
% 0.07/0.48  fof(f1611,plain,(
% 0.07/0.48    $false|~sQ157_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1601,f443])).
% 0.07/0.48  fof(f1612,plain,(
% 0.07/0.48    ~sQ157_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1611])).
% 0.07/0.48  fof(f1628,plain,(
% 0.07/0.48    empty(sK3_skl(sK44_skl,sK43_skl))|~sQ94_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f1229,f1156])).
% 0.07/0.48  fof(f1629,plain,(
% 0.07/0.48    $false|sQ91_spl|~sQ94_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1628,f1213])).
% 0.07/0.48  fof(f1630,plain,(
% 0.07/0.48    sQ91_spl|~sQ94_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1629])).
% 0.07/0.48  fof(f1631,plain,(
% 0.07/0.48    ~rel_str(sK18_skl)|sK18_skl=rel_str_of(the_carrier(sK18_skl),the_InternalRel(sK18_skl))),
% 0.07/0.48    inference(resolution,[status(thm)],[f445,f122])).
% 0.07/0.48  fof(f1632,definition,(
% 0.07/0.48    sQ160_spl <=> (rel_str(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1634,plain,(
% 0.07/0.48    ~rel_str(sK18_skl)|sQ160_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1632])).
% 0.07/0.48  fof(f1635,definition,(
% 0.07/0.48    sQ161_spl <=> (sK18_skl=rel_str_of(the_carrier(sK18_skl),the_InternalRel(sK18_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1638,plain,(
% 0.07/0.48    ~sQ160_spl|sQ161_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1631,f1632,f1635])).
% 0.07/0.48  fof(f1639,plain,(
% 0.07/0.48    $false|sQ160_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1634,f442])).
% 0.07/0.48  fof(f1640,plain,(
% 0.07/0.48    sQ160_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1639])).
% 0.07/0.48  fof(f1642,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|directed_subset(cast_as_carrier_subset(sK11_skl),sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f291,f406])).
% 0.07/0.48  fof(f1644,definition,(
% 0.07/0.48    sQ162_spl <=> (directed_subset(cast_as_carrier_subset(sK11_skl),sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1647,plain,(
% 0.07/0.48    ~sQ43_spl|sQ162_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1642,f869,f1644])).
% 0.07/0.48  fof(f1656,plain,(
% 0.07/0.48    ~rel_str(sK11_skl)|filtered_subset(cast_as_carrier_subset(sK11_skl),sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f323,f407])).
% 0.07/0.48  fof(f1658,definition,(
% 0.07/0.48    sQ163_spl <=> (filtered_subset(cast_as_carrier_subset(sK11_skl),sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1661,plain,(
% 0.07/0.48    ~sQ43_spl|sQ163_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1656,f869,f1658])).
% 0.07/0.48  fof(f1667,definition,(
% 0.07/0.48    sQ164_spl <=> (with_suprema_relstr(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1669,plain,(
% 0.07/0.48    ~with_suprema_relstr(sK18_skl)|sQ164_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1667])).
% 0.07/0.48  fof(f1673,definition,(
% 0.07/0.48    sQ166_spl <=> (upper_bounded_relstr(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1677,plain,(
% 0.07/0.48    $false|sQ164_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1669,f457])).
% 0.07/0.48  fof(f1678,plain,(
% 0.07/0.48    sQ164_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1677])).
% 0.07/0.48  fof(f1680,definition,(
% 0.07/0.48    sQ167_spl <=> (reflexive_relstr(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1682,plain,(
% 0.07/0.48    ~reflexive_relstr(sK18_skl)|sQ167_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1680])).
% 0.07/0.48  fof(f1690,plain,(
% 0.07/0.48    $false|sQ167_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1682,f446])).
% 0.07/0.48  fof(f1691,plain,(
% 0.07/0.48    sQ167_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1690])).
% 0.07/0.48  fof(f1693,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|closed_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f325,f624])).
% 0.07/0.48  fof(f1698,plain,(
% 0.07/0.48    ~sQ3_spl|sQ75_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1693,f660,f1083])).
% 0.07/0.48  fof(f1705,plain,(
% 0.07/0.48    ~topological_space(sK43_skl)|open_subset(cast_as_carrier_subset(sK43_skl),sK43_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f336,f624])).
% 0.07/0.48  fof(f1710,plain,(
% 0.07/0.48    ~sQ3_spl|sQ68_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1705,f660,f1057])).
% 0.07/0.48  fof(f1715,plain,(
% 0.07/0.48    ![X0]: (empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK5_skl(the_carrier(sK43_skl)),the_carrier(sK43_skl))|~in(X0,neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|point_neighbourhood(sK7_skl(X0,sK5_skl(the_carrier(sK43_skl)),sK43_skl),sK43_skl,sK5_skl(the_carrier(sK43_skl)))|~sQ101_spl)),
% 0.07/0.48    inference(paramodulation,[status(thm)],[f1259,f372])).
% 0.07/0.48  fof(f1716,plain,(
% 0.07/0.48    ![X0]: (empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK44_skl,the_carrier(sK43_skl))|~in(X0,neighborhood_system(sK43_skl,sK44_skl))|point_neighbourhood(sK7_skl(X0,sK44_skl,sK43_skl),sK43_skl,sK44_skl)|~sQ6_spl)),
% 0.07/0.48    inference(paramodulation,[status(thm)],[f671,f372])).
% 0.07/0.48  fof(f1717,definition,(
% 0.07/0.48    sQ172_spl <=> (top_str(sK1_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1719,plain,(
% 0.07/0.48    ~top_str(sK1_skl)|sQ172_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1717])).
% 0.07/0.48  fof(f1720,definition,(
% 0.07/0.48    sQ173_spl <=> (element(sK5_skl(the_carrier(sK1_skl)),the_carrier(sK1_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1722,plain,(
% 0.07/0.48    ~element(sK5_skl(the_carrier(sK1_skl)),the_carrier(sK1_skl))|sQ173_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1720])).
% 0.07/0.48  fof(f1727,definition,(
% 0.07/0.48    sQ175_spl <=> (element(sK5_skl(the_carrier(sK43_skl)),the_carrier(sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1729,plain,(
% 0.07/0.48    ~element(sK5_skl(the_carrier(sK43_skl)),the_carrier(sK43_skl))|sQ175_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1727])).
% 0.07/0.48  fof(f1730,definition,(
% 0.07/0.48    ![X0]: (sQ176_spl <=> (~in(X0,neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|point_neighbourhood(sK7_skl(X0,sK5_skl(the_carrier(sK43_skl)),sK43_skl),sK43_skl,sK5_skl(the_carrier(sK43_skl)))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1733,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ175_spl|sQ176_spl|~sQ101_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1715,f657,f660,f663,f1727,f1730,f1258])).
% 0.07/0.48  fof(f1734,definition,(
% 0.07/0.48    ![X0]: (sQ177_spl <=> (~in(X0,neighborhood_system(sK43_skl,sK44_skl))|point_neighbourhood(sK7_skl(X0,sK44_skl,sK43_skl),sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1735,plain,(
% 0.07/0.48    ![X0]: (~in(X0,neighborhood_system(sK43_skl,sK44_skl))|point_neighbourhood(sK7_skl(X0,sK44_skl,sK43_skl),sK43_skl,sK44_skl)|~sQ177_spl)),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1734])).
% 0.07/0.48  fof(f1737,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ25_spl|sQ177_spl|~sQ6_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1716,f657,f660,f663,f778,f1734,f670])).
% 0.07/0.48  fof(f1738,plain,(
% 0.07/0.48    $false|sQ175_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1729,f253])).
% 0.07/0.48  fof(f1739,plain,(
% 0.07/0.48    sQ175_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1738])).
% 0.07/0.48  fof(f1740,plain,(
% 0.07/0.48    $false|sQ173_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1722,f253])).
% 0.07/0.48  fof(f1741,plain,(
% 0.07/0.48    sQ173_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1740])).
% 0.07/0.48  fof(f1742,plain,(
% 0.07/0.48    $false|sQ172_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1719,f244])).
% 0.07/0.48  fof(f1743,plain,(
% 0.07/0.48    sQ172_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1742])).
% 0.07/0.48  fof(f1765,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|~rel_str(sK18_skl)|filtered_subset(cast_as_carrier_subset(sK18_skl),sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f449,f328])).
% 0.07/0.48  fof(f1767,definition,(
% 0.07/0.48    sQ181_spl <=> (filtered_subset(cast_as_carrier_subset(sK18_skl),sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1770,plain,(
% 0.07/0.48    sQ157_spl|~sQ160_spl|sQ181_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1765,f1600,f1632,f1767])).
% 0.07/0.48  fof(f1771,definition,(
% 0.07/0.48    sQ182_spl <=> (bounded_relstr(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1775,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|~rel_str(sK18_skl)|directed_subset(cast_as_carrier_subset(sK18_skl),sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f450,f316])).
% 0.07/0.48  fof(f1776,plain,(
% 0.07/0.48    ~rel_str(sK18_skl)|~lower_bounded_relstr(sK18_skl)|bounded_relstr(sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f450,f202])).
% 0.07/0.48  fof(f1778,definition,(
% 0.07/0.48    sQ183_spl <=> (directed_subset(cast_as_carrier_subset(sK18_skl),sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1781,plain,(
% 0.07/0.48    sQ157_spl|~sQ160_spl|sQ183_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1775,f1600,f1632,f1778])).
% 0.07/0.48  fof(f1782,definition,(
% 0.07/0.48    sQ184_spl <=> (lower_bounded_relstr(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1784,plain,(
% 0.07/0.48    ~lower_bounded_relstr(sK18_skl)|sQ184_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1782])).
% 0.07/0.48  fof(f1785,plain,(
% 0.07/0.48    ~sQ160_spl|~sQ184_spl|sQ182_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1776,f1632,f1782,f1771])).
% 0.07/0.48  fof(f1786,definition,(
% 0.07/0.48    sQ185_spl <=> (antisymmetric_relstr(sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1788,plain,(
% 0.07/0.48    ~antisymmetric_relstr(sK18_skl)|sQ185_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1786])).
% 0.07/0.48  fof(f1790,plain,(
% 0.07/0.48    $false|sQ185_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1788,f448])).
% 0.07/0.48  fof(f1791,plain,(
% 0.07/0.48    sQ185_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1790])).
% 0.07/0.48  fof(f1792,plain,(
% 0.07/0.48    $false|sQ184_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1784,f449])).
% 0.07/0.48  fof(f1793,plain,(
% 0.07/0.48    sQ184_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1792])).
% 0.07/0.48  fof(f1794,plain,(
% 0.07/0.48    ~rel_str(sK18_skl)|upper_bounded_relstr(sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f451,f193])).
% 0.07/0.48  fof(f1796,plain,(
% 0.07/0.48    ~sQ160_spl|sQ166_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1794,f1632,f1673])).
% 0.07/0.48  fof(f1799,plain,(
% 0.07/0.48    ![X0]: (empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK5_skl(the_carrier(sK43_skl)),the_carrier(sK43_skl))|~in(X0,neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|X0=sK7_skl(X0,sK5_skl(the_carrier(sK43_skl)),sK43_skl)|~sQ101_spl)),
% 0.07/0.48    inference(paramodulation,[status(thm)],[f1259,f373])).
% 0.07/0.48  fof(f1800,plain,(
% 0.07/0.48    ![X0]: (empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK44_skl,the_carrier(sK43_skl))|~in(X0,neighborhood_system(sK43_skl,sK44_skl))|X0=sK7_skl(X0,sK44_skl,sK43_skl)|~sQ6_spl)),
% 0.07/0.48    inference(paramodulation,[status(thm)],[f671,f373])).
% 0.07/0.48  fof(f1801,definition,(
% 0.07/0.48    ![X0]: (sQ186_spl <=> (~in(X0,neighborhood_system(sK43_skl,sK5_skl(the_carrier(sK43_skl))))|X0=sK7_skl(X0,sK5_skl(the_carrier(sK43_skl)),sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1804,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ175_spl|sQ186_spl|~sQ101_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1799,f657,f660,f663,f1727,f1801,f1258])).
% 0.07/0.48  fof(f1805,definition,(
% 0.07/0.48    ![X0]: (sQ187_spl <=> (~in(X0,neighborhood_system(sK43_skl,sK44_skl))|X0=sK7_skl(X0,sK44_skl,sK43_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1806,plain,(
% 0.07/0.48    ![X0]: (~in(X0,neighborhood_system(sK43_skl,sK44_skl))|X0=sK7_skl(X0,sK44_skl,sK43_skl)|~sQ187_spl)),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1805])).
% 0.07/0.48  fof(f1808,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ25_spl|sQ187_spl|~sQ6_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1800,f657,f660,f663,f778,f1805,f670])).
% 0.07/0.48  fof(f1809,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK44_skl,the_carrier(sK43_skl))|in(sK3_skl(sK44_skl,sK43_skl),a_2_0_yellow19(sK43_skl,sK44_skl))|~sQ81_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f654,f1131])).
% 0.07/0.48  fof(f1810,plain,(
% 0.07/0.48    empty_carrier(sK43_skl)|~topological_space(sK43_skl)|~top_str(sK43_skl)|~element(sK44_skl,the_carrier(sK43_skl))|in(sK45_skl,a_2_0_yellow19(sK43_skl,sK44_skl))|~sQ1_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f654,f646])).
% 0.07/0.48  fof(f1811,definition,(
% 0.07/0.48    sQ188_spl <=> (in(sK3_skl(sK44_skl,sK43_skl),a_2_0_yellow19(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1814,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ25_spl|sQ188_spl|~sQ81_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1809,f657,f660,f663,f778,f1811,f1130])).
% 0.07/0.48  fof(f1815,definition,(
% 0.07/0.48    sQ189_spl <=> (in(sK45_skl,a_2_0_yellow19(sK43_skl,sK44_skl)))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1816,plain,(
% 0.07/0.48    in(sK45_skl,a_2_0_yellow19(sK43_skl,sK44_skl))|~sQ189_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1815])).
% 0.07/0.48  fof(f1818,plain,(
% 0.07/0.48    sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ25_spl|sQ189_spl|~sQ1_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1810,f657,f660,f663,f778,f1815,f645])).
% 0.07/0.48  fof(f1820,plain,(
% 0.07/0.48    in(sK45_skl,neighborhood_system(sK43_skl,sK44_skl))|~sQ6_spl|~sQ189_spl),
% 0.07/0.48    inference(forward_demodulation,[status(thm)],[f671,f1816])).
% 0.07/0.48  fof(f1821,plain,(
% 0.07/0.48    $false|sQ0_spl|~sQ6_spl|~sQ189_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f1820,f644])).
% 0.07/0.48  fof(f1822,plain,(
% 0.07/0.48    sQ0_spl|~sQ6_spl|~sQ189_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1821])).
% 0.07/0.48  fof(f1829,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|~reflexive_relstr(sK18_skl)|~rel_str(sK18_skl)|element(sK8_skl(sK18_skl),powerset(the_carrier(sK18_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f380,f447])).
% 0.07/0.48  fof(f1830,plain,(
% 0.07/0.48    empty_carrier(sK13_skl)|~reflexive_relstr(sK13_skl)|~rel_str(sK13_skl)|element(sK8_skl(sK13_skl),powerset(the_carrier(sK13_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f380,f422])).
% 0.07/0.48  fof(f1832,plain,(
% 0.07/0.48    empty_carrier(sK11_skl)|~reflexive_relstr(sK11_skl)|~rel_str(sK11_skl)|element(sK8_skl(sK11_skl),powerset(the_carrier(sK11_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f380,f404])).
% 0.07/0.48  fof(f1833,plain,(
% 0.07/0.48    empty_carrier(sK10_skl)|~reflexive_relstr(sK10_skl)|~rel_str(sK10_skl)|element(sK8_skl(sK10_skl),powerset(the_carrier(sK10_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f380,f396])).
% 0.07/0.48  fof(f1834,definition,(
% 0.07/0.48    sQ190_spl <=> (element(sK8_skl(sK18_skl),powerset(the_carrier(sK18_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1837,plain,(
% 0.07/0.48    sQ157_spl|~sQ167_spl|~sQ160_spl|sQ190_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1829,f1600,f1680,f1632,f1834])).
% 0.07/0.48  fof(f1838,definition,(
% 0.07/0.48    sQ191_spl <=> (element(sK8_skl(sK13_skl),powerset(the_carrier(sK13_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1841,plain,(
% 0.07/0.48    sQ102_spl|~sQ151_spl|~sQ146_spl|sQ191_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1830,f1270,f1533,f1505,f1838])).
% 0.07/0.48  fof(f1843,definition,(
% 0.07/0.48    sQ192_spl <=> (element(sK8_skl(sK11_skl),powerset(the_carrier(sK11_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1846,plain,(
% 0.07/0.48    sQ49_spl|~sQ50_spl|~sQ43_spl|sQ192_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1832,f917,f920,f869,f1843])).
% 0.07/0.48  fof(f1847,definition,(
% 0.07/0.48    sQ193_spl <=> (element(sK8_skl(sK10_skl),powerset(the_carrier(sK10_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1850,plain,(
% 0.07/0.48    sQ37_spl|~sQ38_spl|~sQ36_spl|sQ193_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1833,f836,f839,f833,f1847])).
% 0.07/0.48  fof(f1851,plain,(
% 0.07/0.48    $false|sQ38_spl),
% 0.07/0.48    inference(forward_subsumption_resolution,[status(thm)],[f841,f395])).
% 0.07/0.48  fof(f1852,plain,(
% 0.07/0.48    sQ38_spl),
% 0.07/0.48    inference(contradiction_clause,[status(thm)],[f1851])).
% 0.07/0.48  fof(f1856,plain,(
% 0.07/0.48    point_neighbourhood(sK7_skl(sK45_skl,sK44_skl,sK43_skl),sK43_skl,sK44_skl)|~sQ0_spl|~sQ177_spl),
% 0.07/0.48    inference(resolution,[status(thm)],[f643,f1735])).
% 0.07/0.48  fof(f1864,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|~reflexive_relstr(sK18_skl)|~rel_str(sK18_skl)|filtered_subset(sK8_skl(sK18_skl),sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f382,f447])).
% 0.07/0.48  fof(f1865,plain,(
% 0.07/0.48    empty_carrier(sK13_skl)|~reflexive_relstr(sK13_skl)|~rel_str(sK13_skl)|filtered_subset(sK8_skl(sK13_skl),sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f382,f422])).
% 0.07/0.48  fof(f1867,plain,(
% 0.07/0.48    empty_carrier(sK11_skl)|~reflexive_relstr(sK11_skl)|~rel_str(sK11_skl)|filtered_subset(sK8_skl(sK11_skl),sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f382,f404])).
% 0.07/0.48  fof(f1868,plain,(
% 0.07/0.48    empty_carrier(sK10_skl)|~reflexive_relstr(sK10_skl)|~rel_str(sK10_skl)|filtered_subset(sK8_skl(sK10_skl),sK10_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f382,f396])).
% 0.07/0.48  fof(f1869,definition,(
% 0.07/0.48    sQ194_spl <=> (filtered_subset(sK8_skl(sK18_skl),sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1872,plain,(
% 0.07/0.48    sQ157_spl|~sQ167_spl|~sQ160_spl|sQ194_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1864,f1600,f1680,f1632,f1869])).
% 0.07/0.48  fof(f1873,definition,(
% 0.07/0.48    sQ195_spl <=> (filtered_subset(sK8_skl(sK13_skl),sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1876,plain,(
% 0.07/0.48    sQ102_spl|~sQ151_spl|~sQ146_spl|sQ195_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1865,f1270,f1533,f1505,f1873])).
% 0.07/0.48  fof(f1878,definition,(
% 0.07/0.48    sQ196_spl <=> (filtered_subset(sK8_skl(sK11_skl),sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1881,plain,(
% 0.07/0.48    sQ49_spl|~sQ50_spl|~sQ43_spl|sQ196_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1867,f917,f920,f869,f1878])).
% 0.07/0.48  fof(f1882,definition,(
% 0.07/0.48    sQ197_spl <=> (filtered_subset(sK8_skl(sK10_skl),sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1885,plain,(
% 0.07/0.48    sQ37_spl|~sQ38_spl|~sQ36_spl|sQ197_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1868,f836,f839,f833,f1882])).
% 0.07/0.48  fof(f1886,plain,(
% 0.07/0.48    empty_carrier(sK18_skl)|~reflexive_relstr(sK18_skl)|~rel_str(sK18_skl)|upper_relstr_subset(sK8_skl(sK18_skl),sK18_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f383,f447])).
% 0.07/0.48  fof(f1887,plain,(
% 0.07/0.48    empty_carrier(sK13_skl)|~reflexive_relstr(sK13_skl)|~rel_str(sK13_skl)|upper_relstr_subset(sK8_skl(sK13_skl),sK13_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f383,f422])).
% 0.07/0.48  fof(f1889,plain,(
% 0.07/0.48    empty_carrier(sK11_skl)|~reflexive_relstr(sK11_skl)|~rel_str(sK11_skl)|upper_relstr_subset(sK8_skl(sK11_skl),sK11_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f383,f404])).
% 0.07/0.48  fof(f1890,plain,(
% 0.07/0.48    empty_carrier(sK10_skl)|~reflexive_relstr(sK10_skl)|~rel_str(sK10_skl)|upper_relstr_subset(sK8_skl(sK10_skl),sK10_skl)),
% 0.07/0.48    inference(resolution,[status(thm)],[f383,f396])).
% 0.07/0.48  fof(f1891,definition,(
% 0.07/0.48    sQ198_spl <=> (upper_relstr_subset(sK8_skl(sK18_skl),sK18_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1894,plain,(
% 0.07/0.48    sQ157_spl|~sQ167_spl|~sQ160_spl|sQ198_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1886,f1600,f1680,f1632,f1891])).
% 0.07/0.48  fof(f1895,definition,(
% 0.07/0.48    sQ199_spl <=> (upper_relstr_subset(sK8_skl(sK13_skl),sK13_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1898,plain,(
% 0.07/0.48    sQ102_spl|~sQ151_spl|~sQ146_spl|sQ199_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1887,f1270,f1533,f1505,f1895])).
% 0.07/0.48  fof(f1900,definition,(
% 0.07/0.48    sQ200_spl <=> (upper_relstr_subset(sK8_skl(sK11_skl),sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1903,plain,(
% 0.07/0.48    sQ49_spl|~sQ50_spl|~sQ43_spl|sQ200_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1889,f917,f920,f869,f1900])).
% 0.07/0.48  fof(f1904,definition,(
% 0.07/0.48    sQ201_spl <=> (upper_relstr_subset(sK8_skl(sK10_skl),sK10_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1907,plain,(
% 0.07/0.48    sQ37_spl|~sQ38_spl|~sQ36_spl|sQ201_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1890,f836,f839,f833,f1904])).
% 0.07/0.48  fof(f1909,plain,(
% 0.07/0.48    ~reflexive_relstr(sK11_skl)|~transitive_relstr(sK11_skl)|~antisymmetric_relstr(sK11_skl)|~with_suprema_relstr(sK11_skl)|~rel_str(sK11_skl)|element(sK9_skl(sK11_skl),powerset(the_carrier(sK11_skl)))),
% 0.07/0.48    inference(resolution,[status(thm)],[f386,f407])).
% 0.07/0.48  fof(f1911,definition,(
% 0.07/0.48    sQ202_spl <=> (transitive_relstr(sK11_skl))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1913,plain,(
% 0.07/0.48    ~transitive_relstr(sK11_skl)|sQ202_spl),
% 0.07/0.48    inference(component_clause,[status(thm)],[f1911])).
% 0.07/0.48  fof(f1914,definition,(
% 0.07/0.48    sQ203_spl <=> (element(sK9_skl(sK11_skl),powerset(the_carrier(sK11_skl))))),
% 0.07/0.48    introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 0.07/0.48  fof(f1917,plain,(
% 0.07/0.48    ~sQ50_spl|~sQ202_spl|~sQ67_spl|~sQ59_spl|~sQ43_spl|sQ203_spl),
% 0.07/0.48    inference(split_clause,[status(thm)],[f1909,f920,f1911,f1024,f975,f869,f1914])).
% 0.07/0.49  fof(f1918,plain,(
% 0.07/0.49    $false|sQ67_spl),
% 0.07/0.49    inference(forward_subsumption_resolution,[status(thm)],[f1026,f405])).
% 0.07/0.49  fof(f1919,plain,(
% 0.07/0.49    sQ67_spl),
% 0.07/0.49    inference(contradiction_clause,[status(thm)],[f1918])).
% 0.07/0.49  fof(f1920,plain,(
% 0.07/0.49    $false|sQ202_spl),
% 0.07/0.49    inference(forward_subsumption_resolution,[status(thm)],[f1913,f404])).
% 0.07/0.49  fof(f1921,plain,(
% 0.07/0.49    sQ202_spl),
% 0.07/0.49    inference(contradiction_clause,[status(thm)],[f1920])).
% 0.07/0.49  fof(f1923,plain,(
% 0.07/0.49    ~reflexive_relstr(sK11_skl)|~transitive_relstr(sK11_skl)|~antisymmetric_relstr(sK11_skl)|~with_suprema_relstr(sK11_skl)|~rel_str(sK11_skl)|directed_subset(sK9_skl(sK11_skl),sK11_skl)),
% 0.07/0.49    inference(resolution,[status(thm)],[f388,f407])).
% 0.07/0.49  fof(f1925,definition,(
% 0.07/0.49    sQ204_spl <=> (directed_subset(sK9_skl(sK11_skl),sK11_skl))),
% 0.07/0.49    introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 0.07/0.49  fof(f1928,plain,(
% 0.07/0.49    ~sQ50_spl|~sQ202_spl|~sQ67_spl|~sQ59_spl|~sQ43_spl|sQ204_spl),
% 0.07/0.49    inference(split_clause,[status(thm)],[f1923,f920,f1911,f1024,f975,f869,f1925])).
% 0.07/0.49  fof(f1930,plain,(
% 0.07/0.49    ~reflexive_relstr(sK11_skl)|~transitive_relstr(sK11_skl)|~antisymmetric_relstr(sK11_skl)|~with_suprema_relstr(sK11_skl)|~rel_str(sK11_skl)|filtered_subset(sK9_skl(sK11_skl),sK11_skl)),
% 0.07/0.49    inference(resolution,[status(thm)],[f389,f407])).
% 0.07/0.49  fof(f1932,definition,(
% 0.07/0.49    sQ205_spl <=> (filtered_subset(sK9_skl(sK11_skl),sK11_skl))),
% 0.07/0.49    introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 0.07/0.49  fof(f1935,plain,(
% 0.07/0.49    ~sQ50_spl|~sQ202_spl|~sQ67_spl|~sQ59_spl|~sQ43_spl|sQ205_spl),
% 0.07/0.49    inference(split_clause,[status(thm)],[f1930,f920,f1911,f1024,f975,f869,f1932])).
% 0.07/0.49  fof(f1936,plain,(
% 0.07/0.49    sK45_skl=sK7_skl(sK45_skl,sK44_skl,sK43_skl)|~sQ187_spl|~sQ0_spl),
% 0.07/0.49    inference(resolution,[status(thm)],[f1806,f643])).
% 0.07/0.49  fof(f1937,plain,(
% 0.07/0.49    sK5_skl(neighborhood_system(sK43_skl,sK44_skl))=sK7_skl(sK5_skl(neighborhood_system(sK43_skl,sK44_skl)),sK44_skl,sK43_skl)|empty(neighborhood_system(sK43_skl,sK44_skl))|~sQ187_spl),
% 0.07/0.49    inference(resolution,[status(thm)],[f1806,f1156])).
% 0.07/0.49  fof(f1938,plain,(
% 0.07/0.49    point_neighbourhood(sK45_skl,sK43_skl,sK44_skl)|~sQ187_spl|~sQ0_spl|~sQ177_spl),
% 0.07/0.49    inference(backward_demodulation,[status(thm)],[f1936,f1856])).
% 0.07/0.49  fof(f1939,definition,(
% 0.07/0.49    sQ206_spl <=> (sK5_skl(neighborhood_system(sK43_skl,sK44_skl))=sK7_skl(sK5_skl(neighborhood_system(sK43_skl,sK44_skl)),sK44_skl,sK43_skl))),
% 0.07/0.49    introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 0.07/0.49  fof(f1942,plain,(
% 0.07/0.49    sQ206_spl|sQ7_spl|~sQ187_spl),
% 0.07/0.49    inference(split_clause,[status(thm)],[f1937,f1939,f685,f1805])).
% 0.07/0.49  fof(f1943,plain,(
% 0.07/0.49    sQ1_spl|~sQ187_spl|~sQ0_spl|~sQ177_spl),
% 0.07/0.49    inference(split_clause,[status(thm)],[f1938,f645,f1805,f642,f1734])).
% 0.07/0.49  fof(f1944,plain,(
% 0.07/0.49    $false),
% 0.07/0.49    inference(sat_refutation,[status(thm)],[f648,f649,f669,f673,f675,f677,f679,f695,f705,f712,f715,f716,f729,f734,f749,f754,f784,f786,f800,f804,f808,f815,f819,f826,f828,f850,f863,f875,f877,f882,f883,f890,f901,f905,f911,f915,f931,f933,f935,f945,f949,f955,f959,f965,f969,f998,f1000,f1002,f1011,f1012,f1029,f1066,f1070,f1074,f1078,f1082,f1090,f1094,f1097,f1103,f1107,f1111,f1113,f1119,f1133,f1163,f1190,f1194,f1198,f1202,f1206,f1210,f1214,f1218,f1219,f1220,f1222,f1223,f1227,f1231,f1235,f1251,f1261,f1276,f1281,f1285,f1294,f1296,f1305,f1310,f1314,f1376,f1382,f1386,f1390,f1412,f1414,f1503,f1511,f1513,f1524,f1544,f1553,f1554,f1555,f1556,f1557,f1592,f1606,f1610,f1612,f1630,f1638,f1640,f1647,f1661,f1678,f1691,f1698,f1710,f1733,f1737,f1739,f1741,f1743,f1770,f1781,f1785,f1791,f1793,f1796,f1804,f1808,f1814,f1818,f1822,f1837,f1841,f1846,f1850,f1852,f1872,f1876,f1881,f1885,f1894,f1898,f1903,f1907,f1917,f1919,f1921,f1928,f1935,f1942,f1943])).
% 0.07/0.49  % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.50  % Elapsed time: 0.127003 seconds
% 0.24/0.50  % CPU time: 0.691097 seconds
% 0.24/0.50  % Total memory used: 107.445 MB
% 0.24/0.50  % Net memory used: 106.852 MB
%------------------------------------------------------------------------------