FindProof---0.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : SEU388+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n026.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 : Fri Sep 25 02:51:55 PM UTC 2026

% Result   : Theorem 121.12s 16.54s
% Output   : Proof 121.12s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SEU388+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38  % Computer : n026.cluster.edu
% 0.10/0.38  % Model    : x86_64 x86_64
% 0.10/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38  % Memory   : 8046.5625MB
% 0.10/0.38  % OS       : Linux 6.8.0-71-generic
% 0.10/0.38  % CPULimit : 300
% 0.10/0.38  % WCLimit  : 300
% 0.10/0.38  % DateTime : Thu Sep 24 13:59:54 UTC 2026
% 0.10/0.38  % CPUTime  : 
% 0.10/0.38  Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 121.12/16.54  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 121.12/16.54  % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 121.12/16.54  fof(sdef3, definition, (spl3 <=> (~point_neighbourhood(sk45,sk43,sk44))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 121.12/16.54  cnf(p386, plain, (~point_neighbourhood(sk45,sk43,sk44) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 121.12/16.54  fof(sdef2, definition, (spl2 <=> (point_neighbourhood(sk45,sk43,sk44))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 121.12/16.54  cnf(p384, plain, (point_neighbourhood(sk45,sk43,sk44) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 121.12/16.54  cnf(p393, plain, ($false | ~spl2 | ~spl3), inference(resolution, [status(thm)], [p386, p384])).
% 121.12/16.54  cnf(sct0, plain, (~spl2 | ~spl3), inference(avatar_contradiction_clause, [status(thm)], [p393])).
% 121.12/16.54  fof(sdef1, definition, (spl1 <=> (~in(sk45,neighborhood_system(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 121.12/16.54  cnf(p382, plain, (~in(sk45,neighborhood_system(sk43,sk44)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 121.12/16.54  fof(sdef0, definition, (spl0 <=> (in(sk45,neighborhood_system(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 121.12/16.54  cnf(p381, plain, (in(sk45,neighborhood_system(sk43,sk44)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 121.12/16.54  cnf(p394, plain, ($false | ~spl0 | ~spl1), inference(resolution, [status(thm)], [p382, p381])).
% 121.12/16.54  cnf(sct1, plain, (~spl0 | ~spl1), inference(avatar_contradiction_clause, [status(thm)], [p394])).
% 121.12/16.54  fof(sdef13, definition, (spl13 <=> (empty_carrier(sk10))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 121.12/16.54  cnf(p411, plain, (empty_carrier(sk10) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 121.12/16.54  fof(f75, axiom, ? [A] : ( rel_str(A) & ~ empty_carrier(A) & reflexive_relstr(A) & transitive_relstr(A) & antisymmetric_relstr(A) & connected_relstr(A) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc12_waybel_0)).
% 121.12/16.54  fof(f75_nnf, plain, ? [A] : ((((((rel_str(A) & ~(empty_carrier(A))) & reflexive_relstr(A)) & transitive_relstr(A)) & antisymmetric_relstr(A)) & connected_relstr(A))), inference(nnf_transformation, [status(thm)], [f75])).
% 121.12/16.54  fof(f75_sk, plain, (((((rel_str(sk10) & ~(empty_carrier(sk10))) & reflexive_relstr(sk10)) & transitive_relstr(sk10)) & antisymmetric_relstr(sk10)) & connected_relstr(sk10)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk10])], [f75_nnf])).
% 121.12/16.54  cnf(c207, plain, ~empty_carrier(sk10), inference(cnf_transformation, [status(esa)], [f75_sk])).
% 121.12/16.54  cnf(p593, plain, ($false | ~spl13), inference(resolution, [status(thm)], [p411, c207])).
% 121.12/16.54  cnf(sct2, plain, (~spl13), inference(avatar_contradiction_clause, [status(thm)], [p593])).
% 121.12/16.54  fof(sdef14, definition, (spl14 <=> (~reflexive_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 121.12/16.54  cnf(p412, plain, (~reflexive_relstr(sk10) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 121.12/16.54  cnf(c208, plain, reflexive_relstr(sk10), inference(cnf_transformation, [status(esa)], [f75_sk])).
% 121.12/16.54  cnf(p594, plain, ($false | ~spl14), inference(resolution, [status(thm)], [p412, c208])).
% 121.12/16.54  cnf(sct3, plain, (~spl14), inference(avatar_contradiction_clause, [status(thm)], [p594])).
% 121.12/16.54  fof(sdef18, definition, (spl18 <=> (~strict_rel_str(sk11))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 121.12/16.54  cnf(p418, plain, (~strict_rel_str(sk11) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 121.12/16.54  fof(f76, axiom, ? [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) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc13_waybel_0)).
% 121.12/16.54  fof(f76_nnf, plain, ? [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))), inference(nnf_transformation, [status(thm)], [f76])).
% 121.12/16.54  fof(f76_sk, plain, (((((((((((((rel_str(sk11) & ~(empty_carrier(sk11))) & strict_rel_str(sk11)) & reflexive_relstr(sk11)) & transitive_relstr(sk11)) & antisymmetric_relstr(sk11)) & with_suprema_relstr(sk11)) & with_infima_relstr(sk11)) & complete_relstr(sk11)) & lower_bounded_relstr(sk11)) & upper_bounded_relstr(sk11)) & bounded_relstr(sk11)) & up_complete_relstr(sk11)) & join_complete_relstr(sk11)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk11])], [f76_nnf])).
% 121.12/16.54  cnf(c214, plain, strict_rel_str(sk11), inference(cnf_transformation, [status(esa)], [f76_sk])).
% 121.12/16.54  cnf(p595, plain, ($false | ~spl18), inference(resolution, [status(thm)], [p418, c214])).
% 121.12/16.54  cnf(sct4, plain, (~spl18), inference(avatar_contradiction_clause, [status(thm)], [p595])).
% 121.12/16.54  fof(sdef20, definition, (spl20 <=> (~join_complete_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 121.12/16.54  cnf(p421, plain, (~join_complete_relstr(sk0) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 121.12/16.54  fof(sdef10, definition, (spl10 <=> (join_complete_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 121.12/16.54  cnf(p406, plain, (join_complete_relstr(sk0) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 121.12/16.54  cnf(p596, plain, ($false | ~spl10 | ~spl20), inference(resolution, [status(thm)], [p421, p406])).
% 121.12/16.54  cnf(sct5, plain, (~spl10 | ~spl20), inference(avatar_contradiction_clause, [status(thm)], [p596])).
% 121.12/16.54  fof(sdef22, definition, (spl22 <=> (~join_complete_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 121.12/16.54  cnf(p424, plain, (~join_complete_relstr(sk10) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 121.12/16.54  fof(sdef17, definition, (spl17 <=> (join_complete_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 121.12/16.54  cnf(p416, plain, (join_complete_relstr(sk10) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 121.12/16.54  cnf(p597, plain, ($false | ~spl17 | ~spl22), inference(resolution, [status(thm)], [p424, p416])).
% 121.12/16.54  cnf(sct6, plain, (~spl17 | ~spl22), inference(avatar_contradiction_clause, [status(thm)], [p597])).
% 121.12/16.54  fof(sdef24, definition, (spl24 <=> (~strict_rel_str(sk13))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 121.12/16.54  cnf(p427, plain, (~strict_rel_str(sk13) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 121.12/16.54  fof(f78, axiom, ? [A] : ( rel_str(A) & ~ empty_carrier(A) & strict_rel_str(A) & reflexive_relstr(A) & transitive_relstr(A) & antisymmetric_relstr(A) & complete_relstr(A) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc1_lattice3)).
% 121.12/16.54  fof(f78_nnf, plain, ? [A] : (((((((rel_str(A) & ~(empty_carrier(A))) & strict_rel_str(A)) & reflexive_relstr(A)) & transitive_relstr(A)) & antisymmetric_relstr(A)) & complete_relstr(A))), inference(nnf_transformation, [status(thm)], [f78])).
% 121.12/16.54  fof(f78_sk, plain, ((((((rel_str(sk13) & ~(empty_carrier(sk13))) & strict_rel_str(sk13)) & reflexive_relstr(sk13)) & transitive_relstr(sk13)) & antisymmetric_relstr(sk13)) & complete_relstr(sk13)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk13])], [f78_nnf])).
% 121.12/16.54  cnf(c230, plain, strict_rel_str(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p598, plain, ($false | ~spl24), inference(resolution, [status(thm)], [p427, c230])).
% 121.12/16.54  cnf(sct7, plain, (~spl24), inference(avatar_contradiction_clause, [status(thm)], [p598])).
% 121.12/16.54  fof(sdef26, definition, (spl26 <=> (empty_carrier(sk13))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 121.12/16.54  cnf(p430, plain, (empty_carrier(sk13) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 121.12/16.54  cnf(c229, plain, ~empty_carrier(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p599, plain, ($false | ~spl26), inference(resolution, [status(thm)], [p430, c229])).
% 121.12/16.54  cnf(sct8, plain, (~spl26), inference(avatar_contradiction_clause, [status(thm)], [p599])).
% 121.12/16.54  fof(sdef138, definition, (spl138 <=> (~top_str(sk43))), introduced(definition, [new_symbols(naming, [spl138])], [avatar_definition])).
% 121.12/16.54  cnf(p601, plain, (~top_str(sk43) | ~spl138), inference(avatar_component_clause, [status(thm)], [sdef138])).
% 121.12/16.54  fof(f113, conjecture, ! [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) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_yellow19)).
% 121.12/16.54  fof(f113_neg, negated_conjecture, ~(! [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) ) ) )), inference(negated_conjecture, [status(cth)], [f113])).
% 121.12/16.54  fof(f113_nnf, plain, ? [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)))))))), inference(nnf_transformation, [status(thm)], [f113_neg])).
% 121.12/16.54  fof(f113_sk, plain, (((~(empty_carrier(sk43)) & topological_space(sk43)) & top_str(sk43)) & (element(sk44,the_carrier(sk43)) & ((in(sk45,neighborhood_system(sk43,sk44)) & ~(point_neighbourhood(sk45,sk43,sk44))) | (~(in(sk45,neighborhood_system(sk43,sk44))) & point_neighbourhood(sk45,sk43,sk44))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk43,sk44,sk45])], [f113_nnf])).
% 121.12/16.54  cnf(c378, plain, top_str(sk43), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(p603, plain, ($false | ~spl138), inference(resolution, [status(thm)], [p601, c378])).
% 121.12/16.54  cnf(sct9, plain, (~spl138), inference(avatar_contradiction_clause, [status(thm)], [p603])).
% 121.12/16.54  fof(sdef27, definition, (spl27 <=> (~reflexive_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 121.12/16.54  cnf(p431, plain, (~reflexive_relstr(sk13) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 121.12/16.54  cnf(c231, plain, reflexive_relstr(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p604, plain, ($false | ~spl27), inference(resolution, [status(thm)], [p431, c231])).
% 121.12/16.54  cnf(sct10, plain, (~spl27), inference(avatar_contradiction_clause, [status(thm)], [p604])).
% 121.12/16.54  fof(sdef28, definition, (spl28 <=> (~complete_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 121.12/16.54  cnf(p432, plain, (~complete_relstr(sk13) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 121.12/16.54  cnf(c234, plain, complete_relstr(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p605, plain, ($false | ~spl28), inference(resolution, [status(thm)], [p432, c234])).
% 121.12/16.54  cnf(sct11, plain, (~spl28), inference(avatar_contradiction_clause, [status(thm)], [p605])).
% 121.12/16.54  fof(sdef31, definition, (spl31 <=> (~join_complete_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 121.12/16.54  cnf(p437, plain, (~join_complete_relstr(sk13) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 121.12/16.54  fof(sdef30, definition, (spl30 <=> (join_complete_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 121.12/16.54  cnf(p435, plain, (join_complete_relstr(sk13) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 121.12/16.54  cnf(p608, plain, ($false | ~spl30 | ~spl31), inference(resolution, [status(thm)], [p437, p435])).
% 121.12/16.54  cnf(sct12, plain, (~spl30 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p608])).
% 121.12/16.54  fof(sdef33, definition, (spl33 <=> (~strict_rel_str(sk18))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 121.12/16.54  cnf(p440, plain, (~strict_rel_str(sk18) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 121.12/16.54  fof(f83, axiom, ? [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) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc1_waybel_7)).
% 121.12/16.54  fof(f83_nnf, plain, ? [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))), inference(nnf_transformation, [status(thm)], [f83])).
% 121.12/16.54  fof(f83_sk, plain, ((((((((((((((((rel_str(sk18) & ~(empty_carrier(sk18))) & ~(trivial_carrier(sk18))) & strict_rel_str(sk18)) & reflexive_relstr(sk18)) & transitive_relstr(sk18)) & antisymmetric_relstr(sk18)) & lower_bounded_relstr(sk18)) & upper_bounded_relstr(sk18)) & bounded_relstr(sk18)) & ~(v1_yellow_3(sk18))) & distributive_relstr(sk18)) & heyting_relstr(sk18)) & complemented_relstr(sk18)) & boolean_relstr(sk18)) & with_suprema_relstr(sk18)) & with_infima_relstr(sk18)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk18])], [f83_nnf])).
% 121.12/16.54  cnf(c247, plain, strict_rel_str(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p609, plain, ($false | ~spl33), inference(resolution, [status(thm)], [p440, c247])).
% 121.12/16.54  cnf(sct13, plain, (~spl33), inference(avatar_contradiction_clause, [status(thm)], [p609])).
% 121.12/16.54  fof(sdef35, definition, (spl35 <=> (empty_carrier(sk18))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 121.12/16.54  cnf(p443, plain, (empty_carrier(sk18) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 121.12/16.54  cnf(c245, plain, ~empty_carrier(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p610, plain, ($false | ~spl35), inference(resolution, [status(thm)], [p443, c245])).
% 121.12/16.54  cnf(sct14, plain, (~spl35), inference(avatar_contradiction_clause, [status(thm)], [p610])).
% 121.12/16.54  fof(sdef36, definition, (spl36 <=> (~reflexive_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 121.12/16.54  cnf(p444, plain, (~reflexive_relstr(sk18) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 121.12/16.54  cnf(c248, plain, reflexive_relstr(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p611, plain, ($false | ~spl36), inference(resolution, [status(thm)], [p444, c248])).
% 121.12/16.54  cnf(sct15, plain, (~spl36), inference(avatar_contradiction_clause, [status(thm)], [p611])).
% 121.12/16.54  fof(sdef43, definition, (spl43 <=> (~lower_bounded_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 121.12/16.54  cnf(p453, plain, (~lower_bounded_relstr(sk0) | ~spl43), inference(avatar_component_clause, [status(thm)], [sdef43])).
% 121.12/16.54  fof(sdef21, definition, (spl21 <=> (lower_bounded_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 121.12/16.54  cnf(p422, plain, (lower_bounded_relstr(sk0) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 121.12/16.54  cnf(p620, plain, ($false | ~spl21 | ~spl43), inference(resolution, [status(thm)], [p453, p422])).
% 121.12/16.54  cnf(sct16, plain, (~spl21 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p620])).
% 121.12/16.54  fof(sdef44, definition, (spl44 <=> (~up_complete_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 121.12/16.54  cnf(p454, plain, (~up_complete_relstr(sk0) | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 121.12/16.54  fof(sdef9, definition, (spl9 <=> (up_complete_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 121.12/16.54  cnf(p404, plain, (up_complete_relstr(sk0) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 121.12/16.54  cnf(p621, plain, ($false | ~spl9 | ~spl44), inference(resolution, [status(thm)], [p454, p404])).
% 121.12/16.54  cnf(sct17, plain, (~spl9 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p621])).
% 121.12/16.54  fof(sdef46, definition, (spl46 <=> (~transitive_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 121.12/16.54  cnf(p457, plain, (~transitive_relstr(sk10) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 121.12/16.54  cnf(c209, plain, transitive_relstr(sk10), inference(cnf_transformation, [status(esa)], [f75_sk])).
% 121.12/16.54  cnf(p623, plain, ($false | ~spl46), inference(resolution, [status(thm)], [p457, c209])).
% 121.12/16.54  cnf(sct18, plain, (~spl46), inference(avatar_contradiction_clause, [status(thm)], [p623])).
% 121.12/16.54  fof(sdef47, definition, (spl47 <=> (~antisymmetric_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 121.12/16.54  cnf(p458, plain, (~antisymmetric_relstr(sk10) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 121.12/16.54  cnf(c210, plain, antisymmetric_relstr(sk10), inference(cnf_transformation, [status(esa)], [f75_sk])).
% 121.12/16.54  cnf(p624, plain, ($false | ~spl47), inference(resolution, [status(thm)], [p458, c210])).
% 121.12/16.54  cnf(sct19, plain, (~spl47), inference(avatar_contradiction_clause, [status(thm)], [p624])).
% 121.12/16.54  fof(sdef49, definition, (spl49 <=> (~lower_bounded_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 121.12/16.54  cnf(p460, plain, (~lower_bounded_relstr(sk10) | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 121.12/16.54  fof(sdef23, definition, (spl23 <=> (lower_bounded_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 121.12/16.54  cnf(p425, plain, (lower_bounded_relstr(sk10) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 121.12/16.54  cnf(p627, plain, ($false | ~spl23 | ~spl49), inference(resolution, [status(thm)], [p460, p425])).
% 121.12/16.54  cnf(sct20, plain, (~spl23 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p627])).
% 121.12/16.54  fof(sdef50, definition, (spl50 <=> (~up_complete_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 121.12/16.54  cnf(p461, plain, (~up_complete_relstr(sk10) | ~spl50), inference(avatar_component_clause, [status(thm)], [sdef50])).
% 121.12/16.54  fof(sdef16, definition, (spl16 <=> (up_complete_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 121.12/16.54  cnf(p414, plain, (up_complete_relstr(sk10) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 121.12/16.54  cnf(p628, plain, ($false | ~spl16 | ~spl50), inference(resolution, [status(thm)], [p461, p414])).
% 121.12/16.54  cnf(sct21, plain, (~spl16 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p628])).
% 121.12/16.54  fof(sdef52, definition, (spl52 <=> (~transitive_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 121.12/16.54  cnf(p464, plain, (~transitive_relstr(sk13) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 121.12/16.54  cnf(c232, plain, transitive_relstr(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p629, plain, ($false | ~spl52), inference(resolution, [status(thm)], [p464, c232])).
% 121.12/16.54  cnf(sct22, plain, (~spl52), inference(avatar_contradiction_clause, [status(thm)], [p629])).
% 121.12/16.54  fof(sdef53, definition, (spl53 <=> (~antisymmetric_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 121.12/16.54  cnf(p465, plain, (~antisymmetric_relstr(sk13) | ~spl53), inference(avatar_component_clause, [status(thm)], [sdef53])).
% 121.12/16.54  cnf(c233, plain, antisymmetric_relstr(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p632, plain, ($false | ~spl53), inference(resolution, [status(thm)], [p465, c233])).
% 121.12/16.54  cnf(sct23, plain, (~spl53), inference(avatar_contradiction_clause, [status(thm)], [p632])).
% 121.12/16.54  fof(sdef55, definition, (spl55 <=> (~lower_bounded_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 121.12/16.54  cnf(p467, plain, (~lower_bounded_relstr(sk13) | ~spl55), inference(avatar_component_clause, [status(thm)], [sdef55])).
% 121.12/16.54  fof(sdef32, definition, (spl32 <=> (lower_bounded_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 121.12/16.54  cnf(p438, plain, (lower_bounded_relstr(sk13) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 121.12/16.54  cnf(p633, plain, ($false | ~spl32 | ~spl55), inference(resolution, [status(thm)], [p467, p438])).
% 121.12/16.54  cnf(sct24, plain, (~spl32 | ~spl55), inference(avatar_contradiction_clause, [status(thm)], [p633])).
% 121.12/16.54  fof(sdef56, definition, (spl56 <=> (~up_complete_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 121.12/16.54  cnf(p468, plain, (~up_complete_relstr(sk13) | ~spl56), inference(avatar_component_clause, [status(thm)], [sdef56])).
% 121.12/16.54  fof(sdef29, definition, (spl29 <=> (up_complete_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 121.12/16.54  cnf(p433, plain, (up_complete_relstr(sk13) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 121.12/16.54  cnf(p634, plain, ($false | ~spl29 | ~spl56), inference(resolution, [status(thm)], [p468, p433])).
% 121.12/16.54  cnf(sct25, plain, (~spl29 | ~spl56), inference(avatar_contradiction_clause, [status(thm)], [p634])).
% 121.12/16.54  fof(sdef58, definition, (spl58 <=> (complete_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 121.12/16.54  cnf(p471, plain, (complete_relstr(sk0) | ~spl58), inference(avatar_component_clause, [status(thm)], [sdef58])).
% 121.12/16.54  fof(sdef8, definition, (spl8 <=> (~complete_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 121.12/16.54  cnf(p403, plain, (~complete_relstr(sk0) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 121.12/16.54  cnf(p635, plain, ($false | ~spl8 | ~spl58), inference(resolution, [status(thm)], [p471, p403])).
% 121.12/16.54  cnf(sct26, plain, (~spl8 | ~spl58), inference(avatar_contradiction_clause, [status(thm)], [p635])).
% 121.12/16.54  fof(sdef59, definition, (spl59 <=> (complete_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 121.12/16.54  cnf(p473, plain, (complete_relstr(sk10) | ~spl59), inference(avatar_component_clause, [status(thm)], [sdef59])).
% 121.12/16.54  fof(sdef15, definition, (spl15 <=> (~complete_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 121.12/16.54  cnf(p413, plain, (~complete_relstr(sk10) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 121.12/16.54  cnf(p636, plain, ($false | ~spl15 | ~spl59), inference(resolution, [status(thm)], [p473, p413])).
% 121.12/16.54  cnf(sct27, plain, (~spl15 | ~spl59), inference(avatar_contradiction_clause, [status(thm)], [p636])).
% 121.12/16.54  fof(sdef60, definition, (spl60 <=> (~transitive_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 121.12/16.54  cnf(p475, plain, (~transitive_relstr(sk18) | ~spl60), inference(avatar_component_clause, [status(thm)], [sdef60])).
% 121.12/16.54  cnf(c249, plain, transitive_relstr(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p637, plain, ($false | ~spl60), inference(resolution, [status(thm)], [p475, c249])).
% 121.12/16.54  cnf(sct28, plain, (~spl60), inference(avatar_contradiction_clause, [status(thm)], [p637])).
% 121.12/16.54  fof(sdef61, definition, (spl61 <=> (~antisymmetric_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 121.12/16.54  cnf(p476, plain, (~antisymmetric_relstr(sk18) | ~spl61), inference(avatar_component_clause, [status(thm)], [sdef61])).
% 121.12/16.54  cnf(c250, plain, antisymmetric_relstr(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p638, plain, ($false | ~spl61), inference(resolution, [status(thm)], [p476, c250])).
% 121.12/16.54  cnf(sct29, plain, (~spl61), inference(avatar_contradiction_clause, [status(thm)], [p638])).
% 121.12/16.54  fof(sdef62, definition, (spl62 <=> (~with_suprema_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 121.12/16.54  cnf(p477, plain, (~with_suprema_relstr(sk18) | ~spl62), inference(avatar_component_clause, [status(thm)], [sdef62])).
% 121.12/16.54  cnf(c259, plain, with_suprema_relstr(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p639, plain, ($false | ~spl62), inference(resolution, [status(thm)], [p477, c259])).
% 121.12/16.54  cnf(sct30, plain, (~spl62), inference(avatar_contradiction_clause, [status(thm)], [p639])).
% 121.12/16.54  fof(sdef63, definition, (spl63 <=> (~lower_bounded_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 121.12/16.54  cnf(p478, plain, (~lower_bounded_relstr(sk18) | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 121.12/16.54  cnf(c251, plain, lower_bounded_relstr(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p640, plain, ($false | ~spl63), inference(resolution, [status(thm)], [p478, c251])).
% 121.12/16.54  cnf(sct31, plain, (~spl63), inference(avatar_contradiction_clause, [status(thm)], [p640])).
% 121.12/16.54  fof(sdef64, definition, (spl64 <=> (~up_complete_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 121.12/16.54  cnf(p479, plain, (~up_complete_relstr(sk18) | ~spl64), inference(avatar_component_clause, [status(thm)], [sdef64])).
% 121.12/16.54  fof(sdef38, definition, (spl38 <=> (up_complete_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 121.12/16.54  cnf(p446, plain, (up_complete_relstr(sk18) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 121.12/16.54  cnf(p644, plain, ($false | ~spl38 | ~spl64), inference(resolution, [status(thm)], [p479, p446])).
% 121.12/16.54  cnf(sct32, plain, (~spl38 | ~spl64), inference(avatar_contradiction_clause, [status(thm)], [p644])).
% 121.12/16.54  fof(sdef65, definition, (spl65 <=> (complete_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 121.12/16.54  cnf(p480, plain, (complete_relstr(sk18) | ~spl65), inference(avatar_component_clause, [status(thm)], [sdef65])).
% 121.12/16.54  fof(sdef37, definition, (spl37 <=> (~complete_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 121.12/16.54  cnf(p445, plain, (~complete_relstr(sk18) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 121.12/16.54  cnf(p645, plain, ($false | ~spl37 | ~spl65), inference(resolution, [status(thm)], [p480, p445])).
% 121.12/16.54  cnf(sct33, plain, (~spl37 | ~spl65), inference(avatar_contradiction_clause, [status(thm)], [p645])).
% 121.12/16.54  fof(sdef69, definition, (spl69 <=> (~strict_rel_str(sk19))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 121.12/16.54  cnf(p488, plain, (~strict_rel_str(sk19) | ~spl69), inference(avatar_component_clause, [status(thm)], [sdef69])).
% 121.12/16.54  fof(f84, axiom, ? [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) & trivial_carrier(A) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc1_yellow_0)).
% 121.12/16.54  fof(f84_nnf, plain, ? [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)) & trivial_carrier(A))), inference(nnf_transformation, [status(thm)], [f84])).
% 121.12/16.54  fof(f84_sk, plain, (((((((((rel_str(sk19) & ~(empty_carrier(sk19))) & strict_rel_str(sk19)) & reflexive_relstr(sk19)) & transitive_relstr(sk19)) & antisymmetric_relstr(sk19)) & with_suprema_relstr(sk19)) & with_infima_relstr(sk19)) & complete_relstr(sk19)) & trivial_carrier(sk19)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk19])], [f84_nnf])).
% 121.12/16.54  cnf(c263, plain, strict_rel_str(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p651, plain, ($false | ~spl69), inference(resolution, [status(thm)], [p488, c263])).
% 121.12/16.54  cnf(sct34, plain, (~spl69), inference(avatar_contradiction_clause, [status(thm)], [p651])).
% 121.12/16.54  fof(sdef71, definition, (spl71 <=> (empty_carrier(sk19))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 121.12/16.54  cnf(p491, plain, (empty_carrier(sk19) | ~spl71), inference(avatar_component_clause, [status(thm)], [sdef71])).
% 121.12/16.54  cnf(c262, plain, ~empty_carrier(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p652, plain, ($false | ~spl71), inference(resolution, [status(thm)], [p491, c262])).
% 121.12/16.54  cnf(sct35, plain, (~spl71), inference(avatar_contradiction_clause, [status(thm)], [p652])).
% 121.12/16.54  fof(sdef72, definition, (spl72 <=> (~reflexive_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 121.12/16.54  cnf(p492, plain, (~reflexive_relstr(sk19) | ~spl72), inference(avatar_component_clause, [status(thm)], [sdef72])).
% 121.12/16.54  cnf(c264, plain, reflexive_relstr(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p653, plain, ($false | ~spl72), inference(resolution, [status(thm)], [p492, c264])).
% 121.12/16.54  cnf(sct36, plain, (~spl72), inference(avatar_contradiction_clause, [status(thm)], [p653])).
% 121.12/16.54  fof(sdef73, definition, (spl73 <=> (~complete_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 121.12/16.54  cnf(p493, plain, (~complete_relstr(sk19) | ~spl73), inference(avatar_component_clause, [status(thm)], [sdef73])).
% 121.12/16.54  cnf(c269, plain, complete_relstr(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p658, plain, ($false | ~spl73), inference(resolution, [status(thm)], [p493, c269])).
% 121.12/16.54  cnf(sct37, plain, (~spl73), inference(avatar_contradiction_clause, [status(thm)], [p658])).
% 121.12/16.54  fof(sdef76, definition, (spl76 <=> (~join_complete_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 121.12/16.54  cnf(p498, plain, (~join_complete_relstr(sk19) | ~spl76), inference(avatar_component_clause, [status(thm)], [sdef76])).
% 121.12/16.54  fof(sdef75, definition, (spl75 <=> (join_complete_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 121.12/16.54  cnf(p496, plain, (join_complete_relstr(sk19) | ~spl75), inference(avatar_component_clause, [status(thm)], [sdef75])).
% 121.12/16.54  cnf(p659, plain, ($false | ~spl75 | ~spl76), inference(resolution, [status(thm)], [p498, p496])).
% 121.12/16.54  cnf(sct38, plain, (~spl75 | ~spl76), inference(avatar_contradiction_clause, [status(thm)], [p659])).
% 121.12/16.54  fof(sdef78, definition, (spl78 <=> (~transitive_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 121.12/16.54  cnf(p501, plain, (~transitive_relstr(sk19) | ~spl78), inference(avatar_component_clause, [status(thm)], [sdef78])).
% 121.12/16.54  cnf(c265, plain, transitive_relstr(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p662, plain, ($false | ~spl78), inference(resolution, [status(thm)], [p501, c265])).
% 121.12/16.54  cnf(sct39, plain, (~spl78), inference(avatar_contradiction_clause, [status(thm)], [p662])).
% 121.12/16.54  fof(sdef79, definition, (spl79 <=> (~antisymmetric_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 121.12/16.54  cnf(p502, plain, (~antisymmetric_relstr(sk19) | ~spl79), inference(avatar_component_clause, [status(thm)], [sdef79])).
% 121.12/16.54  cnf(c266, plain, antisymmetric_relstr(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p663, plain, ($false | ~spl79), inference(resolution, [status(thm)], [p502, c266])).
% 121.12/16.54  cnf(sct40, plain, (~spl79), inference(avatar_contradiction_clause, [status(thm)], [p663])).
% 121.12/16.54  fof(sdef80, definition, (spl80 <=> (~with_suprema_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 121.12/16.54  cnf(p503, plain, (~with_suprema_relstr(sk19) | ~spl80), inference(avatar_component_clause, [status(thm)], [sdef80])).
% 121.12/16.54  cnf(c267, plain, with_suprema_relstr(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p664, plain, ($false | ~spl80), inference(resolution, [status(thm)], [p503, c267])).
% 121.12/16.54  cnf(sct41, plain, (~spl80), inference(avatar_contradiction_clause, [status(thm)], [p664])).
% 121.12/16.54  fof(sdef81, definition, (spl81 <=> (~lower_bounded_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 121.12/16.54  cnf(p504, plain, (~lower_bounded_relstr(sk19) | ~spl81), inference(avatar_component_clause, [status(thm)], [sdef81])).
% 121.12/16.54  fof(sdef77, definition, (spl77 <=> (lower_bounded_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 121.12/16.54  cnf(p499, plain, (lower_bounded_relstr(sk19) | ~spl77), inference(avatar_component_clause, [status(thm)], [sdef77])).
% 121.12/16.54  cnf(p665, plain, ($false | ~spl77 | ~spl81), inference(resolution, [status(thm)], [p504, p499])).
% 121.12/16.54  cnf(sct42, plain, (~spl77 | ~spl81), inference(avatar_contradiction_clause, [status(thm)], [p665])).
% 121.12/16.54  fof(sdef82, definition, (spl82 <=> (~up_complete_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 121.12/16.54  cnf(p505, plain, (~up_complete_relstr(sk19) | ~spl82), inference(avatar_component_clause, [status(thm)], [sdef82])).
% 121.12/16.54  fof(sdef74, definition, (spl74 <=> (up_complete_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 121.12/16.54  cnf(p494, plain, (up_complete_relstr(sk19) | ~spl74), inference(avatar_component_clause, [status(thm)], [sdef74])).
% 121.12/16.54  cnf(p666, plain, ($false | ~spl74 | ~spl82), inference(resolution, [status(thm)], [p505, p494])).
% 121.12/16.54  cnf(sct43, plain, (~spl74 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p666])).
% 121.12/16.54  fof(sdef88, definition, (spl88 <=> (~strict_rel_str(sk20))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 121.12/16.54  cnf(p516, plain, (~strict_rel_str(sk20) | ~spl88), inference(avatar_component_clause, [status(thm)], [sdef88])).
% 121.12/16.54  fof(f85, axiom, ? [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) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc2_lattice3)).
% 121.12/16.54  fof(f85_nnf, plain, ? [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))), inference(nnf_transformation, [status(thm)], [f85])).
% 121.12/16.54  fof(f85_sk, plain, ((((((((rel_str(sk20) & ~(empty_carrier(sk20))) & strict_rel_str(sk20)) & reflexive_relstr(sk20)) & transitive_relstr(sk20)) & antisymmetric_relstr(sk20)) & with_suprema_relstr(sk20)) & with_infima_relstr(sk20)) & complete_relstr(sk20)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk20])], [f85_nnf])).
% 121.12/16.54  cnf(c273, plain, strict_rel_str(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p675, plain, ($false | ~spl88), inference(resolution, [status(thm)], [p516, c273])).
% 121.12/16.54  cnf(sct44, plain, (~spl88), inference(avatar_contradiction_clause, [status(thm)], [p675])).
% 121.12/16.54  fof(sdef90, definition, (spl90 <=> (empty_carrier(sk20))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 121.12/16.54  cnf(p519, plain, (empty_carrier(sk20) | ~spl90), inference(avatar_component_clause, [status(thm)], [sdef90])).
% 121.12/16.54  cnf(c272, plain, ~empty_carrier(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p676, plain, ($false | ~spl90), inference(resolution, [status(thm)], [p519, c272])).
% 121.12/16.54  cnf(sct45, plain, (~spl90), inference(avatar_contradiction_clause, [status(thm)], [p676])).
% 121.12/16.54  fof(sdef91, definition, (spl91 <=> (~reflexive_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 121.12/16.54  cnf(p520, plain, (~reflexive_relstr(sk20) | ~spl91), inference(avatar_component_clause, [status(thm)], [sdef91])).
% 121.12/16.54  cnf(c274, plain, reflexive_relstr(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p677, plain, ($false | ~spl91), inference(resolution, [status(thm)], [p520, c274])).
% 121.12/16.54  cnf(sct46, plain, (~spl91), inference(avatar_contradiction_clause, [status(thm)], [p677])).
% 121.12/16.54  fof(sdef92, definition, (spl92 <=> (~complete_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 121.12/16.54  cnf(p521, plain, (~complete_relstr(sk20) | ~spl92), inference(avatar_component_clause, [status(thm)], [sdef92])).
% 121.12/16.54  cnf(c279, plain, complete_relstr(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p690, plain, ($false | ~spl92), inference(resolution, [status(thm)], [p521, c279])).
% 121.12/16.54  cnf(sct47, plain, (~spl92), inference(avatar_contradiction_clause, [status(thm)], [p690])).
% 121.12/16.54  fof(sdef95, definition, (spl95 <=> (~join_complete_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 121.12/16.54  cnf(p526, plain, (~join_complete_relstr(sk20) | ~spl95), inference(avatar_component_clause, [status(thm)], [sdef95])).
% 121.12/16.54  fof(sdef94, definition, (spl94 <=> (join_complete_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 121.12/16.54  cnf(p524, plain, (join_complete_relstr(sk20) | ~spl94), inference(avatar_component_clause, [status(thm)], [sdef94])).
% 121.12/16.54  cnf(p697, plain, ($false | ~spl94 | ~spl95), inference(resolution, [status(thm)], [p526, p524])).
% 121.12/16.54  cnf(sct48, plain, (~spl94 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p697])).
% 121.12/16.54  fof(sdef97, definition, (spl97 <=> (~transitive_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 121.12/16.54  cnf(p529, plain, (~transitive_relstr(sk20) | ~spl97), inference(avatar_component_clause, [status(thm)], [sdef97])).
% 121.12/16.54  cnf(c275, plain, transitive_relstr(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p698, plain, ($false | ~spl97), inference(resolution, [status(thm)], [p529, c275])).
% 121.12/16.54  cnf(sct49, plain, (~spl97), inference(avatar_contradiction_clause, [status(thm)], [p698])).
% 121.12/16.54  fof(sdef98, definition, (spl98 <=> (~antisymmetric_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl98])], [avatar_definition])).
% 121.12/16.54  cnf(p530, plain, (~antisymmetric_relstr(sk20) | ~spl98), inference(avatar_component_clause, [status(thm)], [sdef98])).
% 121.12/16.54  cnf(c276, plain, antisymmetric_relstr(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p699, plain, ($false | ~spl98), inference(resolution, [status(thm)], [p530, c276])).
% 121.12/16.54  cnf(sct50, plain, (~spl98), inference(avatar_contradiction_clause, [status(thm)], [p699])).
% 121.12/16.54  fof(sdef99, definition, (spl99 <=> (~with_suprema_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl99])], [avatar_definition])).
% 121.12/16.54  cnf(p531, plain, (~with_suprema_relstr(sk20) | ~spl99), inference(avatar_component_clause, [status(thm)], [sdef99])).
% 121.12/16.54  cnf(c277, plain, with_suprema_relstr(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p700, plain, ($false | ~spl99), inference(resolution, [status(thm)], [p531, c277])).
% 121.12/16.54  cnf(sct51, plain, (~spl99), inference(avatar_contradiction_clause, [status(thm)], [p700])).
% 121.12/16.54  fof(sdef100, definition, (spl100 <=> (~lower_bounded_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl100])], [avatar_definition])).
% 121.12/16.54  cnf(p532, plain, (~lower_bounded_relstr(sk20) | ~spl100), inference(avatar_component_clause, [status(thm)], [sdef100])).
% 121.12/16.54  fof(sdef96, definition, (spl96 <=> (lower_bounded_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 121.12/16.54  cnf(p527, plain, (lower_bounded_relstr(sk20) | ~spl96), inference(avatar_component_clause, [status(thm)], [sdef96])).
% 121.12/16.54  cnf(p701, plain, ($false | ~spl96 | ~spl100), inference(resolution, [status(thm)], [p532, p527])).
% 121.12/16.54  cnf(sct52, plain, (~spl96 | ~spl100), inference(avatar_contradiction_clause, [status(thm)], [p701])).
% 121.12/16.54  fof(sdef101, definition, (spl101 <=> (~up_complete_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl101])], [avatar_definition])).
% 121.12/16.54  cnf(p533, plain, (~up_complete_relstr(sk20) | ~spl101), inference(avatar_component_clause, [status(thm)], [sdef101])).
% 121.12/16.54  fof(sdef93, definition, (spl93 <=> (up_complete_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 121.12/16.54  cnf(p522, plain, (up_complete_relstr(sk20) | ~spl93), inference(avatar_component_clause, [status(thm)], [sdef93])).
% 121.12/16.54  cnf(p702, plain, ($false | ~spl93 | ~spl101), inference(resolution, [status(thm)], [p533, p522])).
% 121.12/16.54  cnf(sct53, plain, (~spl93 | ~spl101), inference(avatar_contradiction_clause, [status(thm)], [p702])).
% 121.12/16.54  fof(sdef106, definition, (spl106 <=> (empty_carrier(sk26))), introduced(definition, [new_symbols(naming, [spl106])], [avatar_definition])).
% 121.12/16.54  cnf(p544, plain, (empty_carrier(sk26) | ~spl106), inference(avatar_component_clause, [status(thm)], [sdef106])).
% 121.12/16.54  fof(f91, axiom, ? [A] : ( rel_str(A) & ~ empty_carrier(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) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc2_yellow_0)).
% 121.12/16.54  fof(f91_nnf, plain, ? [A] : (((((((((((rel_str(A) & ~(empty_carrier(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))), inference(nnf_transformation, [status(thm)], [f91])).
% 121.12/16.54  fof(f91_sk, plain, ((((((((((rel_str(sk26) & ~(empty_carrier(sk26))) & reflexive_relstr(sk26)) & transitive_relstr(sk26)) & antisymmetric_relstr(sk26)) & with_suprema_relstr(sk26)) & with_infima_relstr(sk26)) & complete_relstr(sk26)) & lower_bounded_relstr(sk26)) & upper_bounded_relstr(sk26)) & bounded_relstr(sk26)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk26])], [f91_nnf])).
% 121.12/16.54  cnf(c296, plain, ~empty_carrier(sk26), inference(cnf_transformation, [status(esa)], [f91_sk])).
% 121.12/16.54  cnf(p705, plain, ($false | ~spl106), inference(resolution, [status(thm)], [p544, c296])).
% 121.12/16.54  cnf(sct54, plain, (~spl106), inference(avatar_contradiction_clause, [status(thm)], [p705])).
% 121.12/16.54  fof(sdef107, definition, (spl107 <=> (~reflexive_relstr(sk26))), introduced(definition, [new_symbols(naming, [spl107])], [avatar_definition])).
% 121.12/16.54  cnf(p545, plain, (~reflexive_relstr(sk26) | ~spl107), inference(avatar_component_clause, [status(thm)], [sdef107])).
% 121.12/16.54  cnf(c297, plain, reflexive_relstr(sk26), inference(cnf_transformation, [status(esa)], [f91_sk])).
% 121.12/16.54  cnf(p706, plain, ($false | ~spl107), inference(resolution, [status(thm)], [p545, c297])).
% 121.12/16.54  cnf(sct55, plain, (~spl107), inference(avatar_contradiction_clause, [status(thm)], [p706])).
% 121.12/16.54  fof(sdef108, definition, (spl108 <=> (~complete_relstr(sk26))), introduced(definition, [new_symbols(naming, [spl108])], [avatar_definition])).
% 121.12/16.54  cnf(p546, plain, (~complete_relstr(sk26) | ~spl108), inference(avatar_component_clause, [status(thm)], [sdef108])).
% 121.12/16.54  cnf(c302, plain, complete_relstr(sk26), inference(cnf_transformation, [status(esa)], [f91_sk])).
% 121.12/16.54  cnf(p707, plain, ($false | ~spl108), inference(resolution, [status(thm)], [p546, c302])).
% 121.12/16.54  cnf(sct56, plain, (~spl108), inference(avatar_contradiction_clause, [status(thm)], [p707])).
% 121.12/16.54  fof(sdef111, definition, (spl111 <=> (~upper_bounded_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl111])], [avatar_definition])).
% 121.12/16.54  cnf(p551, plain, (~upper_bounded_relstr(sk0) | ~spl111), inference(avatar_component_clause, [status(thm)], [sdef111])).
% 121.12/16.54  fof(sdef66, definition, (spl66 <=> (upper_bounded_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 121.12/16.54  cnf(p482, plain, (upper_bounded_relstr(sk0) | ~spl66), inference(avatar_component_clause, [status(thm)], [sdef66])).
% 121.12/16.54  cnf(p708, plain, ($false | ~spl66 | ~spl111), inference(resolution, [status(thm)], [p551, p482])).
% 121.12/16.54  cnf(sct57, plain, (~spl66 | ~spl111), inference(avatar_contradiction_clause, [status(thm)], [p708])).
% 121.12/16.54  fof(sdef112, definition, (spl112 <=> (with_suprema_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl112])], [avatar_definition])).
% 121.12/16.54  cnf(p552, plain, (with_suprema_relstr(sk0) | ~spl112), inference(avatar_component_clause, [status(thm)], [sdef112])).
% 121.12/16.54  fof(sdef42, definition, (spl42 <=> (~with_suprema_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 121.12/16.54  cnf(p452, plain, (~with_suprema_relstr(sk0) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 121.12/16.54  cnf(p709, plain, ($false | ~spl42 | ~spl112), inference(resolution, [status(thm)], [p552, p452])).
% 121.12/16.54  cnf(sct58, plain, (~spl42 | ~spl112), inference(avatar_contradiction_clause, [status(thm)], [p709])).
% 121.12/16.54  fof(sdef113, definition, (spl113 <=> (~upper_bounded_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl113])], [avatar_definition])).
% 121.12/16.54  cnf(p554, plain, (~upper_bounded_relstr(sk10) | ~spl113), inference(avatar_component_clause, [status(thm)], [sdef113])).
% 121.12/16.54  fof(sdef67, definition, (spl67 <=> (upper_bounded_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 121.12/16.54  cnf(p484, plain, (upper_bounded_relstr(sk10) | ~spl67), inference(avatar_component_clause, [status(thm)], [sdef67])).
% 121.12/16.54  cnf(p710, plain, ($false | ~spl67 | ~spl113), inference(resolution, [status(thm)], [p554, p484])).
% 121.12/16.54  cnf(sct59, plain, (~spl67 | ~spl113), inference(avatar_contradiction_clause, [status(thm)], [p710])).
% 121.12/16.54  fof(sdef114, definition, (spl114 <=> (with_suprema_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl114])], [avatar_definition])).
% 121.12/16.54  cnf(p555, plain, (with_suprema_relstr(sk10) | ~spl114), inference(avatar_component_clause, [status(thm)], [sdef114])).
% 121.12/16.54  fof(sdef48, definition, (spl48 <=> (~with_suprema_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 121.12/16.54  cnf(p459, plain, (~with_suprema_relstr(sk10) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 121.12/16.54  cnf(p732, plain, ($false | ~spl48 | ~spl114), inference(resolution, [status(thm)], [p555, p459])).
% 121.12/16.54  cnf(sct60, plain, (~spl48 | ~spl114), inference(avatar_contradiction_clause, [status(thm)], [p732])).
% 121.12/16.54  fof(sdef115, definition, (spl115 <=> (~upper_bounded_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl115])], [avatar_definition])).
% 121.12/16.54  cnf(p557, plain, (~upper_bounded_relstr(sk13) | ~spl115), inference(avatar_component_clause, [status(thm)], [sdef115])).
% 121.12/16.54  fof(sdef68, definition, (spl68 <=> (upper_bounded_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 121.12/16.54  cnf(p486, plain, (upper_bounded_relstr(sk13) | ~spl68), inference(avatar_component_clause, [status(thm)], [sdef68])).
% 121.12/16.54  cnf(p733, plain, ($false | ~spl68 | ~spl115), inference(resolution, [status(thm)], [p557, p486])).
% 121.12/16.54  cnf(sct61, plain, (~spl68 | ~spl115), inference(avatar_contradiction_clause, [status(thm)], [p733])).
% 121.12/16.54  fof(sdef116, definition, (spl116 <=> (with_suprema_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl116])], [avatar_definition])).
% 121.12/16.54  cnf(p558, plain, (with_suprema_relstr(sk13) | ~spl116), inference(avatar_component_clause, [status(thm)], [sdef116])).
% 121.12/16.54  fof(sdef54, definition, (spl54 <=> (~with_suprema_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 121.12/16.54  cnf(p466, plain, (~with_suprema_relstr(sk13) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 121.12/16.54  cnf(p734, plain, ($false | ~spl54 | ~spl116), inference(resolution, [status(thm)], [p558, p466])).
% 121.12/16.54  cnf(sct62, plain, (~spl54 | ~spl116), inference(avatar_contradiction_clause, [status(thm)], [p734])).
% 121.12/16.54  fof(sdef117, definition, (spl117 <=> (~strict_rel_str(sk34))), introduced(definition, [new_symbols(naming, [spl117])], [avatar_definition])).
% 121.12/16.54  cnf(p560, plain, (~strict_rel_str(sk34) | ~spl117), inference(avatar_component_clause, [status(thm)], [sdef117])).
% 121.12/16.54  fof(f99, axiom, ? [A] : ( rel_str(A) & ~ empty_carrier(A) & strict_rel_str(A) & transitive_relstr(A) & directed_relstr(A) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rc4_yellow_6)).
% 121.12/16.54  fof(f99_nnf, plain, ? [A] : (((((rel_str(A) & ~(empty_carrier(A))) & strict_rel_str(A)) & transitive_relstr(A)) & directed_relstr(A))), inference(nnf_transformation, [status(thm)], [f99])).
% 121.12/16.54  fof(f99_sk, plain, ((((rel_str(sk34) & ~(empty_carrier(sk34))) & strict_rel_str(sk34)) & transitive_relstr(sk34)) & directed_relstr(sk34)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk34])], [f99_nnf])).
% 121.12/16.54  cnf(c333, plain, strict_rel_str(sk34), inference(cnf_transformation, [status(esa)], [f99_sk])).
% 121.12/16.54  cnf(p735, plain, ($false | ~spl117), inference(resolution, [status(thm)], [p560, c333])).
% 121.12/16.54  cnf(sct63, plain, (~spl117), inference(avatar_contradiction_clause, [status(thm)], [p735])).
% 121.12/16.54  fof(sdef119, definition, (spl119 <=> (empty_carrier(sk34))), introduced(definition, [new_symbols(naming, [spl119])], [avatar_definition])).
% 121.12/16.54  cnf(p563, plain, (empty_carrier(sk34) | ~spl119), inference(avatar_component_clause, [status(thm)], [sdef119])).
% 121.12/16.54  cnf(c332, plain, ~empty_carrier(sk34), inference(cnf_transformation, [status(esa)], [f99_sk])).
% 121.12/16.54  cnf(p744, plain, ($false | ~spl119), inference(resolution, [status(thm)], [p563, c332])).
% 121.12/16.54  cnf(sct64, plain, (~spl119), inference(avatar_contradiction_clause, [status(thm)], [p744])).
% 121.12/16.54  fof(sdef124, definition, (spl124 <=> (~join_complete_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl124])], [avatar_definition])).
% 121.12/16.54  cnf(p570, plain, (~join_complete_relstr(sk34) | ~spl124), inference(avatar_component_clause, [status(thm)], [sdef124])).
% 121.12/16.54  fof(sdef123, definition, (spl123 <=> (join_complete_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl123])], [avatar_definition])).
% 121.12/16.54  cnf(p568, plain, (join_complete_relstr(sk34) | ~spl123), inference(avatar_component_clause, [status(thm)], [sdef123])).
% 121.12/16.54  cnf(p747, plain, ($false | ~spl123 | ~spl124), inference(resolution, [status(thm)], [p570, p568])).
% 121.12/16.54  cnf(sct65, plain, (~spl123 | ~spl124), inference(avatar_contradiction_clause, [status(thm)], [p747])).
% 121.12/16.54  fof(sdef126, definition, (spl126 <=> (~transitive_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl126])], [avatar_definition])).
% 121.12/16.54  cnf(p573, plain, (~transitive_relstr(sk34) | ~spl126), inference(avatar_component_clause, [status(thm)], [sdef126])).
% 121.12/16.54  cnf(c334, plain, transitive_relstr(sk34), inference(cnf_transformation, [status(esa)], [f99_sk])).
% 121.12/16.54  cnf(p748, plain, ($false | ~spl126), inference(resolution, [status(thm)], [p573, c334])).
% 121.12/16.54  cnf(sct66, plain, (~spl126), inference(avatar_contradiction_clause, [status(thm)], [p748])).
% 121.12/16.54  fof(sdef129, definition, (spl129 <=> (~lower_bounded_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl129])], [avatar_definition])).
% 121.12/16.54  cnf(p576, plain, (~lower_bounded_relstr(sk34) | ~spl129), inference(avatar_component_clause, [status(thm)], [sdef129])).
% 121.12/16.54  fof(sdef125, definition, (spl125 <=> (lower_bounded_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl125])], [avatar_definition])).
% 121.12/16.54  cnf(p571, plain, (lower_bounded_relstr(sk34) | ~spl125), inference(avatar_component_clause, [status(thm)], [sdef125])).
% 121.12/16.54  cnf(p749, plain, ($false | ~spl125 | ~spl129), inference(resolution, [status(thm)], [p576, p571])).
% 121.12/16.54  cnf(sct67, plain, (~spl125 | ~spl129), inference(avatar_contradiction_clause, [status(thm)], [p749])).
% 121.12/16.54  fof(sdef130, definition, (spl130 <=> (~up_complete_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl130])], [avatar_definition])).
% 121.12/16.54  cnf(p577, plain, (~up_complete_relstr(sk34) | ~spl130), inference(avatar_component_clause, [status(thm)], [sdef130])).
% 121.12/16.54  fof(sdef122, definition, (spl122 <=> (up_complete_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl122])], [avatar_definition])).
% 121.12/16.54  cnf(p566, plain, (up_complete_relstr(sk34) | ~spl122), inference(avatar_component_clause, [status(thm)], [sdef122])).
% 121.12/16.54  cnf(p752, plain, ($false | ~spl122 | ~spl130), inference(resolution, [status(thm)], [p577, p566])).
% 121.12/16.54  cnf(sct68, plain, (~spl122 | ~spl130), inference(avatar_contradiction_clause, [status(thm)], [p752])).
% 121.12/16.54  fof(sdef132, definition, (spl132 <=> (complete_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl132])], [avatar_definition])).
% 121.12/16.54  cnf(p580, plain, (complete_relstr(sk34) | ~spl132), inference(avatar_component_clause, [status(thm)], [sdef132])).
% 121.12/16.54  fof(sdef121, definition, (spl121 <=> (~complete_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl121])], [avatar_definition])).
% 121.12/16.54  cnf(p565, plain, (~complete_relstr(sk34) | ~spl121), inference(avatar_component_clause, [status(thm)], [sdef121])).
% 121.12/16.54  cnf(p753, plain, ($false | ~spl121 | ~spl132), inference(resolution, [status(thm)], [p580, p565])).
% 121.12/16.54  cnf(sct69, plain, (~spl121 | ~spl132), inference(avatar_contradiction_clause, [status(thm)], [p753])).
% 121.12/16.54  fof(sdef135, definition, (spl135 <=> (~upper_bounded_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl135])], [avatar_definition])).
% 121.12/16.54  cnf(p587, plain, (~upper_bounded_relstr(sk34) | ~spl135), inference(avatar_component_clause, [status(thm)], [sdef135])).
% 121.12/16.54  fof(sdef133, definition, (spl133 <=> (upper_bounded_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl133])], [avatar_definition])).
% 121.12/16.54  cnf(p582, plain, (upper_bounded_relstr(sk34) | ~spl133), inference(avatar_component_clause, [status(thm)], [sdef133])).
% 121.12/16.54  cnf(p756, plain, ($false | ~spl133 | ~spl135), inference(resolution, [status(thm)], [p587, p582])).
% 121.12/16.54  cnf(sct70, plain, (~spl133 | ~spl135), inference(avatar_contradiction_clause, [status(thm)], [p756])).
% 121.12/16.54  fof(sdef136, definition, (spl136 <=> (with_suprema_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl136])], [avatar_definition])).
% 121.12/16.54  cnf(p588, plain, (with_suprema_relstr(sk34) | ~spl136), inference(avatar_component_clause, [status(thm)], [sdef136])).
% 121.12/16.54  fof(sdef128, definition, (spl128 <=> (~with_suprema_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl128])], [avatar_definition])).
% 121.12/16.54  cnf(p575, plain, (~with_suprema_relstr(sk34) | ~spl128), inference(avatar_component_clause, [status(thm)], [sdef128])).
% 121.12/16.54  cnf(p759, plain, ($false | ~spl128 | ~spl136), inference(resolution, [status(thm)], [p588, p575])).
% 121.12/16.54  cnf(sct71, plain, (~spl128 | ~spl136), inference(avatar_contradiction_clause, [status(thm)], [p759])).
% 121.12/16.54  fof(sdef137, definition, (spl137 <=> (~empty_carrier(sk0))), introduced(definition, [new_symbols(naming, [spl137])], [avatar_definition])).
% 121.12/16.54  cnf(p592, plain, (~empty_carrier(sk0) | ~spl137), inference(avatar_component_clause, [status(thm)], [sdef137])).
% 121.12/16.54  fof(sdef6, definition, (spl6 <=> (empty_carrier(sk0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 121.12/16.54  cnf(p401, plain, (empty_carrier(sk0) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 121.12/16.54  cnf(p764, plain, ($false | ~spl6 | ~spl137), inference(resolution, [status(thm)], [p592, p401])).
% 121.12/16.54  cnf(sct72, plain, (~spl6 | ~spl137), inference(avatar_contradiction_clause, [status(thm)], [p764])).
% 121.12/16.54  fof(sdef141, definition, (spl141 <=> (~with_infima_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl141])], [avatar_definition])).
% 121.12/16.54  cnf(p626, plain, (~with_infima_relstr(sk0) | ~spl141), inference(avatar_component_clause, [status(thm)], [sdef141])).
% 121.12/16.54  fof(sdef45, definition, (spl45 <=> (with_infima_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 121.12/16.54  cnf(p455, plain, (with_infima_relstr(sk0) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 121.12/16.54  cnf(p765, plain, ($false | ~spl45 | ~spl141), inference(resolution, [status(thm)], [p626, p455])).
% 121.12/16.54  cnf(sct73, plain, (~spl45 | ~spl141), inference(avatar_contradiction_clause, [status(thm)], [p765])).
% 121.12/16.54  fof(sdef143, definition, (spl143 <=> (transitive_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl143])], [avatar_definition])).
% 121.12/16.54  cnf(p643, plain, (transitive_relstr(sk0) | ~spl143), inference(avatar_component_clause, [status(thm)], [sdef143])).
% 121.12/16.54  fof(sdef40, definition, (spl40 <=> (~transitive_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 121.12/16.54  cnf(p450, plain, (~transitive_relstr(sk0) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 121.12/16.54  cnf(p768, plain, ($false | ~spl40 | ~spl143), inference(resolution, [status(thm)], [p643, p450])).
% 121.12/16.54  cnf(sct74, plain, (~spl40 | ~spl143), inference(avatar_contradiction_clause, [status(thm)], [p768])).
% 121.12/16.54  fof(sdef144, definition, (spl144 <=> (antisymmetric_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl144])], [avatar_definition])).
% 121.12/16.54  cnf(p647, plain, (antisymmetric_relstr(sk0) | ~spl144), inference(avatar_component_clause, [status(thm)], [sdef144])).
% 121.12/16.54  fof(sdef41, definition, (spl41 <=> (~antisymmetric_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 121.12/16.54  cnf(p451, plain, (~antisymmetric_relstr(sk0) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 121.12/16.54  cnf(p769, plain, ($false | ~spl41 | ~spl144), inference(resolution, [status(thm)], [p647, p451])).
% 121.12/16.54  cnf(sct75, plain, (~spl41 | ~spl144), inference(avatar_contradiction_clause, [status(thm)], [p769])).
% 121.12/16.54  fof(sdef146, definition, (spl146 <=> (antisymmetric_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl146])], [avatar_definition])).
% 121.12/16.54  cnf(p650, plain, (antisymmetric_relstr(sk34) | ~spl146), inference(avatar_component_clause, [status(thm)], [sdef146])).
% 121.12/16.54  fof(sdef127, definition, (spl127 <=> (~antisymmetric_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl127])], [avatar_definition])).
% 121.12/16.54  cnf(p574, plain, (~antisymmetric_relstr(sk34) | ~spl127), inference(avatar_component_clause, [status(thm)], [sdef127])).
% 121.12/16.54  cnf(p772, plain, ($false | ~spl127 | ~spl146), inference(resolution, [status(thm)], [p650, p574])).
% 121.12/16.54  cnf(sct76, plain, (~spl127 | ~spl146), inference(avatar_contradiction_clause, [status(thm)], [p772])).
% 121.12/16.54  fof(sdef150, definition, (spl150 <=> (~bounded_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl150])], [avatar_definition])).
% 121.12/16.54  cnf(p679, plain, (~bounded_relstr(sk0) | ~spl150), inference(avatar_component_clause, [status(thm)], [sdef150])).
% 121.12/16.54  fof(sdef84, definition, (spl84 <=> (bounded_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 121.12/16.54  cnf(p508, plain, (bounded_relstr(sk0) | ~spl84), inference(avatar_component_clause, [status(thm)], [sdef84])).
% 121.12/16.54  cnf(p773, plain, ($false | ~spl84 | ~spl150), inference(resolution, [status(thm)], [p679, p508])).
% 121.12/16.54  cnf(sct77, plain, (~spl84 | ~spl150), inference(avatar_contradiction_clause, [status(thm)], [p773])).
% 121.12/16.54  fof(sdef151, definition, (spl151 <=> (~bounded_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl151])], [avatar_definition])).
% 121.12/16.54  cnf(p681, plain, (~bounded_relstr(sk10) | ~spl151), inference(avatar_component_clause, [status(thm)], [sdef151])).
% 121.12/16.54  fof(sdef85, definition, (spl85 <=> (bounded_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 121.12/16.54  cnf(p510, plain, (bounded_relstr(sk10) | ~spl85), inference(avatar_component_clause, [status(thm)], [sdef85])).
% 121.12/16.54  cnf(p774, plain, ($false | ~spl85 | ~spl151), inference(resolution, [status(thm)], [p681, p510])).
% 121.12/16.54  cnf(sct78, plain, (~spl85 | ~spl151), inference(avatar_contradiction_clause, [status(thm)], [p774])).
% 121.12/16.54  fof(sdef152, definition, (spl152 <=> (~bounded_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl152])], [avatar_definition])).
% 121.12/16.54  cnf(p683, plain, (~bounded_relstr(sk13) | ~spl152), inference(avatar_component_clause, [status(thm)], [sdef152])).
% 121.12/16.54  fof(sdef86, definition, (spl86 <=> (bounded_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 121.12/16.54  cnf(p512, plain, (bounded_relstr(sk13) | ~spl86), inference(avatar_component_clause, [status(thm)], [sdef86])).
% 121.12/16.54  cnf(p775, plain, ($false | ~spl86 | ~spl152), inference(resolution, [status(thm)], [p683, p512])).
% 121.12/16.54  cnf(sct79, plain, (~spl86 | ~spl152), inference(avatar_contradiction_clause, [status(thm)], [p775])).
% 121.12/16.54  fof(sdef153, definition, (spl153 <=> (~bounded_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl153])], [avatar_definition])).
% 121.12/16.54  cnf(p685, plain, (~bounded_relstr(sk19) | ~spl153), inference(avatar_component_clause, [status(thm)], [sdef153])).
% 121.12/16.54  fof(sdef87, definition, (spl87 <=> (bounded_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 121.12/16.54  cnf(p514, plain, (bounded_relstr(sk19) | ~spl87), inference(avatar_component_clause, [status(thm)], [sdef87])).
% 121.12/16.54  cnf(p776, plain, ($false | ~spl87 | ~spl153), inference(resolution, [status(thm)], [p685, p514])).
% 121.12/16.54  cnf(sct80, plain, (~spl87 | ~spl153), inference(avatar_contradiction_clause, [status(thm)], [p776])).
% 121.12/16.54  fof(sdef154, definition, (spl154 <=> (~bounded_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl154])], [avatar_definition])).
% 121.12/16.54  cnf(p687, plain, (~bounded_relstr(sk20) | ~spl154), inference(avatar_component_clause, [status(thm)], [sdef154])).
% 121.12/16.54  fof(sdef103, definition, (spl103 <=> (bounded_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl103])], [avatar_definition])).
% 121.12/16.54  cnf(p536, plain, (bounded_relstr(sk20) | ~spl103), inference(avatar_component_clause, [status(thm)], [sdef103])).
% 121.12/16.54  cnf(p777, plain, ($false | ~spl103 | ~spl154), inference(resolution, [status(thm)], [p687, p536])).
% 121.12/16.54  cnf(sct81, plain, (~spl103 | ~spl154), inference(avatar_contradiction_clause, [status(thm)], [p777])).
% 121.12/16.54  fof(sdef155, definition, (spl155 <=> (~bounded_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl155])], [avatar_definition])).
% 121.12/16.54  cnf(p689, plain, (~bounded_relstr(sk34) | ~spl155), inference(avatar_component_clause, [status(thm)], [sdef155])).
% 121.12/16.54  fof(sdef134, definition, (spl134 <=> (bounded_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl134])], [avatar_definition])).
% 121.12/16.54  cnf(p584, plain, (bounded_relstr(sk34) | ~spl134), inference(avatar_component_clause, [status(thm)], [sdef134])).
% 121.12/16.54  cnf(p778, plain, ($false | ~spl134 | ~spl155), inference(resolution, [status(thm)], [p689, p584])).
% 121.12/16.54  cnf(sct82, plain, (~spl134 | ~spl155), inference(avatar_contradiction_clause, [status(thm)], [p778])).
% 121.12/16.54  fof(sdef158, definition, (spl158 <=> (empty_carrier(sk11))), introduced(definition, [new_symbols(naming, [spl158])], [avatar_definition])).
% 121.12/16.54  cnf(p714, plain, (empty_carrier(sk11) | ~spl158), inference(avatar_component_clause, [status(thm)], [sdef158])).
% 121.12/16.54  cnf(c213, plain, ~empty_carrier(sk11), inference(cnf_transformation, [status(esa)], [f76_sk])).
% 121.12/16.54  cnf(p779, plain, ($false | ~spl158), inference(resolution, [status(thm)], [p714, c213])).
% 121.12/16.54  cnf(sct83, plain, (~spl158), inference(avatar_contradiction_clause, [status(thm)], [p779])).
% 121.12/16.54  fof(sdef159, definition, (spl159 <=> (~reflexive_relstr(sk11))), introduced(definition, [new_symbols(naming, [spl159])], [avatar_definition])).
% 121.12/16.54  cnf(p715, plain, (~reflexive_relstr(sk11) | ~spl159), inference(avatar_component_clause, [status(thm)], [sdef159])).
% 121.12/16.54  cnf(c215, plain, reflexive_relstr(sk11), inference(cnf_transformation, [status(esa)], [f76_sk])).
% 121.12/16.54  cnf(p780, plain, ($false | ~spl159), inference(resolution, [status(thm)], [p715, c215])).
% 121.12/16.54  cnf(sct84, plain, (~spl159), inference(avatar_contradiction_clause, [status(thm)], [p780])).
% 121.12/16.54  fof(sdef164, definition, (spl164 <=> (~trivial_carrier(sk19))), introduced(definition, [new_symbols(naming, [spl164])], [avatar_definition])).
% 121.12/16.54  cnf(p722, plain, (~trivial_carrier(sk19) | ~spl164), inference(avatar_component_clause, [status(thm)], [sdef164])).
% 121.12/16.54  cnf(c270, plain, trivial_carrier(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p781, plain, ($false | ~spl164), inference(resolution, [status(thm)], [p722, c270])).
% 121.12/16.54  cnf(sct85, plain, (~spl164), inference(avatar_contradiction_clause, [status(thm)], [p781])).
% 121.12/16.54  fof(sdef171, definition, (spl171 <=> (~upper_bounded_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl171])], [avatar_definition])).
% 121.12/16.54  cnf(p740, plain, (~upper_bounded_relstr(sk19) | ~spl171), inference(avatar_component_clause, [status(thm)], [sdef171])).
% 121.12/16.54  fof(sdef83, definition, (spl83 <=> (upper_bounded_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 121.12/16.54  cnf(p506, plain, (upper_bounded_relstr(sk19) | ~spl83), inference(avatar_component_clause, [status(thm)], [sdef83])).
% 121.12/16.54  cnf(p782, plain, ($false | ~spl83 | ~spl171), inference(resolution, [status(thm)], [p740, p506])).
% 121.12/16.54  cnf(sct86, plain, (~spl83 | ~spl171), inference(avatar_contradiction_clause, [status(thm)], [p782])).
% 121.12/16.54  fof(sdef172, definition, (spl172 <=> (~upper_bounded_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl172])], [avatar_definition])).
% 121.12/16.54  cnf(p742, plain, (~upper_bounded_relstr(sk20) | ~spl172), inference(avatar_component_clause, [status(thm)], [sdef172])).
% 121.12/16.54  fof(sdef102, definition, (spl102 <=> (upper_bounded_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl102])], [avatar_definition])).
% 121.12/16.54  cnf(p534, plain, (upper_bounded_relstr(sk20) | ~spl102), inference(avatar_component_clause, [status(thm)], [sdef102])).
% 121.12/16.54  cnf(p789, plain, ($false | ~spl102 | ~spl172), inference(resolution, [status(thm)], [p742, p534])).
% 121.12/16.54  cnf(sct87, plain, (~spl102 | ~spl172), inference(avatar_contradiction_clause, [status(thm)], [p789])).
% 121.12/16.54  fof(sdef180, definition, (spl180 <=> (empty_carrier(sk43))), introduced(definition, [new_symbols(naming, [spl180])], [avatar_definition])).
% 121.12/16.54  cnf(p793, plain, (empty_carrier(sk43) | ~spl180), inference(avatar_component_clause, [status(thm)], [sdef180])).
% 121.12/16.54  cnf(c376, plain, ~empty_carrier(sk43), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(p795, plain, ($false | ~spl180), inference(resolution, [status(thm)], [p793, c376])).
% 121.12/16.54  cnf(sct88, plain, (~spl180), inference(avatar_contradiction_clause, [status(thm)], [p795])).
% 121.12/16.54  fof(sdef192, definition, (spl192 <=> (empty(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl192])], [avatar_definition])).
% 121.12/16.54  cnf(p835, plain, (empty(cast_as_carrier_subset(sk43)) | ~spl192), inference(avatar_component_clause, [status(thm)], [sdef192])).
% 121.12/16.54  fof(sdef183, definition, (spl183 <=> (~empty(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl183])], [avatar_definition])).
% 121.12/16.54  cnf(p820, plain, (~empty(cast_as_carrier_subset(sk43)) | ~spl183), inference(avatar_component_clause, [status(thm)], [sdef183])).
% 121.12/16.54  cnf(p849, plain, ($false | ~spl183 | ~spl192), inference(resolution, [status(thm)], [p835, p820])).
% 121.12/16.54  cnf(sct89, plain, (~spl183 | ~spl192), inference(avatar_contradiction_clause, [status(thm)], [p849])).
% 121.12/16.54  fof(sdef188, definition, (spl188 <=> (~nowhere_dense(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl188])], [avatar_definition])).
% 121.12/16.54  cnf(p829, plain, (~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | ~spl188), inference(avatar_component_clause, [status(thm)], [sdef188])).
% 121.12/16.54  fof(sdef187, definition, (spl187 <=> (nowhere_dense(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl187])], [avatar_definition])).
% 121.12/16.54  cnf(p827, plain, (nowhere_dense(cast_as_carrier_subset(sk43),sk43) | ~spl187), inference(avatar_component_clause, [status(thm)], [sdef187])).
% 121.12/16.54  cnf(p862, plain, ($false | ~spl187 | ~spl188), inference(resolution, [status(thm)], [p829, p827])).
% 121.12/16.54  cnf(sct90, plain, (~spl187 | ~spl188), inference(avatar_contradiction_clause, [status(thm)], [p862])).
% 121.12/16.54  fof(sdef189, definition, (spl189 <=> (~closed_subset(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl189])], [avatar_definition])).
% 121.12/16.54  cnf(p831, plain, (~closed_subset(cast_as_carrier_subset(sk43),sk43) | ~spl189), inference(avatar_component_clause, [status(thm)], [sdef189])).
% 121.12/16.54  fof(sdef185, definition, (spl185 <=> (closed_subset(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl185])], [avatar_definition])).
% 121.12/16.54  cnf(p823, plain, (closed_subset(cast_as_carrier_subset(sk43),sk43) | ~spl185), inference(avatar_component_clause, [status(thm)], [sdef185])).
% 121.12/16.54  cnf(p863, plain, ($false | ~spl185 | ~spl189), inference(resolution, [status(thm)], [p831, p823])).
% 121.12/16.54  cnf(sct91, plain, (~spl185 | ~spl189), inference(avatar_contradiction_clause, [status(thm)], [p863])).
% 121.12/16.54  fof(sdef190, definition, (spl190 <=> (~boundary_set(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl190])], [avatar_definition])).
% 121.12/16.54  cnf(p832, plain, (~boundary_set(cast_as_carrier_subset(sk43),sk43) | ~spl190), inference(avatar_component_clause, [status(thm)], [sdef190])).
% 121.12/16.54  fof(sdef186, definition, (spl186 <=> (boundary_set(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl186])], [avatar_definition])).
% 121.12/16.54  cnf(p825, plain, (boundary_set(cast_as_carrier_subset(sk43),sk43) | ~spl186), inference(avatar_component_clause, [status(thm)], [sdef186])).
% 121.12/16.54  cnf(p864, plain, ($false | ~spl186 | ~spl190), inference(resolution, [status(thm)], [p832, p825])).
% 121.12/16.54  cnf(sct92, plain, (~spl186 | ~spl190), inference(avatar_contradiction_clause, [status(thm)], [p864])).
% 121.12/16.54  fof(sdef191, definition, (spl191 <=> (~open_subset(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl191])], [avatar_definition])).
% 121.12/16.54  cnf(p834, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~spl191), inference(avatar_component_clause, [status(thm)], [sdef191])).
% 121.12/16.54  fof(sdef184, definition, (spl184 <=> (open_subset(cast_as_carrier_subset(sk43),sk43))), introduced(definition, [new_symbols(naming, [spl184])], [avatar_definition])).
% 121.12/16.54  cnf(p821, plain, (open_subset(cast_as_carrier_subset(sk43),sk43) | ~spl184), inference(avatar_component_clause, [status(thm)], [sdef184])).
% 121.12/16.54  cnf(p867, plain, ($false | ~spl184 | ~spl191), inference(resolution, [status(thm)], [p834, p821])).
% 121.12/16.54  cnf(sct93, plain, (~spl184 | ~spl191), inference(avatar_contradiction_clause, [status(thm)], [p867])).
% 121.12/16.54  fof(sdef209, definition, (spl209 <=> (empty(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl209])], [avatar_definition])).
% 121.12/16.54  cnf(p889, plain, (empty(sk3(sk43,sk44)) | ~spl209), inference(avatar_component_clause, [status(thm)], [sdef209])).
% 121.12/16.54  fof(sdef200, definition, (spl200 <=> (~empty(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl200])], [avatar_definition])).
% 121.12/16.54  cnf(p874, plain, (~empty(sk3(sk43,sk44)) | ~spl200), inference(avatar_component_clause, [status(thm)], [sdef200])).
% 121.12/16.54  cnf(p903, plain, ($false | ~spl200 | ~spl209), inference(resolution, [status(thm)], [p889, p874])).
% 121.12/16.54  cnf(sct94, plain, (~spl200 | ~spl209), inference(avatar_contradiction_clause, [status(thm)], [p903])).
% 121.12/16.54  fof(sdef205, definition, (spl205 <=> (~nowhere_dense(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl205])], [avatar_definition])).
% 121.12/16.54  cnf(p883, plain, (~nowhere_dense(sk3(sk43,sk44),sk43) | ~spl205), inference(avatar_component_clause, [status(thm)], [sdef205])).
% 121.12/16.54  fof(sdef204, definition, (spl204 <=> (nowhere_dense(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl204])], [avatar_definition])).
% 121.12/16.54  cnf(p881, plain, (nowhere_dense(sk3(sk43,sk44),sk43) | ~spl204), inference(avatar_component_clause, [status(thm)], [sdef204])).
% 121.12/16.54  cnf(p942, plain, ($false | ~spl204 | ~spl205), inference(resolution, [status(thm)], [p883, p881])).
% 121.12/16.54  cnf(sct95, plain, (~spl204 | ~spl205), inference(avatar_contradiction_clause, [status(thm)], [p942])).
% 121.12/16.54  fof(sdef206, definition, (spl206 <=> (~closed_subset(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl206])], [avatar_definition])).
% 121.12/16.54  cnf(p885, plain, (~closed_subset(sk3(sk43,sk44),sk43) | ~spl206), inference(avatar_component_clause, [status(thm)], [sdef206])).
% 121.12/16.54  fof(sdef202, definition, (spl202 <=> (closed_subset(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl202])], [avatar_definition])).
% 121.12/16.54  cnf(p877, plain, (closed_subset(sk3(sk43,sk44),sk43) | ~spl202), inference(avatar_component_clause, [status(thm)], [sdef202])).
% 121.12/16.54  cnf(p943, plain, ($false | ~spl202 | ~spl206), inference(resolution, [status(thm)], [p885, p877])).
% 121.12/16.54  cnf(sct96, plain, (~spl202 | ~spl206), inference(avatar_contradiction_clause, [status(thm)], [p943])).
% 121.12/16.54  fof(sdef207, definition, (spl207 <=> (~boundary_set(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl207])], [avatar_definition])).
% 121.12/16.54  cnf(p886, plain, (~boundary_set(sk3(sk43,sk44),sk43) | ~spl207), inference(avatar_component_clause, [status(thm)], [sdef207])).
% 121.12/16.54  fof(sdef203, definition, (spl203 <=> (boundary_set(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl203])], [avatar_definition])).
% 121.12/16.54  cnf(p879, plain, (boundary_set(sk3(sk43,sk44),sk43) | ~spl203), inference(avatar_component_clause, [status(thm)], [sdef203])).
% 121.12/16.54  cnf(p944, plain, ($false | ~spl203 | ~spl207), inference(resolution, [status(thm)], [p886, p879])).
% 121.12/16.54  cnf(sct97, plain, (~spl203 | ~spl207), inference(avatar_contradiction_clause, [status(thm)], [p944])).
% 121.12/16.54  fof(sdef208, definition, (spl208 <=> (~open_subset(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl208])], [avatar_definition])).
% 121.12/16.54  cnf(p888, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~spl208), inference(avatar_component_clause, [status(thm)], [sdef208])).
% 121.12/16.54  fof(sdef201, definition, (spl201 <=> (open_subset(sk3(sk43,sk44),sk43))), introduced(definition, [new_symbols(naming, [spl201])], [avatar_definition])).
% 121.12/16.54  cnf(p875, plain, (open_subset(sk3(sk43,sk44),sk43) | ~spl201), inference(avatar_component_clause, [status(thm)], [sdef201])).
% 121.12/16.54  cnf(p964, plain, ($false | ~spl201 | ~spl208), inference(resolution, [status(thm)], [p888, p875])).
% 121.12/16.54  cnf(sct98, plain, (~spl201 | ~spl208), inference(avatar_contradiction_clause, [status(thm)], [p964])).
% 121.12/16.54  fof(sdef224, definition, (spl224 <=> (empty(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl224])], [avatar_definition])).
% 121.12/16.54  cnf(p921, plain, (empty(sk5(powerset(the_carrier(sk43)))) | ~spl224), inference(avatar_component_clause, [status(thm)], [sdef224])).
% 121.12/16.54  fof(sdef215, definition, (spl215 <=> (~empty(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl215])], [avatar_definition])).
% 121.12/16.54  cnf(p906, plain, (~empty(sk5(powerset(the_carrier(sk43)))) | ~spl215), inference(avatar_component_clause, [status(thm)], [sdef215])).
% 121.12/16.54  cnf(p967, plain, ($false | ~spl215 | ~spl224), inference(resolution, [status(thm)], [p921, p906])).
% 121.12/16.54  cnf(sct99, plain, (~spl215 | ~spl224), inference(avatar_contradiction_clause, [status(thm)], [p967])).
% 121.12/16.54  fof(sdef220, definition, (spl220 <=> (~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl220])], [avatar_definition])).
% 121.12/16.54  cnf(p915, plain, (~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | ~spl220), inference(avatar_component_clause, [status(thm)], [sdef220])).
% 121.12/16.54  fof(sdef219, definition, (spl219 <=> (nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl219])], [avatar_definition])).
% 121.12/16.54  cnf(p913, plain, (nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | ~spl219), inference(avatar_component_clause, [status(thm)], [sdef219])).
% 121.12/16.54  cnf(p1012, plain, ($false | ~spl219 | ~spl220), inference(resolution, [status(thm)], [p915, p913])).
% 121.12/16.54  cnf(sct100, plain, (~spl219 | ~spl220), inference(avatar_contradiction_clause, [status(thm)], [p1012])).
% 121.12/16.54  fof(sdef221, definition, (spl221 <=> (~closed_subset(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl221])], [avatar_definition])).
% 121.12/16.54  cnf(p917, plain, (~closed_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl221), inference(avatar_component_clause, [status(thm)], [sdef221])).
% 121.12/16.54  fof(sdef217, definition, (spl217 <=> (closed_subset(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl217])], [avatar_definition])).
% 121.12/16.54  cnf(p909, plain, (closed_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl217), inference(avatar_component_clause, [status(thm)], [sdef217])).
% 121.12/16.54  cnf(p1013, plain, ($false | ~spl217 | ~spl221), inference(resolution, [status(thm)], [p917, p909])).
% 121.12/16.54  cnf(sct101, plain, (~spl217 | ~spl221), inference(avatar_contradiction_clause, [status(thm)], [p1013])).
% 121.12/16.54  fof(sdef222, definition, (spl222 <=> (~boundary_set(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl222])], [avatar_definition])).
% 121.12/16.54  cnf(p918, plain, (~boundary_set(sk5(powerset(the_carrier(sk43))),sk43) | ~spl222), inference(avatar_component_clause, [status(thm)], [sdef222])).
% 121.12/16.54  fof(sdef218, definition, (spl218 <=> (boundary_set(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl218])], [avatar_definition])).
% 121.12/16.54  cnf(p911, plain, (boundary_set(sk5(powerset(the_carrier(sk43))),sk43) | ~spl218), inference(avatar_component_clause, [status(thm)], [sdef218])).
% 121.12/16.54  cnf(p1014, plain, ($false | ~spl218 | ~spl222), inference(resolution, [status(thm)], [p918, p911])).
% 121.12/16.54  cnf(sct102, plain, (~spl218 | ~spl222), inference(avatar_contradiction_clause, [status(thm)], [p1014])).
% 121.12/16.54  fof(sdef223, definition, (spl223 <=> (~open_subset(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl223])], [avatar_definition])).
% 121.12/16.54  cnf(p920, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl223), inference(avatar_component_clause, [status(thm)], [sdef223])).
% 121.12/16.54  fof(sdef216, definition, (spl216 <=> (open_subset(sk5(powerset(the_carrier(sk43))),sk43))), introduced(definition, [new_symbols(naming, [spl216])], [avatar_definition])).
% 121.12/16.54  cnf(p907, plain, (open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl216), inference(avatar_component_clause, [status(thm)], [sdef216])).
% 121.12/16.54  cnf(p1015, plain, ($false | ~spl216 | ~spl223), inference(resolution, [status(thm)], [p920, p907])).
% 121.12/16.54  cnf(sct103, plain, (~spl216 | ~spl223), inference(avatar_contradiction_clause, [status(thm)], [p1015])).
% 121.12/16.54  cnf(c380, plain, in(sk45,neighborhood_system(sk43,sk44)) | ~in(sk45,neighborhood_system(sk43,sk44)), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c380, sdef0, sdef1])).
% 121.12/16.54  cnf(c381, plain, in(sk45,neighborhood_system(sk43,sk44)) | point_neighbourhood(sk45,sk43,sk44), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(ssp1, plain, (spl0 | spl2), inference(avatar_split_clause, [status(thm)], [c381, sdef0, sdef2])).
% 121.12/16.54  cnf(c382, plain, ~point_neighbourhood(sk45,sk43,sk44) | ~in(sk45,neighborhood_system(sk43,sk44)), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(ssp2, plain, (spl1 | spl3), inference(avatar_split_clause, [status(thm)], [c382, sdef1, sdef3])).
% 121.12/16.54  cnf(c383, plain, ~point_neighbourhood(sk45,sk43,sk44) | point_neighbourhood(sk45,sk43,sk44), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(ssp3, plain, (spl2 | spl3), inference(avatar_split_clause, [status(thm)], [c383, sdef2, sdef3])).
% 121.12/16.54  fof(f43, axiom, ? [A] : rel_str(A), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', existence_l1_orders_2)).
% 121.12/16.54  fof(f43_nnf, plain, ? [A] : (rel_str(A)), inference(nnf_transformation, [status(thm)], [f43])).
% 121.12/16.54  fof(f43_sk, plain, rel_str(sk0), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0])], [f43_nnf])).
% 121.12/16.54  cnf(c90, plain, rel_str(sk0), inference(cnf_transformation, [status(esa)], [f43_sk])).
% 121.12/16.54  fof(f0, axiom, ! [A] : ( rel_str(A) => ( strict_rel_str(A) => A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', abstractness_v1_orders_2)).
% 121.12/16.54  fof(f0_nnf, plain, ! [A] : ((~(rel_str(A)) | (~(strict_rel_str(A)) | A = rel_str_of(the_carrier(A),the_InternalRel(A))))), inference(nnf_transformation, [status(thm)], [f0])).
% 121.12/16.54  fof(f0_sk, plain, ! [A] : ((~(rel_str(A)) | (~(strict_rel_str(A)) | A = rel_str_of(the_carrier(A),the_InternalRel(A))))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 121.12/16.54  cnf(c0, plain, ~rel_str(X0) | ~strict_rel_str(X0) | X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0)), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 121.12/16.54  cnf(p397, plain, ~strict_rel_str(sk0) | sk0 = rel_str_of(the_carrier(sk0),the_InternalRel(sk0)), inference(resolution, [status(thm)], [c90, c0])).
% 121.12/16.54  fof(sdef4, definition, (spl4 <=> (~strict_rel_str(sk0))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 121.12/16.54  fof(sdef5, definition, (spl5 <=> (sk0 = rel_str_of(the_carrier(sk0),the_InternalRel(sk0)))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 121.12/16.54  cnf(ssp4, plain, (spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p397, sdef4, sdef5])).
% 121.12/16.54  fof(f2, axiom, ! [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) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc10_waybel_0)).
% 121.12/16.54  fof(f2_nnf, plain, ! [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))))), inference(nnf_transformation, [status(thm)], [f2])).
% 121.12/16.54  fof(f2_sk, plain, ! [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))))), inference(skolemisation, [status(esa)], [f2_nnf])).
% 121.12/16.54  cnf(c4, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~complete_relstr(X0) | up_complete_relstr(X0), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 121.12/16.54  cnf(p400, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~complete_relstr(sk0) | up_complete_relstr(sk0), inference(resolution, [status(thm)], [c4, c90])).
% 121.12/16.54  fof(sdef7, definition, (spl7 <=> (~reflexive_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 121.12/16.54  cnf(ssp5, plain, (spl6 | spl7 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p400, sdef6, sdef7, sdef8, sdef9])).
% 121.12/16.54  cnf(c5, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~complete_relstr(X0) | join_complete_relstr(X0), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 121.12/16.54  cnf(p405, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~complete_relstr(sk0) | join_complete_relstr(sk0), inference(resolution, [status(thm)], [c5, c90])).
% 121.12/16.54  cnf(ssp6, plain, (spl6 | spl7 | spl8 | spl10), inference(avatar_split_clause, [status(thm)], [p405, sdef6, sdef7, sdef8, sdef10])).
% 121.12/16.54  cnf(c206, plain, rel_str(sk10), inference(cnf_transformation, [status(esa)], [f75_sk])).
% 121.12/16.54  cnf(p407, plain, ~strict_rel_str(sk10) | sk10 = rel_str_of(the_carrier(sk10),the_InternalRel(sk10)), inference(resolution, [status(thm)], [c206, c0])).
% 121.12/16.54  fof(sdef11, definition, (spl11 <=> (~strict_rel_str(sk10))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 121.12/16.54  fof(sdef12, definition, (spl12 <=> (sk10 = rel_str_of(the_carrier(sk10),the_InternalRel(sk10)))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 121.12/16.54  cnf(ssp7, plain, (spl11 | spl12), inference(avatar_split_clause, [status(thm)], [p407, sdef11, sdef12])).
% 121.12/16.54  cnf(p410, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~complete_relstr(sk10) | up_complete_relstr(sk10), inference(resolution, [status(thm)], [c206, c4])).
% 121.12/16.54  cnf(ssp8, plain, (spl13 | spl14 | spl15 | spl16), inference(avatar_split_clause, [status(thm)], [p410, sdef13, sdef14, sdef15, sdef16])).
% 121.12/16.54  cnf(p415, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~complete_relstr(sk10) | join_complete_relstr(sk10), inference(resolution, [status(thm)], [c206, c5])).
% 121.12/16.54  cnf(ssp9, plain, (spl13 | spl14 | spl15 | spl17), inference(avatar_split_clause, [status(thm)], [p415, sdef13, sdef14, sdef15, sdef17])).
% 121.12/16.54  cnf(c212, plain, rel_str(sk11), inference(cnf_transformation, [status(esa)], [f76_sk])).
% 121.12/16.54  cnf(p417, plain, ~strict_rel_str(sk11) | sk11 = rel_str_of(the_carrier(sk11),the_InternalRel(sk11)), inference(resolution, [status(thm)], [c212, c0])).
% 121.12/16.54  fof(sdef19, definition, (spl19 <=> (sk11 = rel_str_of(the_carrier(sk11),the_InternalRel(sk11)))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 121.12/16.54  cnf(ssp10, plain, (spl18 | spl19), inference(avatar_split_clause, [status(thm)], [p417, sdef18, sdef19])).
% 121.12/16.54  fof(f3, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & reflexive_relstr(A) & join_complete_relstr(A) ) => ( ~ empty_carrier(A) & reflexive_relstr(A) & lower_bounded_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc11_waybel_0)).
% 121.12/16.54  fof(f3_nnf, plain, ! [A] : ((~(rel_str(A)) | (((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(join_complete_relstr(A))) | ((~(empty_carrier(A)) & reflexive_relstr(A)) & lower_bounded_relstr(A))))), inference(nnf_transformation, [status(thm)], [f3])).
% 121.12/16.54  fof(f3_sk, plain, ! [A] : ((~(rel_str(A)) | (((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(join_complete_relstr(A))) | ((~(empty_carrier(A)) & reflexive_relstr(A)) & lower_bounded_relstr(A))))), inference(skolemisation, [status(esa)], [f3_nnf])).
% 121.12/16.54  cnf(c8, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~join_complete_relstr(X0) | lower_bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 121.12/16.54  cnf(p420, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~join_complete_relstr(sk0) | lower_bounded_relstr(sk0), inference(resolution, [status(thm)], [c8, c90])).
% 121.12/16.54  cnf(ssp11, plain, (spl6 | spl7 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p420, sdef6, sdef7, sdef20, sdef21])).
% 121.12/16.54  cnf(p423, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~join_complete_relstr(sk10) | lower_bounded_relstr(sk10), inference(resolution, [status(thm)], [c8, c206])).
% 121.12/16.54  cnf(ssp12, plain, (spl13 | spl14 | spl22 | spl23), inference(avatar_split_clause, [status(thm)], [p423, sdef13, sdef14, sdef22, sdef23])).
% 121.12/16.54  cnf(c228, plain, rel_str(sk13), inference(cnf_transformation, [status(esa)], [f78_sk])).
% 121.12/16.54  cnf(p426, plain, ~strict_rel_str(sk13) | sk13 = rel_str_of(the_carrier(sk13),the_InternalRel(sk13)), inference(resolution, [status(thm)], [c228, c0])).
% 121.12/16.54  fof(sdef25, definition, (spl25 <=> (sk13 = rel_str_of(the_carrier(sk13),the_InternalRel(sk13)))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 121.12/16.54  cnf(ssp13, plain, (spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p426, sdef24, sdef25])).
% 121.12/16.54  cnf(p429, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~complete_relstr(sk13) | up_complete_relstr(sk13), inference(resolution, [status(thm)], [c228, c4])).
% 121.12/16.54  cnf(ssp14, plain, (spl26 | spl27 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p429, sdef26, sdef27, sdef28, sdef29])).
% 121.12/16.54  cnf(p434, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~complete_relstr(sk13) | join_complete_relstr(sk13), inference(resolution, [status(thm)], [c228, c5])).
% 121.12/16.54  cnf(ssp15, plain, (spl26 | spl27 | spl28 | spl30), inference(avatar_split_clause, [status(thm)], [p434, sdef26, sdef27, sdef28, sdef30])).
% 121.12/16.54  cnf(p436, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~join_complete_relstr(sk13) | lower_bounded_relstr(sk13), inference(resolution, [status(thm)], [c228, c8])).
% 121.12/16.54  cnf(ssp16, plain, (spl26 | spl27 | spl31 | spl32), inference(avatar_split_clause, [status(thm)], [p436, sdef26, sdef27, sdef31, sdef32])).
% 121.12/16.54  cnf(c244, plain, rel_str(sk18), inference(cnf_transformation, [status(esa)], [f83_sk])).
% 121.12/16.54  cnf(p439, plain, ~strict_rel_str(sk18) | sk18 = rel_str_of(the_carrier(sk18),the_InternalRel(sk18)), inference(resolution, [status(thm)], [c244, c0])).
% 121.12/16.54  fof(sdef34, definition, (spl34 <=> (sk18 = rel_str_of(the_carrier(sk18),the_InternalRel(sk18)))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 121.12/16.54  cnf(ssp17, plain, (spl33 | spl34), inference(avatar_split_clause, [status(thm)], [p439, sdef33, sdef34])).
% 121.12/16.54  cnf(p442, plain, empty_carrier(sk18) | ~reflexive_relstr(sk18) | ~complete_relstr(sk18) | up_complete_relstr(sk18), inference(resolution, [status(thm)], [c244, c4])).
% 121.12/16.54  cnf(ssp18, plain, (spl35 | spl36 | spl37 | spl38), inference(avatar_split_clause, [status(thm)], [p442, sdef35, sdef36, sdef37, sdef38])).
% 121.12/16.54  cnf(p447, plain, empty_carrier(sk18) | ~reflexive_relstr(sk18) | ~complete_relstr(sk18) | join_complete_relstr(sk18), inference(resolution, [status(thm)], [c244, c5])).
% 121.12/16.54  fof(sdef39, definition, (spl39 <=> (join_complete_relstr(sk18))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 121.12/16.54  cnf(ssp19, plain, (spl35 | spl36 | spl37 | spl39), inference(avatar_split_clause, [status(thm)], [p447, sdef35, sdef36, sdef37, sdef39])).
% 121.12/16.54  fof(f4, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & reflexive_relstr(A) & transitive_relstr(A) & antisymmetric_relstr(A) & with_suprema_relstr(A) & lower_bounded_relstr(A) & up_complete_relstr(A) ) => ( ~ empty_carrier(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) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc12_waybel_0)).
% 121.12/16.54  fof(f4_nnf, plain, ! [A] : ((~(rel_str(A)) | (((((((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(transitive_relstr(A))) | ~(antisymmetric_relstr(A))) | ~(with_suprema_relstr(A))) | ~(lower_bounded_relstr(A))) | ~(up_complete_relstr(A))) | (((((((((~(empty_carrier(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))))), inference(nnf_transformation, [status(thm)], [f4])).
% 121.12/16.54  fof(f4_sk, plain, ! [A] : ((~(rel_str(A)) | (((((((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(transitive_relstr(A))) | ~(antisymmetric_relstr(A))) | ~(with_suprema_relstr(A))) | ~(lower_bounded_relstr(A))) | ~(up_complete_relstr(A))) | (((((((((~(empty_carrier(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))))), inference(skolemisation, [status(esa)], [f4_nnf])).
% 121.12/16.54  cnf(c14, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~transitive_relstr(X0) | ~antisymmetric_relstr(X0) | ~with_suprema_relstr(X0) | ~lower_bounded_relstr(X0) | ~up_complete_relstr(X0) | with_infima_relstr(X0), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 121.12/16.54  cnf(p449, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~transitive_relstr(sk0) | ~antisymmetric_relstr(sk0) | ~with_suprema_relstr(sk0) | ~lower_bounded_relstr(sk0) | ~up_complete_relstr(sk0) | with_infima_relstr(sk0), inference(resolution, [status(thm)], [c14, c90])).
% 121.12/16.54  cnf(ssp20, plain, (spl6 | spl7 | spl40 | spl41 | spl42 | spl43 | spl44 | spl45), inference(avatar_split_clause, [status(thm)], [p449, sdef6, sdef7, sdef40, sdef41, sdef42, sdef43, sdef44, sdef45])).
% 121.12/16.54  cnf(p456, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~transitive_relstr(sk10) | ~antisymmetric_relstr(sk10) | ~with_suprema_relstr(sk10) | ~lower_bounded_relstr(sk10) | ~up_complete_relstr(sk10) | with_infima_relstr(sk10), inference(resolution, [status(thm)], [c14, c206])).
% 121.12/16.54  fof(sdef51, definition, (spl51 <=> (with_infima_relstr(sk10))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 121.12/16.54  cnf(ssp21, plain, (spl13 | spl14 | spl46 | spl47 | spl48 | spl49 | spl50 | spl51), inference(avatar_split_clause, [status(thm)], [p456, sdef13, sdef14, sdef46, sdef47, sdef48, sdef49, sdef50, sdef51])).
% 121.12/16.54  cnf(p463, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~transitive_relstr(sk13) | ~antisymmetric_relstr(sk13) | ~with_suprema_relstr(sk13) | ~lower_bounded_relstr(sk13) | ~up_complete_relstr(sk13) | with_infima_relstr(sk13), inference(resolution, [status(thm)], [c14, c228])).
% 121.12/16.54  fof(sdef57, definition, (spl57 <=> (with_infima_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 121.12/16.54  cnf(ssp22, plain, (spl26 | spl27 | spl52 | spl53 | spl54 | spl55 | spl56 | spl57), inference(avatar_split_clause, [status(thm)], [p463, sdef26, sdef27, sdef52, sdef53, sdef54, sdef55, sdef56, sdef57])).
% 121.12/16.54  cnf(c15, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~transitive_relstr(X0) | ~antisymmetric_relstr(X0) | ~with_suprema_relstr(X0) | ~lower_bounded_relstr(X0) | ~up_complete_relstr(X0) | complete_relstr(X0), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 121.12/16.54  cnf(p470, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~transitive_relstr(sk0) | ~antisymmetric_relstr(sk0) | ~with_suprema_relstr(sk0) | ~lower_bounded_relstr(sk0) | ~up_complete_relstr(sk0) | complete_relstr(sk0), inference(resolution, [status(thm)], [c15, c90])).
% 121.12/16.54  cnf(ssp23, plain, (spl6 | spl7 | spl40 | spl41 | spl42 | spl43 | spl44 | spl58), inference(avatar_split_clause, [status(thm)], [p470, sdef6, sdef7, sdef40, sdef41, sdef42, sdef43, sdef44, sdef58])).
% 121.12/16.54  cnf(p472, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~transitive_relstr(sk10) | ~antisymmetric_relstr(sk10) | ~with_suprema_relstr(sk10) | ~lower_bounded_relstr(sk10) | ~up_complete_relstr(sk10) | complete_relstr(sk10), inference(resolution, [status(thm)], [c15, c206])).
% 121.12/16.54  cnf(ssp24, plain, (spl13 | spl14 | spl46 | spl47 | spl48 | spl49 | spl50 | spl59), inference(avatar_split_clause, [status(thm)], [p472, sdef13, sdef14, sdef46, sdef47, sdef48, sdef49, sdef50, sdef59])).
% 121.12/16.54  cnf(p474, plain, empty_carrier(sk18) | ~reflexive_relstr(sk18) | ~transitive_relstr(sk18) | ~antisymmetric_relstr(sk18) | ~with_suprema_relstr(sk18) | ~lower_bounded_relstr(sk18) | ~up_complete_relstr(sk18) | complete_relstr(sk18), inference(resolution, [status(thm)], [c15, c244])).
% 121.12/16.54  cnf(ssp25, plain, (spl35 | spl36 | spl60 | spl61 | spl62 | spl63 | spl64 | spl65), inference(avatar_split_clause, [status(thm)], [p474, sdef35, sdef36, sdef60, sdef61, sdef62, sdef63, sdef64, sdef65])).
% 121.12/16.54  cnf(c17, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~transitive_relstr(X0) | ~antisymmetric_relstr(X0) | ~with_suprema_relstr(X0) | ~lower_bounded_relstr(X0) | ~up_complete_relstr(X0) | upper_bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 121.12/16.54  cnf(p481, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~transitive_relstr(sk0) | ~antisymmetric_relstr(sk0) | ~with_suprema_relstr(sk0) | ~lower_bounded_relstr(sk0) | ~up_complete_relstr(sk0) | upper_bounded_relstr(sk0), inference(resolution, [status(thm)], [c17, c90])).
% 121.12/16.54  cnf(ssp26, plain, (spl6 | spl7 | spl40 | spl41 | spl42 | spl43 | spl44 | spl66), inference(avatar_split_clause, [status(thm)], [p481, sdef6, sdef7, sdef40, sdef41, sdef42, sdef43, sdef44, sdef66])).
% 121.12/16.54  cnf(p483, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~transitive_relstr(sk10) | ~antisymmetric_relstr(sk10) | ~with_suprema_relstr(sk10) | ~lower_bounded_relstr(sk10) | ~up_complete_relstr(sk10) | upper_bounded_relstr(sk10), inference(resolution, [status(thm)], [c17, c206])).
% 121.12/16.54  cnf(ssp27, plain, (spl13 | spl14 | spl46 | spl47 | spl48 | spl49 | spl50 | spl67), inference(avatar_split_clause, [status(thm)], [p483, sdef13, sdef14, sdef46, sdef47, sdef48, sdef49, sdef50, sdef67])).
% 121.12/16.54  cnf(p485, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~transitive_relstr(sk13) | ~antisymmetric_relstr(sk13) | ~with_suprema_relstr(sk13) | ~lower_bounded_relstr(sk13) | ~up_complete_relstr(sk13) | upper_bounded_relstr(sk13), inference(resolution, [status(thm)], [c17, c228])).
% 121.12/16.54  cnf(ssp28, plain, (spl26 | spl27 | spl52 | spl53 | spl54 | spl55 | spl56 | spl68), inference(avatar_split_clause, [status(thm)], [p485, sdef26, sdef27, sdef52, sdef53, sdef54, sdef55, sdef56, sdef68])).
% 121.12/16.54  cnf(c261, plain, rel_str(sk19), inference(cnf_transformation, [status(esa)], [f84_sk])).
% 121.12/16.54  cnf(p487, plain, ~strict_rel_str(sk19) | sk19 = rel_str_of(the_carrier(sk19),the_InternalRel(sk19)), inference(resolution, [status(thm)], [c261, c0])).
% 121.12/16.54  fof(sdef70, definition, (spl70 <=> (sk19 = rel_str_of(the_carrier(sk19),the_InternalRel(sk19)))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 121.12/16.54  cnf(ssp29, plain, (spl69 | spl70), inference(avatar_split_clause, [status(thm)], [p487, sdef69, sdef70])).
% 121.12/16.54  cnf(p490, plain, empty_carrier(sk19) | ~reflexive_relstr(sk19) | ~complete_relstr(sk19) | up_complete_relstr(sk19), inference(resolution, [status(thm)], [c261, c4])).
% 121.12/16.54  cnf(ssp30, plain, (spl71 | spl72 | spl73 | spl74), inference(avatar_split_clause, [status(thm)], [p490, sdef71, sdef72, sdef73, sdef74])).
% 121.12/16.54  cnf(p495, plain, empty_carrier(sk19) | ~reflexive_relstr(sk19) | ~complete_relstr(sk19) | join_complete_relstr(sk19), inference(resolution, [status(thm)], [c261, c5])).
% 121.12/16.54  cnf(ssp31, plain, (spl71 | spl72 | spl73 | spl75), inference(avatar_split_clause, [status(thm)], [p495, sdef71, sdef72, sdef73, sdef75])).
% 121.12/16.54  cnf(p497, plain, empty_carrier(sk19) | ~reflexive_relstr(sk19) | ~join_complete_relstr(sk19) | lower_bounded_relstr(sk19), inference(resolution, [status(thm)], [c261, c8])).
% 121.12/16.54  cnf(ssp32, plain, (spl71 | spl72 | spl76 | spl77), inference(avatar_split_clause, [status(thm)], [p497, sdef71, sdef72, sdef76, sdef77])).
% 121.12/16.54  cnf(p500, plain, empty_carrier(sk19) | ~reflexive_relstr(sk19) | ~transitive_relstr(sk19) | ~antisymmetric_relstr(sk19) | ~with_suprema_relstr(sk19) | ~lower_bounded_relstr(sk19) | ~up_complete_relstr(sk19) | upper_bounded_relstr(sk19), inference(resolution, [status(thm)], [c261, c17])).
% 121.12/16.54  cnf(ssp33, plain, (spl71 | spl72 | spl78 | spl79 | spl80 | spl81 | spl82 | spl83), inference(avatar_split_clause, [status(thm)], [p500, sdef71, sdef72, sdef78, sdef79, sdef80, sdef81, sdef82, sdef83])).
% 121.12/16.54  cnf(c18, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~transitive_relstr(X0) | ~antisymmetric_relstr(X0) | ~with_suprema_relstr(X0) | ~lower_bounded_relstr(X0) | ~up_complete_relstr(X0) | bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 121.12/16.54  cnf(p507, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~transitive_relstr(sk0) | ~antisymmetric_relstr(sk0) | ~with_suprema_relstr(sk0) | ~lower_bounded_relstr(sk0) | ~up_complete_relstr(sk0) | bounded_relstr(sk0), inference(resolution, [status(thm)], [c18, c90])).
% 121.12/16.54  cnf(ssp34, plain, (spl6 | spl7 | spl40 | spl41 | spl42 | spl43 | spl44 | spl84), inference(avatar_split_clause, [status(thm)], [p507, sdef6, sdef7, sdef40, sdef41, sdef42, sdef43, sdef44, sdef84])).
% 121.12/16.54  cnf(p509, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~transitive_relstr(sk10) | ~antisymmetric_relstr(sk10) | ~with_suprema_relstr(sk10) | ~lower_bounded_relstr(sk10) | ~up_complete_relstr(sk10) | bounded_relstr(sk10), inference(resolution, [status(thm)], [c18, c206])).
% 121.12/16.54  cnf(ssp35, plain, (spl13 | spl14 | spl46 | spl47 | spl48 | spl49 | spl50 | spl85), inference(avatar_split_clause, [status(thm)], [p509, sdef13, sdef14, sdef46, sdef47, sdef48, sdef49, sdef50, sdef85])).
% 121.12/16.54  cnf(p511, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~transitive_relstr(sk13) | ~antisymmetric_relstr(sk13) | ~with_suprema_relstr(sk13) | ~lower_bounded_relstr(sk13) | ~up_complete_relstr(sk13) | bounded_relstr(sk13), inference(resolution, [status(thm)], [c18, c228])).
% 121.12/16.54  cnf(ssp36, plain, (spl26 | spl27 | spl52 | spl53 | spl54 | spl55 | spl56 | spl86), inference(avatar_split_clause, [status(thm)], [p511, sdef26, sdef27, sdef52, sdef53, sdef54, sdef55, sdef56, sdef86])).
% 121.12/16.54  cnf(p513, plain, empty_carrier(sk19) | ~reflexive_relstr(sk19) | ~transitive_relstr(sk19) | ~antisymmetric_relstr(sk19) | ~with_suprema_relstr(sk19) | ~lower_bounded_relstr(sk19) | ~up_complete_relstr(sk19) | bounded_relstr(sk19), inference(resolution, [status(thm)], [c18, c261])).
% 121.12/16.54  cnf(ssp37, plain, (spl71 | spl72 | spl78 | spl79 | spl80 | spl81 | spl82 | spl87), inference(avatar_split_clause, [status(thm)], [p513, sdef71, sdef72, sdef78, sdef79, sdef80, sdef81, sdef82, sdef87])).
% 121.12/16.54  cnf(c271, plain, rel_str(sk20), inference(cnf_transformation, [status(esa)], [f85_sk])).
% 121.12/16.54  cnf(p515, plain, ~strict_rel_str(sk20) | sk20 = rel_str_of(the_carrier(sk20),the_InternalRel(sk20)), inference(resolution, [status(thm)], [c271, c0])).
% 121.12/16.54  fof(sdef89, definition, (spl89 <=> (sk20 = rel_str_of(the_carrier(sk20),the_InternalRel(sk20)))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 121.12/16.54  cnf(ssp38, plain, (spl88 | spl89), inference(avatar_split_clause, [status(thm)], [p515, sdef88, sdef89])).
% 121.12/16.54  cnf(p518, plain, empty_carrier(sk20) | ~reflexive_relstr(sk20) | ~complete_relstr(sk20) | up_complete_relstr(sk20), inference(resolution, [status(thm)], [c271, c4])).
% 121.12/16.54  cnf(ssp39, plain, (spl90 | spl91 | spl92 | spl93), inference(avatar_split_clause, [status(thm)], [p518, sdef90, sdef91, sdef92, sdef93])).
% 121.12/16.54  cnf(p523, plain, empty_carrier(sk20) | ~reflexive_relstr(sk20) | ~complete_relstr(sk20) | join_complete_relstr(sk20), inference(resolution, [status(thm)], [c271, c5])).
% 121.12/16.54  cnf(ssp40, plain, (spl90 | spl91 | spl92 | spl94), inference(avatar_split_clause, [status(thm)], [p523, sdef90, sdef91, sdef92, sdef94])).
% 121.12/16.54  cnf(p525, plain, empty_carrier(sk20) | ~reflexive_relstr(sk20) | ~join_complete_relstr(sk20) | lower_bounded_relstr(sk20), inference(resolution, [status(thm)], [c271, c8])).
% 121.12/16.54  cnf(ssp41, plain, (spl90 | spl91 | spl95 | spl96), inference(avatar_split_clause, [status(thm)], [p525, sdef90, sdef91, sdef95, sdef96])).
% 121.12/16.54  cnf(p528, plain, empty_carrier(sk20) | ~reflexive_relstr(sk20) | ~transitive_relstr(sk20) | ~antisymmetric_relstr(sk20) | ~with_suprema_relstr(sk20) | ~lower_bounded_relstr(sk20) | ~up_complete_relstr(sk20) | upper_bounded_relstr(sk20), inference(resolution, [status(thm)], [c271, c17])).
% 121.12/16.54  cnf(ssp42, plain, (spl90 | spl91 | spl97 | spl98 | spl99 | spl100 | spl101 | spl102), inference(avatar_split_clause, [status(thm)], [p528, sdef90, sdef91, sdef97, sdef98, sdef99, sdef100, sdef101, sdef102])).
% 121.12/16.54  cnf(p535, plain, empty_carrier(sk20) | ~reflexive_relstr(sk20) | ~transitive_relstr(sk20) | ~antisymmetric_relstr(sk20) | ~with_suprema_relstr(sk20) | ~lower_bounded_relstr(sk20) | ~up_complete_relstr(sk20) | bounded_relstr(sk20), inference(resolution, [status(thm)], [c271, c18])).
% 121.12/16.54  cnf(ssp43, plain, (spl90 | spl91 | spl97 | spl98 | spl99 | spl100 | spl101 | spl103), inference(avatar_split_clause, [status(thm)], [p535, sdef90, sdef91, sdef97, sdef98, sdef99, sdef100, sdef101, sdef103])).
% 121.12/16.54  fof(f5, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & reflexive_relstr(A) & antisymmetric_relstr(A) & join_complete_relstr(A) ) => ( ~ empty_carrier(A) & reflexive_relstr(A) & antisymmetric_relstr(A) & with_infima_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc13_waybel_0)).
% 121.12/16.54  fof(f5_nnf, plain, ! [A] : ((~(rel_str(A)) | ((((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(antisymmetric_relstr(A))) | ~(join_complete_relstr(A))) | (((~(empty_carrier(A)) & reflexive_relstr(A)) & antisymmetric_relstr(A)) & with_infima_relstr(A))))), inference(nnf_transformation, [status(thm)], [f5])).
% 121.12/16.54  fof(f5_sk, plain, ! [A] : ((~(rel_str(A)) | ((((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(antisymmetric_relstr(A))) | ~(join_complete_relstr(A))) | (((~(empty_carrier(A)) & reflexive_relstr(A)) & antisymmetric_relstr(A)) & with_infima_relstr(A))))), inference(skolemisation, [status(esa)], [f5_nnf])).
% 121.12/16.54  cnf(c22, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~antisymmetric_relstr(X0) | ~join_complete_relstr(X0) | with_infima_relstr(X0), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 121.12/16.54  cnf(p537, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~antisymmetric_relstr(sk0) | ~join_complete_relstr(sk0) | with_infima_relstr(sk0), inference(resolution, [status(thm)], [c22, c90])).
% 121.12/16.54  cnf(ssp44, plain, (spl6 | spl7 | spl20 | spl41 | spl45), inference(avatar_split_clause, [status(thm)], [p537, sdef6, sdef7, sdef20, sdef41, sdef45])).
% 121.12/16.54  cnf(p538, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~antisymmetric_relstr(sk10) | ~join_complete_relstr(sk10) | with_infima_relstr(sk10), inference(resolution, [status(thm)], [c22, c206])).
% 121.12/16.54  cnf(ssp45, plain, (spl13 | spl14 | spl22 | spl47 | spl51), inference(avatar_split_clause, [status(thm)], [p538, sdef13, sdef14, sdef22, sdef47, sdef51])).
% 121.12/16.54  cnf(p539, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~antisymmetric_relstr(sk13) | ~join_complete_relstr(sk13) | with_infima_relstr(sk13), inference(resolution, [status(thm)], [c22, c228])).
% 121.12/16.54  cnf(ssp46, plain, (spl26 | spl27 | spl31 | spl53 | spl57), inference(avatar_split_clause, [status(thm)], [p539, sdef26, sdef27, sdef31, sdef53, sdef57])).
% 121.12/16.54  cnf(c295, plain, rel_str(sk26), inference(cnf_transformation, [status(esa)], [f91_sk])).
% 121.12/16.54  cnf(p540, plain, ~strict_rel_str(sk26) | sk26 = rel_str_of(the_carrier(sk26),the_InternalRel(sk26)), inference(resolution, [status(thm)], [c295, c0])).
% 121.12/16.54  fof(sdef104, definition, (spl104 <=> (~strict_rel_str(sk26))), introduced(definition, [new_symbols(naming, [spl104])], [avatar_definition])).
% 121.12/16.54  fof(sdef105, definition, (spl105 <=> (sk26 = rel_str_of(the_carrier(sk26),the_InternalRel(sk26)))), introduced(definition, [new_symbols(naming, [spl105])], [avatar_definition])).
% 121.12/16.54  cnf(ssp47, plain, (spl104 | spl105), inference(avatar_split_clause, [status(thm)], [p540, sdef104, sdef105])).
% 121.12/16.54  cnf(p543, plain, empty_carrier(sk26) | ~reflexive_relstr(sk26) | ~complete_relstr(sk26) | up_complete_relstr(sk26), inference(resolution, [status(thm)], [c295, c4])).
% 121.12/16.54  fof(sdef109, definition, (spl109 <=> (up_complete_relstr(sk26))), introduced(definition, [new_symbols(naming, [spl109])], [avatar_definition])).
% 121.12/16.54  cnf(ssp48, plain, (spl106 | spl107 | spl108 | spl109), inference(avatar_split_clause, [status(thm)], [p543, sdef106, sdef107, sdef108, sdef109])).
% 121.12/16.54  cnf(p548, plain, empty_carrier(sk26) | ~reflexive_relstr(sk26) | ~complete_relstr(sk26) | join_complete_relstr(sk26), inference(resolution, [status(thm)], [c295, c5])).
% 121.12/16.54  fof(sdef110, definition, (spl110 <=> (join_complete_relstr(sk26))), introduced(definition, [new_symbols(naming, [spl110])], [avatar_definition])).
% 121.12/16.54  cnf(ssp49, plain, (spl106 | spl107 | spl108 | spl110), inference(avatar_split_clause, [status(thm)], [p548, sdef106, sdef107, sdef108, sdef110])).
% 121.12/16.54  fof(f6, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & reflexive_relstr(A) & antisymmetric_relstr(A) & upper_bounded_relstr(A) & join_complete_relstr(A) ) => ( ~ empty_carrier(A) & reflexive_relstr(A) & antisymmetric_relstr(A) & with_suprema_relstr(A) & upper_bounded_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc14_waybel_0)).
% 121.12/16.54  fof(f6_nnf, plain, ! [A] : ((~(rel_str(A)) | (((((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(antisymmetric_relstr(A))) | ~(upper_bounded_relstr(A))) | ~(join_complete_relstr(A))) | ((((~(empty_carrier(A)) & reflexive_relstr(A)) & antisymmetric_relstr(A)) & with_suprema_relstr(A)) & upper_bounded_relstr(A))))), inference(nnf_transformation, [status(thm)], [f6])).
% 121.12/16.54  fof(f6_sk, plain, ! [A] : ((~(rel_str(A)) | (((((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(antisymmetric_relstr(A))) | ~(upper_bounded_relstr(A))) | ~(join_complete_relstr(A))) | ((((~(empty_carrier(A)) & reflexive_relstr(A)) & antisymmetric_relstr(A)) & with_suprema_relstr(A)) & upper_bounded_relstr(A))))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 121.12/16.54  cnf(c26, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~antisymmetric_relstr(X0) | ~upper_bounded_relstr(X0) | ~join_complete_relstr(X0) | with_suprema_relstr(X0), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 121.12/16.54  cnf(p550, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~antisymmetric_relstr(sk0) | ~upper_bounded_relstr(sk0) | ~join_complete_relstr(sk0) | with_suprema_relstr(sk0), inference(resolution, [status(thm)], [c26, c90])).
% 121.12/16.54  cnf(ssp50, plain, (spl6 | spl7 | spl20 | spl41 | spl111 | spl112), inference(avatar_split_clause, [status(thm)], [p550, sdef6, sdef7, sdef20, sdef41, sdef111, sdef112])).
% 121.12/16.54  cnf(p553, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~antisymmetric_relstr(sk10) | ~upper_bounded_relstr(sk10) | ~join_complete_relstr(sk10) | with_suprema_relstr(sk10), inference(resolution, [status(thm)], [c26, c206])).
% 121.12/16.54  cnf(ssp51, plain, (spl13 | spl14 | spl22 | spl47 | spl113 | spl114), inference(avatar_split_clause, [status(thm)], [p553, sdef13, sdef14, sdef22, sdef47, sdef113, sdef114])).
% 121.12/16.54  cnf(p556, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~antisymmetric_relstr(sk13) | ~upper_bounded_relstr(sk13) | ~join_complete_relstr(sk13) | with_suprema_relstr(sk13), inference(resolution, [status(thm)], [c26, c228])).
% 121.12/16.54  cnf(ssp52, plain, (spl26 | spl27 | spl31 | spl53 | spl115 | spl116), inference(avatar_split_clause, [status(thm)], [p556, sdef26, sdef27, sdef31, sdef53, sdef115, sdef116])).
% 121.12/16.54  cnf(c331, plain, rel_str(sk34), inference(cnf_transformation, [status(esa)], [f99_sk])).
% 121.12/16.54  cnf(p559, plain, ~strict_rel_str(sk34) | sk34 = rel_str_of(the_carrier(sk34),the_InternalRel(sk34)), inference(resolution, [status(thm)], [c331, c0])).
% 121.12/16.54  fof(sdef118, definition, (spl118 <=> (sk34 = rel_str_of(the_carrier(sk34),the_InternalRel(sk34)))), introduced(definition, [new_symbols(naming, [spl118])], [avatar_definition])).
% 121.12/16.54  cnf(ssp53, plain, (spl117 | spl118), inference(avatar_split_clause, [status(thm)], [p559, sdef117, sdef118])).
% 121.12/16.54  cnf(p562, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~complete_relstr(sk34) | up_complete_relstr(sk34), inference(resolution, [status(thm)], [c331, c4])).
% 121.12/16.54  fof(sdef120, definition, (spl120 <=> (~reflexive_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl120])], [avatar_definition])).
% 121.12/16.54  cnf(ssp54, plain, (spl119 | spl120 | spl121 | spl122), inference(avatar_split_clause, [status(thm)], [p562, sdef119, sdef120, sdef121, sdef122])).
% 121.12/16.54  cnf(p567, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~complete_relstr(sk34) | join_complete_relstr(sk34), inference(resolution, [status(thm)], [c331, c5])).
% 121.12/16.54  cnf(ssp55, plain, (spl119 | spl120 | spl121 | spl123), inference(avatar_split_clause, [status(thm)], [p567, sdef119, sdef120, sdef121, sdef123])).
% 121.12/16.54  cnf(p569, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~join_complete_relstr(sk34) | lower_bounded_relstr(sk34), inference(resolution, [status(thm)], [c331, c8])).
% 121.12/16.54  cnf(ssp56, plain, (spl119 | spl120 | spl124 | spl125), inference(avatar_split_clause, [status(thm)], [p569, sdef119, sdef120, sdef124, sdef125])).
% 121.12/16.54  cnf(p572, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~transitive_relstr(sk34) | ~antisymmetric_relstr(sk34) | ~with_suprema_relstr(sk34) | ~lower_bounded_relstr(sk34) | ~up_complete_relstr(sk34) | with_infima_relstr(sk34), inference(resolution, [status(thm)], [c331, c14])).
% 121.12/16.54  fof(sdef131, definition, (spl131 <=> (with_infima_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl131])], [avatar_definition])).
% 121.12/16.54  cnf(ssp57, plain, (spl119 | spl120 | spl126 | spl127 | spl128 | spl129 | spl130 | spl131), inference(avatar_split_clause, [status(thm)], [p572, sdef119, sdef120, sdef126, sdef127, sdef128, sdef129, sdef130, sdef131])).
% 121.12/16.54  cnf(p579, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~transitive_relstr(sk34) | ~antisymmetric_relstr(sk34) | ~with_suprema_relstr(sk34) | ~lower_bounded_relstr(sk34) | ~up_complete_relstr(sk34) | complete_relstr(sk34), inference(resolution, [status(thm)], [c331, c15])).
% 121.12/16.54  cnf(ssp58, plain, (spl119 | spl120 | spl126 | spl127 | spl128 | spl129 | spl130 | spl132), inference(avatar_split_clause, [status(thm)], [p579, sdef119, sdef120, sdef126, sdef127, sdef128, sdef129, sdef130, sdef132])).
% 121.12/16.54  cnf(p581, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~transitive_relstr(sk34) | ~antisymmetric_relstr(sk34) | ~with_suprema_relstr(sk34) | ~lower_bounded_relstr(sk34) | ~up_complete_relstr(sk34) | upper_bounded_relstr(sk34), inference(resolution, [status(thm)], [c331, c17])).
% 121.12/16.54  cnf(ssp59, plain, (spl119 | spl120 | spl126 | spl127 | spl128 | spl129 | spl130 | spl133), inference(avatar_split_clause, [status(thm)], [p581, sdef119, sdef120, sdef126, sdef127, sdef128, sdef129, sdef130, sdef133])).
% 121.12/16.54  cnf(p583, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~transitive_relstr(sk34) | ~antisymmetric_relstr(sk34) | ~with_suprema_relstr(sk34) | ~lower_bounded_relstr(sk34) | ~up_complete_relstr(sk34) | bounded_relstr(sk34), inference(resolution, [status(thm)], [c331, c18])).
% 121.12/16.54  cnf(ssp60, plain, (spl119 | spl120 | spl126 | spl127 | spl128 | spl129 | spl130 | spl134), inference(avatar_split_clause, [status(thm)], [p583, sdef119, sdef120, sdef126, sdef127, sdef128, sdef129, sdef130, sdef134])).
% 121.12/16.54  cnf(p585, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~antisymmetric_relstr(sk34) | ~join_complete_relstr(sk34) | with_infima_relstr(sk34), inference(resolution, [status(thm)], [c331, c22])).
% 121.12/16.54  cnf(ssp61, plain, (spl119 | spl120 | spl124 | spl127 | spl131), inference(avatar_split_clause, [status(thm)], [p585, sdef119, sdef120, sdef124, sdef127, sdef131])).
% 121.12/16.54  cnf(p586, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~antisymmetric_relstr(sk34) | ~upper_bounded_relstr(sk34) | ~join_complete_relstr(sk34) | with_suprema_relstr(sk34), inference(resolution, [status(thm)], [c331, c26])).
% 121.12/16.54  cnf(ssp62, plain, (spl119 | spl120 | spl124 | spl127 | spl135 | spl136), inference(avatar_split_clause, [status(thm)], [p586, sdef119, sdef120, sdef124, sdef127, sdef135, sdef136])).
% 121.12/16.54  fof(f8, axiom, ! [A] : ( rel_str(A) => ( with_suprema_relstr(A) => ~ empty_carrier(A) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc1_lattice3)).
% 121.12/16.54  fof(f8_nnf, plain, ! [A] : ((~(rel_str(A)) | (~(with_suprema_relstr(A)) | ~(empty_carrier(A))))), inference(nnf_transformation, [status(thm)], [f8])).
% 121.12/16.54  fof(f8_sk, plain, ! [A] : ((~(rel_str(A)) | (~(with_suprema_relstr(A)) | ~(empty_carrier(A))))), inference(skolemisation, [status(esa)], [f8_nnf])).
% 121.12/16.54  cnf(c29, plain, ~rel_str(X0) | ~with_suprema_relstr(X0) | ~empty_carrier(X0), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 121.12/16.54  cnf(p591, plain, ~with_suprema_relstr(sk0) | ~empty_carrier(sk0), inference(resolution, [status(thm)], [c29, c90])).
% 121.12/16.54  cnf(ssp63, plain, (spl42 | spl137), inference(avatar_split_clause, [status(thm)], [p591, sdef42, sdef137])).
% 121.12/16.54  fof(f11, axiom, ! [A] : ( ( topological_space(A) & top_str(A) ) => ! [B] : ( element(B,powerset(the_carrier(A))) => ( empty(B) => ( open_subset(B,A) & closed_subset(B,A) ) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc1_tops_1)).
% 121.12/16.54  fof(f11_nnf, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | ! [B] : ((~(element(B,powerset(the_carrier(A)))) | (~(empty(B)) | (open_subset(B,A) & closed_subset(B,A))))))), inference(nnf_transformation, [status(thm)], [f11])).
% 121.12/16.54  fof(f11_sk, plain, ! [A,B] : (((~(topological_space(A)) | ~(top_str(A))) | (~(element(B,powerset(the_carrier(A)))) | (~(empty(B)) | (open_subset(B,A) & closed_subset(B,A)))))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 121.12/16.54  cnf(c32, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~empty(X1) | open_subset(X1,X0), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 121.12/16.54  cnf(c377, plain, topological_space(sk43), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(p600, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | open_subset(X0,sk43), inference(resolution, [status(thm)], [c32, c377])).
% 121.12/16.54  fof(sdef139, definition, (spl139 <=> (~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | open_subset(X0,sk43))), introduced(definition, [new_symbols(naming, [spl139])], [avatar_definition])).
% 121.12/16.54  cnf(ssp64, plain, (spl138 | spl139), inference(avatar_split_clause, [status(thm)], [p600, sdef138, sdef139])).
% 121.12/16.54  cnf(c33, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~empty(X1) | closed_subset(X1,X0), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 121.12/16.54  cnf(p606, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | closed_subset(X0,sk43), inference(resolution, [status(thm)], [c33, c377])).
% 121.12/16.54  fof(sdef140, definition, (spl140 <=> (~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | closed_subset(X0,sk43))), introduced(definition, [new_symbols(naming, [spl140])], [avatar_definition])).
% 121.12/16.54  cnf(ssp65, plain, (spl138 | spl140), inference(avatar_split_clause, [status(thm)], [p606, sdef138, sdef140])).
% 121.12/16.54  fof(f12, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & complete_relstr(A) ) => ( ~ empty_carrier(A) & with_suprema_relstr(A) & with_infima_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc1_yellow_0)).
% 121.12/16.54  fof(f12_nnf, plain, ! [A] : ((~(rel_str(A)) | ((empty_carrier(A) | ~(complete_relstr(A))) | ((~(empty_carrier(A)) & with_suprema_relstr(A)) & with_infima_relstr(A))))), inference(nnf_transformation, [status(thm)], [f12])).
% 121.12/16.54  fof(f12_sk, plain, ! [A] : ((~(rel_str(A)) | ((empty_carrier(A) | ~(complete_relstr(A))) | ((~(empty_carrier(A)) & with_suprema_relstr(A)) & with_infima_relstr(A))))), inference(skolemisation, [status(esa)], [f12_nnf])).
% 121.12/16.54  cnf(c35, plain, ~rel_str(X0) | empty_carrier(X0) | ~complete_relstr(X0) | with_suprema_relstr(X0), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 121.12/16.54  cnf(p612, plain, empty_carrier(sk0) | ~complete_relstr(sk0) | with_suprema_relstr(sk0), inference(resolution, [status(thm)], [c35, c90])).
% 121.12/16.54  cnf(ssp66, plain, (spl6 | spl8 | spl112), inference(avatar_split_clause, [status(thm)], [p612, sdef6, sdef8, sdef112])).
% 121.12/16.54  cnf(p613, plain, empty_carrier(sk10) | ~complete_relstr(sk10) | with_suprema_relstr(sk10), inference(resolution, [status(thm)], [c35, c206])).
% 121.12/16.54  cnf(ssp67, plain, (spl13 | spl15 | spl114), inference(avatar_split_clause, [status(thm)], [p613, sdef13, sdef15, sdef114])).
% 121.12/16.54  cnf(p614, plain, empty_carrier(sk13) | ~complete_relstr(sk13) | with_suprema_relstr(sk13), inference(resolution, [status(thm)], [c35, c228])).
% 121.12/16.54  cnf(ssp68, plain, (spl26 | spl28 | spl116), inference(avatar_split_clause, [status(thm)], [p614, sdef26, sdef28, sdef116])).
% 121.12/16.54  cnf(p615, plain, empty_carrier(sk34) | ~complete_relstr(sk34) | with_suprema_relstr(sk34), inference(resolution, [status(thm)], [c35, c331])).
% 121.12/16.54  cnf(ssp69, plain, (spl119 | spl121 | spl136), inference(avatar_split_clause, [status(thm)], [p615, sdef119, sdef121, sdef136])).
% 121.12/16.54  cnf(c36, plain, ~rel_str(X0) | empty_carrier(X0) | ~complete_relstr(X0) | with_infima_relstr(X0), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 121.12/16.54  cnf(p616, plain, empty_carrier(sk0) | ~complete_relstr(sk0) | with_infima_relstr(sk0), inference(resolution, [status(thm)], [c36, c90])).
% 121.12/16.54  cnf(ssp70, plain, (spl6 | spl8 | spl45), inference(avatar_split_clause, [status(thm)], [p616, sdef6, sdef8, sdef45])).
% 121.12/16.54  cnf(p617, plain, empty_carrier(sk10) | ~complete_relstr(sk10) | with_infima_relstr(sk10), inference(resolution, [status(thm)], [c36, c206])).
% 121.12/16.54  cnf(ssp71, plain, (spl13 | spl15 | spl51), inference(avatar_split_clause, [status(thm)], [p617, sdef13, sdef15, sdef51])).
% 121.12/16.54  cnf(p618, plain, empty_carrier(sk13) | ~complete_relstr(sk13) | with_infima_relstr(sk13), inference(resolution, [status(thm)], [c36, c228])).
% 121.12/16.54  cnf(ssp72, plain, (spl26 | spl28 | spl57), inference(avatar_split_clause, [status(thm)], [p618, sdef26, sdef28, sdef57])).
% 121.12/16.54  cnf(p619, plain, empty_carrier(sk34) | ~complete_relstr(sk34) | with_infima_relstr(sk34), inference(resolution, [status(thm)], [c36, c331])).
% 121.12/16.54  cnf(ssp73, plain, (spl119 | spl121 | spl131), inference(avatar_split_clause, [status(thm)], [p619, sdef119, sdef121, sdef131])).
% 121.12/16.54  fof(f14, axiom, ! [A] : ( rel_str(A) => ( with_infima_relstr(A) => ~ empty_carrier(A) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_lattice3)).
% 121.12/16.54  fof(f14_nnf, plain, ! [A] : ((~(rel_str(A)) | (~(with_infima_relstr(A)) | ~(empty_carrier(A))))), inference(nnf_transformation, [status(thm)], [f14])).
% 121.12/16.54  fof(f14_sk, plain, ! [A] : ((~(rel_str(A)) | (~(with_infima_relstr(A)) | ~(empty_carrier(A))))), inference(skolemisation, [status(esa)], [f14_nnf])).
% 121.12/16.54  cnf(c38, plain, ~rel_str(X0) | ~with_infima_relstr(X0) | ~empty_carrier(X0), inference(cnf_transformation, [status(esa)], [f14_sk])).
% 121.12/16.54  cnf(p625, plain, ~with_infima_relstr(sk0) | ~empty_carrier(sk0), inference(resolution, [status(thm)], [c38, c90])).
% 121.12/16.54  cnf(ssp74, plain, (spl137 | spl141), inference(avatar_split_clause, [status(thm)], [p625, sdef137, sdef141])).
% 121.12/16.54  fof(f16, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & reflexive_relstr(A) & trivial_carrier(A) ) => ( ~ empty_carrier(A) & reflexive_relstr(A) & transitive_relstr(A) & antisymmetric_relstr(A) & complete_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_yellow_0)).
% 121.12/16.54  fof(f16_nnf, plain, ! [A] : ((~(rel_str(A)) | (((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(trivial_carrier(A))) | ((((~(empty_carrier(A)) & reflexive_relstr(A)) & transitive_relstr(A)) & antisymmetric_relstr(A)) & complete_relstr(A))))), inference(nnf_transformation, [status(thm)], [f16])).
% 121.12/16.54  fof(f16_sk, plain, ! [A] : ((~(rel_str(A)) | (((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(trivial_carrier(A))) | ((((~(empty_carrier(A)) & reflexive_relstr(A)) & transitive_relstr(A)) & antisymmetric_relstr(A)) & complete_relstr(A))))), inference(skolemisation, [status(esa)], [f16_nnf])).
% 121.12/16.54  cnf(c42, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~trivial_carrier(X0) | transitive_relstr(X0), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 121.12/16.54  cnf(p641, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~trivial_carrier(sk0) | transitive_relstr(sk0), inference(resolution, [status(thm)], [c42, c90])).
% 121.12/16.54  fof(sdef142, definition, (spl142 <=> (~trivial_carrier(sk0))), introduced(definition, [new_symbols(naming, [spl142])], [avatar_definition])).
% 121.12/16.54  cnf(ssp75, plain, (spl6 | spl7 | spl142 | spl143), inference(avatar_split_clause, [status(thm)], [p641, sdef6, sdef7, sdef142, sdef143])).
% 121.12/16.54  cnf(c43, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~trivial_carrier(X0) | antisymmetric_relstr(X0), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 121.12/16.54  cnf(p646, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~trivial_carrier(sk0) | antisymmetric_relstr(sk0), inference(resolution, [status(thm)], [c43, c90])).
% 121.12/16.54  cnf(ssp76, plain, (spl6 | spl7 | spl142 | spl144), inference(avatar_split_clause, [status(thm)], [p646, sdef6, sdef7, sdef142, sdef144])).
% 121.12/16.54  cnf(p648, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~trivial_carrier(sk34) | antisymmetric_relstr(sk34), inference(resolution, [status(thm)], [c43, c331])).
% 121.12/16.54  fof(sdef145, definition, (spl145 <=> (~trivial_carrier(sk34))), introduced(definition, [new_symbols(naming, [spl145])], [avatar_definition])).
% 121.12/16.54  cnf(ssp77, plain, (spl119 | spl120 | spl145 | spl146), inference(avatar_split_clause, [status(thm)], [p648, sdef119, sdef120, sdef145, sdef146])).
% 121.12/16.54  cnf(c44, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~trivial_carrier(X0) | complete_relstr(X0), inference(cnf_transformation, [status(esa)], [f16_sk])).
% 121.12/16.54  cnf(p654, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~trivial_carrier(sk0) | complete_relstr(sk0), inference(resolution, [status(thm)], [c44, c90])).
% 121.12/16.54  cnf(ssp78, plain, (spl6 | spl7 | spl58 | spl142), inference(avatar_split_clause, [status(thm)], [p654, sdef6, sdef7, sdef58, sdef142])).
% 121.12/16.54  cnf(p655, plain, empty_carrier(sk10) | ~reflexive_relstr(sk10) | ~trivial_carrier(sk10) | complete_relstr(sk10), inference(resolution, [status(thm)], [c44, c206])).
% 121.12/16.54  fof(sdef147, definition, (spl147 <=> (~trivial_carrier(sk10))), introduced(definition, [new_symbols(naming, [spl147])], [avatar_definition])).
% 121.12/16.54  cnf(ssp79, plain, (spl13 | spl14 | spl59 | spl147), inference(avatar_split_clause, [status(thm)], [p655, sdef13, sdef14, sdef59, sdef147])).
% 121.12/16.54  cnf(p657, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~trivial_carrier(sk34) | complete_relstr(sk34), inference(resolution, [status(thm)], [c44, c331])).
% 121.12/16.54  cnf(ssp80, plain, (spl119 | spl120 | spl132 | spl145), inference(avatar_split_clause, [status(thm)], [p657, sdef119, sdef120, sdef132, sdef145])).
% 121.12/16.54  fof(f17, axiom, ! [A] : ( ( topological_space(A) & top_str(A) ) => ! [B] : ( element(B,powerset(the_carrier(A))) => ( empty(B) => nowhere_dense(B,A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc3_tops_1)).
% 121.12/16.54  fof(f17_nnf, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | ! [B] : ((~(element(B,powerset(the_carrier(A)))) | (~(empty(B)) | nowhere_dense(B,A)))))), inference(nnf_transformation, [status(thm)], [f17])).
% 121.12/16.54  fof(f17_sk, plain, ! [A,B] : (((~(topological_space(A)) | ~(top_str(A))) | (~(element(B,powerset(the_carrier(A)))) | (~(empty(B)) | nowhere_dense(B,A))))), inference(skolemisation, [status(esa)], [f17_nnf])).
% 121.12/16.54  cnf(c45, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~empty(X1) | nowhere_dense(X1,X0), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 121.12/16.54  cnf(p660, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | nowhere_dense(X0,sk43), inference(resolution, [status(thm)], [c45, c377])).
% 121.12/16.54  fof(sdef148, definition, (spl148 <=> (~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | nowhere_dense(X0,sk43))), introduced(definition, [new_symbols(naming, [spl148])], [avatar_definition])).
% 121.12/16.54  cnf(ssp81, plain, (spl138 | spl148), inference(avatar_split_clause, [status(thm)], [p660, sdef138, sdef148])).
% 121.12/16.54  fof(f18, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & complete_relstr(A) ) => ( ~ empty_carrier(A) & bounded_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc3_yellow_0)).
% 121.12/16.54  fof(f18_nnf, plain, ! [A] : ((~(rel_str(A)) | ((empty_carrier(A) | ~(complete_relstr(A))) | (~(empty_carrier(A)) & bounded_relstr(A))))), inference(nnf_transformation, [status(thm)], [f18])).
% 121.12/16.54  fof(f18_sk, plain, ! [A] : ((~(rel_str(A)) | ((empty_carrier(A) | ~(complete_relstr(A))) | (~(empty_carrier(A)) & bounded_relstr(A))))), inference(skolemisation, [status(esa)], [f18_nnf])).
% 121.12/16.54  cnf(c47, plain, ~rel_str(X0) | empty_carrier(X0) | ~complete_relstr(X0) | bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 121.12/16.54  cnf(p667, plain, empty_carrier(sk0) | ~complete_relstr(sk0) | bounded_relstr(sk0), inference(resolution, [status(thm)], [c47, c90])).
% 121.12/16.54  cnf(ssp82, plain, (spl6 | spl8 | spl84), inference(avatar_split_clause, [status(thm)], [p667, sdef6, sdef8, sdef84])).
% 121.12/16.54  cnf(p668, plain, empty_carrier(sk10) | ~complete_relstr(sk10) | bounded_relstr(sk10), inference(resolution, [status(thm)], [c47, c206])).
% 121.12/16.54  cnf(ssp83, plain, (spl13 | spl15 | spl85), inference(avatar_split_clause, [status(thm)], [p668, sdef13, sdef15, sdef85])).
% 121.12/16.54  cnf(p669, plain, empty_carrier(sk13) | ~complete_relstr(sk13) | bounded_relstr(sk13), inference(resolution, [status(thm)], [c47, c228])).
% 121.12/16.54  cnf(ssp84, plain, (spl26 | spl28 | spl86), inference(avatar_split_clause, [status(thm)], [p669, sdef26, sdef28, sdef86])).
% 121.12/16.54  cnf(p670, plain, empty_carrier(sk19) | ~complete_relstr(sk19) | bounded_relstr(sk19), inference(resolution, [status(thm)], [c47, c261])).
% 121.12/16.54  cnf(ssp85, plain, (spl71 | spl73 | spl87), inference(avatar_split_clause, [status(thm)], [p670, sdef71, sdef73, sdef87])).
% 121.12/16.54  cnf(p671, plain, empty_carrier(sk20) | ~complete_relstr(sk20) | bounded_relstr(sk20), inference(resolution, [status(thm)], [c47, c271])).
% 121.12/16.54  cnf(ssp86, plain, (spl90 | spl92 | spl103), inference(avatar_split_clause, [status(thm)], [p671, sdef90, sdef92, sdef103])).
% 121.12/16.54  cnf(p672, plain, empty_carrier(sk34) | ~complete_relstr(sk34) | bounded_relstr(sk34), inference(resolution, [status(thm)], [c47, c331])).
% 121.12/16.54  cnf(ssp87, plain, (spl119 | spl121 | spl134), inference(avatar_split_clause, [status(thm)], [p672, sdef119, sdef121, sdef134])).
% 121.12/16.54  fof(f19, axiom, ! [A] : ( ( topological_space(A) & top_str(A) ) => ! [B] : ( element(B,powerset(the_carrier(A))) => ( nowhere_dense(B,A) => boundary_set(B,A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc4_tops_1)).
% 121.12/16.54  fof(f19_nnf, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | ! [B] : ((~(element(B,powerset(the_carrier(A)))) | (~(nowhere_dense(B,A)) | boundary_set(B,A)))))), inference(nnf_transformation, [status(thm)], [f19])).
% 121.12/16.54  fof(f19_sk, plain, ! [A,B] : (((~(topological_space(A)) | ~(top_str(A))) | (~(element(B,powerset(the_carrier(A)))) | (~(nowhere_dense(B,A)) | boundary_set(B,A))))), inference(skolemisation, [status(esa)], [f19_nnf])).
% 121.12/16.54  cnf(c48, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~nowhere_dense(X1,X0) | boundary_set(X1,X0), inference(cnf_transformation, [status(esa)], [f19_sk])).
% 121.12/16.54  cnf(p673, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~nowhere_dense(X0,sk43) | boundary_set(X0,sk43), inference(resolution, [status(thm)], [c48, c377])).
% 121.12/16.54  fof(sdef149, definition, (spl149 <=> (~element(X0,powerset(the_carrier(sk43))) | ~nowhere_dense(X0,sk43) | boundary_set(X0,sk43))), introduced(definition, [new_symbols(naming, [spl149])], [avatar_definition])).
% 121.12/16.54  cnf(ssp88, plain, (spl138 | spl149), inference(avatar_split_clause, [status(thm)], [p673, sdef138, sdef149])).
% 121.12/16.54  fof(f20, axiom, ! [A] : ( rel_str(A) => ( bounded_relstr(A) => ( lower_bounded_relstr(A) & upper_bounded_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc4_yellow_0)).
% 121.12/16.54  fof(f20_nnf, plain, ! [A] : ((~(rel_str(A)) | (~(bounded_relstr(A)) | (lower_bounded_relstr(A) & upper_bounded_relstr(A))))), inference(nnf_transformation, [status(thm)], [f20])).
% 121.12/16.54  fof(f20_sk, plain, ! [A] : ((~(rel_str(A)) | (~(bounded_relstr(A)) | (lower_bounded_relstr(A) & upper_bounded_relstr(A))))), inference(skolemisation, [status(esa)], [f20_nnf])).
% 121.12/16.54  cnf(c49, plain, ~rel_str(X0) | ~bounded_relstr(X0) | lower_bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f20_sk])).
% 121.12/16.54  cnf(p678, plain, ~bounded_relstr(sk0) | lower_bounded_relstr(sk0), inference(resolution, [status(thm)], [c49, c90])).
% 121.12/16.54  cnf(ssp89, plain, (spl21 | spl150), inference(avatar_split_clause, [status(thm)], [p678, sdef21, sdef150])).
% 121.12/16.54  cnf(p680, plain, ~bounded_relstr(sk10) | lower_bounded_relstr(sk10), inference(resolution, [status(thm)], [c49, c206])).
% 121.12/16.54  cnf(ssp90, plain, (spl23 | spl151), inference(avatar_split_clause, [status(thm)], [p680, sdef23, sdef151])).
% 121.12/16.54  cnf(p682, plain, ~bounded_relstr(sk13) | lower_bounded_relstr(sk13), inference(resolution, [status(thm)], [c49, c228])).
% 121.12/16.54  cnf(ssp91, plain, (spl32 | spl152), inference(avatar_split_clause, [status(thm)], [p682, sdef32, sdef152])).
% 121.12/16.54  cnf(p684, plain, ~bounded_relstr(sk19) | lower_bounded_relstr(sk19), inference(resolution, [status(thm)], [c49, c261])).
% 121.12/16.54  cnf(ssp92, plain, (spl77 | spl153), inference(avatar_split_clause, [status(thm)], [p684, sdef77, sdef153])).
% 121.12/16.54  cnf(p686, plain, ~bounded_relstr(sk20) | lower_bounded_relstr(sk20), inference(resolution, [status(thm)], [c49, c271])).
% 121.12/16.54  cnf(ssp93, plain, (spl96 | spl154), inference(avatar_split_clause, [status(thm)], [p686, sdef96, sdef154])).
% 121.12/16.54  cnf(p688, plain, ~bounded_relstr(sk34) | lower_bounded_relstr(sk34), inference(resolution, [status(thm)], [c49, c331])).
% 121.12/16.54  cnf(ssp94, plain, (spl125 | spl155), inference(avatar_split_clause, [status(thm)], [p688, sdef125, sdef155])).
% 121.12/16.54  cnf(c50, plain, ~rel_str(X0) | ~bounded_relstr(X0) | upper_bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f20_sk])).
% 121.12/16.54  cnf(p691, plain, ~bounded_relstr(sk0) | upper_bounded_relstr(sk0), inference(resolution, [status(thm)], [c50, c90])).
% 121.12/16.54  cnf(ssp95, plain, (spl66 | spl150), inference(avatar_split_clause, [status(thm)], [p691, sdef66, sdef150])).
% 121.12/16.54  cnf(p692, plain, ~bounded_relstr(sk10) | upper_bounded_relstr(sk10), inference(resolution, [status(thm)], [c50, c206])).
% 121.12/16.54  cnf(ssp96, plain, (spl67 | spl151), inference(avatar_split_clause, [status(thm)], [p692, sdef67, sdef151])).
% 121.12/16.54  cnf(p693, plain, ~bounded_relstr(sk13) | upper_bounded_relstr(sk13), inference(resolution, [status(thm)], [c50, c228])).
% 121.12/16.54  cnf(ssp97, plain, (spl68 | spl152), inference(avatar_split_clause, [status(thm)], [p693, sdef68, sdef152])).
% 121.12/16.54  cnf(p694, plain, ~bounded_relstr(sk19) | upper_bounded_relstr(sk19), inference(resolution, [status(thm)], [c50, c261])).
% 121.12/16.54  cnf(ssp98, plain, (spl83 | spl153), inference(avatar_split_clause, [status(thm)], [p694, sdef83, sdef153])).
% 121.12/16.54  cnf(p695, plain, ~bounded_relstr(sk20) | upper_bounded_relstr(sk20), inference(resolution, [status(thm)], [c50, c271])).
% 121.12/16.54  cnf(ssp99, plain, (spl102 | spl154), inference(avatar_split_clause, [status(thm)], [p695, sdef102, sdef154])).
% 121.12/16.54  cnf(p696, plain, ~bounded_relstr(sk34) | upper_bounded_relstr(sk34), inference(resolution, [status(thm)], [c50, c331])).
% 121.12/16.54  cnf(ssp100, plain, (spl133 | spl155), inference(avatar_split_clause, [status(thm)], [p696, sdef133, sdef155])).
% 121.12/16.54  fof(f21, axiom, ! [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) ) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc5_tops_1)).
% 121.12/16.54  fof(f21_nnf, plain, ! [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))))))), inference(nnf_transformation, [status(thm)], [f21])).
% 121.12/16.54  fof(f21_sk, plain, ! [A,B] : (((~(topological_space(A)) | ~(top_str(A))) | (~(element(B,powerset(the_carrier(A)))) | ((~(closed_subset(B,A)) | ~(boundary_set(B,A))) | (boundary_set(B,A) & nowhere_dense(B,A)))))), inference(skolemisation, [status(esa)], [f21_nnf])).
% 121.12/16.54  cnf(c52, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~closed_subset(X1,X0) | ~boundary_set(X1,X0) | nowhere_dense(X1,X0), inference(cnf_transformation, [status(esa)], [f21_sk])).
% 121.12/16.54  cnf(p703, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~closed_subset(X0,sk43) | ~boundary_set(X0,sk43) | nowhere_dense(X0,sk43), inference(resolution, [status(thm)], [c52, c377])).
% 121.12/16.54  fof(sdef156, definition, (spl156 <=> (~element(X0,powerset(the_carrier(sk43))) | ~closed_subset(X0,sk43) | ~boundary_set(X0,sk43) | nowhere_dense(X0,sk43))), introduced(definition, [new_symbols(naming, [spl156])], [avatar_definition])).
% 121.12/16.54  cnf(ssp101, plain, (spl138 | spl156), inference(avatar_split_clause, [status(thm)], [p703, sdef138, sdef156])).
% 121.12/16.54  fof(f22, axiom, ! [A] : ( rel_str(A) => ( ( ~ empty_carrier(A) & reflexive_relstr(A) & trivial_carrier(A) ) => ( ~ empty_carrier(A) & reflexive_relstr(A) & connected_relstr(A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc5_waybel_0)).
% 121.12/16.54  fof(f22_nnf, plain, ! [A] : ((~(rel_str(A)) | (((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(trivial_carrier(A))) | ((~(empty_carrier(A)) & reflexive_relstr(A)) & connected_relstr(A))))), inference(nnf_transformation, [status(thm)], [f22])).
% 121.12/16.54  fof(f22_sk, plain, ! [A] : ((~(rel_str(A)) | (((empty_carrier(A) | ~(reflexive_relstr(A))) | ~(trivial_carrier(A))) | ((~(empty_carrier(A)) & reflexive_relstr(A)) & connected_relstr(A))))), inference(skolemisation, [status(esa)], [f22_nnf])).
% 121.12/16.54  cnf(c55, plain, ~rel_str(X0) | empty_carrier(X0) | ~reflexive_relstr(X0) | ~trivial_carrier(X0) | connected_relstr(X0), inference(cnf_transformation, [status(esa)], [f22_sk])).
% 121.12/16.54  cnf(p711, plain, empty_carrier(sk0) | ~reflexive_relstr(sk0) | ~trivial_carrier(sk0) | connected_relstr(sk0), inference(resolution, [status(thm)], [c55, c90])).
% 121.12/16.54  fof(sdef157, definition, (spl157 <=> (connected_relstr(sk0))), introduced(definition, [new_symbols(naming, [spl157])], [avatar_definition])).
% 121.12/16.54  cnf(ssp102, plain, (spl6 | spl7 | spl142 | spl157), inference(avatar_split_clause, [status(thm)], [p711, sdef6, sdef7, sdef142, sdef157])).
% 121.12/16.54  cnf(p713, plain, empty_carrier(sk11) | ~reflexive_relstr(sk11) | ~trivial_carrier(sk11) | connected_relstr(sk11), inference(resolution, [status(thm)], [c55, c212])).
% 121.12/16.54  fof(sdef160, definition, (spl160 <=> (~trivial_carrier(sk11))), introduced(definition, [new_symbols(naming, [spl160])], [avatar_definition])).
% 121.12/16.54  fof(sdef161, definition, (spl161 <=> (connected_relstr(sk11))), introduced(definition, [new_symbols(naming, [spl161])], [avatar_definition])).
% 121.12/16.54  cnf(ssp103, plain, (spl158 | spl159 | spl160 | spl161), inference(avatar_split_clause, [status(thm)], [p713, sdef158, sdef159, sdef160, sdef161])).
% 121.12/16.54  cnf(p718, plain, empty_carrier(sk13) | ~reflexive_relstr(sk13) | ~trivial_carrier(sk13) | connected_relstr(sk13), inference(resolution, [status(thm)], [c55, c228])).
% 121.12/16.54  fof(sdef162, definition, (spl162 <=> (~trivial_carrier(sk13))), introduced(definition, [new_symbols(naming, [spl162])], [avatar_definition])).
% 121.12/16.54  fof(sdef163, definition, (spl163 <=> (connected_relstr(sk13))), introduced(definition, [new_symbols(naming, [spl163])], [avatar_definition])).
% 121.12/16.54  cnf(ssp104, plain, (spl26 | spl27 | spl162 | spl163), inference(avatar_split_clause, [status(thm)], [p718, sdef26, sdef27, sdef162, sdef163])).
% 121.12/16.54  cnf(p721, plain, empty_carrier(sk19) | ~reflexive_relstr(sk19) | ~trivial_carrier(sk19) | connected_relstr(sk19), inference(resolution, [status(thm)], [c55, c261])).
% 121.12/16.54  fof(sdef165, definition, (spl165 <=> (connected_relstr(sk19))), introduced(definition, [new_symbols(naming, [spl165])], [avatar_definition])).
% 121.12/16.54  cnf(ssp105, plain, (spl71 | spl72 | spl164 | spl165), inference(avatar_split_clause, [status(thm)], [p721, sdef71, sdef72, sdef164, sdef165])).
% 121.12/16.54  cnf(p724, plain, empty_carrier(sk20) | ~reflexive_relstr(sk20) | ~trivial_carrier(sk20) | connected_relstr(sk20), inference(resolution, [status(thm)], [c55, c271])).
% 121.12/16.54  fof(sdef166, definition, (spl166 <=> (~trivial_carrier(sk20))), introduced(definition, [new_symbols(naming, [spl166])], [avatar_definition])).
% 121.12/16.54  fof(sdef167, definition, (spl167 <=> (connected_relstr(sk20))), introduced(definition, [new_symbols(naming, [spl167])], [avatar_definition])).
% 121.12/16.54  cnf(ssp106, plain, (spl90 | spl91 | spl166 | spl167), inference(avatar_split_clause, [status(thm)], [p724, sdef90, sdef91, sdef166, sdef167])).
% 121.12/16.54  cnf(p727, plain, empty_carrier(sk26) | ~reflexive_relstr(sk26) | ~trivial_carrier(sk26) | connected_relstr(sk26), inference(resolution, [status(thm)], [c55, c295])).
% 121.12/16.54  fof(sdef168, definition, (spl168 <=> (~trivial_carrier(sk26))), introduced(definition, [new_symbols(naming, [spl168])], [avatar_definition])).
% 121.12/16.54  fof(sdef169, definition, (spl169 <=> (connected_relstr(sk26))), introduced(definition, [new_symbols(naming, [spl169])], [avatar_definition])).
% 121.12/16.54  cnf(ssp107, plain, (spl106 | spl107 | spl168 | spl169), inference(avatar_split_clause, [status(thm)], [p727, sdef106, sdef107, sdef168, sdef169])).
% 121.12/16.54  cnf(p730, plain, empty_carrier(sk34) | ~reflexive_relstr(sk34) | ~trivial_carrier(sk34) | connected_relstr(sk34), inference(resolution, [status(thm)], [c55, c331])).
% 121.12/16.54  fof(sdef170, definition, (spl170 <=> (connected_relstr(sk34))), introduced(definition, [new_symbols(naming, [spl170])], [avatar_definition])).
% 121.12/16.54  cnf(ssp108, plain, (spl119 | spl120 | spl145 | spl170), inference(avatar_split_clause, [status(thm)], [p730, sdef119, sdef120, sdef145, sdef170])).
% 121.12/16.54  fof(f23, axiom, ! [A] : ( rel_str(A) => ( ( lower_bounded_relstr(A) & upper_bounded_relstr(A) ) => bounded_relstr(A) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc5_yellow_0)).
% 121.12/16.54  fof(f23_nnf, plain, ! [A] : ((~(rel_str(A)) | ((~(lower_bounded_relstr(A)) | ~(upper_bounded_relstr(A))) | bounded_relstr(A)))), inference(nnf_transformation, [status(thm)], [f23])).
% 121.12/16.54  fof(f23_sk, plain, ! [A] : ((~(rel_str(A)) | ((~(lower_bounded_relstr(A)) | ~(upper_bounded_relstr(A))) | bounded_relstr(A)))), inference(skolemisation, [status(esa)], [f23_nnf])).
% 121.12/16.54  cnf(c56, plain, ~rel_str(X0) | ~lower_bounded_relstr(X0) | ~upper_bounded_relstr(X0) | bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f23_sk])).
% 121.12/16.54  cnf(p736, plain, ~lower_bounded_relstr(sk0) | ~upper_bounded_relstr(sk0) | bounded_relstr(sk0), inference(resolution, [status(thm)], [c56, c90])).
% 121.12/16.54  cnf(ssp109, plain, (spl43 | spl84 | spl111), inference(avatar_split_clause, [status(thm)], [p736, sdef43, sdef84, sdef111])).
% 121.12/16.54  cnf(p737, plain, ~lower_bounded_relstr(sk10) | ~upper_bounded_relstr(sk10) | bounded_relstr(sk10), inference(resolution, [status(thm)], [c56, c206])).
% 121.12/16.54  cnf(ssp110, plain, (spl49 | spl85 | spl113), inference(avatar_split_clause, [status(thm)], [p737, sdef49, sdef85, sdef113])).
% 121.12/16.54  cnf(p738, plain, ~lower_bounded_relstr(sk13) | ~upper_bounded_relstr(sk13) | bounded_relstr(sk13), inference(resolution, [status(thm)], [c56, c228])).
% 121.12/16.54  cnf(ssp111, plain, (spl55 | spl86 | spl115), inference(avatar_split_clause, [status(thm)], [p738, sdef55, sdef86, sdef115])).
% 121.12/16.54  cnf(p739, plain, ~lower_bounded_relstr(sk19) | ~upper_bounded_relstr(sk19) | bounded_relstr(sk19), inference(resolution, [status(thm)], [c56, c261])).
% 121.12/16.54  cnf(ssp112, plain, (spl81 | spl87 | spl171), inference(avatar_split_clause, [status(thm)], [p739, sdef81, sdef87, sdef171])).
% 121.12/16.54  cnf(p741, plain, ~lower_bounded_relstr(sk20) | ~upper_bounded_relstr(sk20) | bounded_relstr(sk20), inference(resolution, [status(thm)], [c56, c271])).
% 121.12/16.54  cnf(ssp113, plain, (spl100 | spl103 | spl172), inference(avatar_split_clause, [status(thm)], [p741, sdef100, sdef103, sdef172])).
% 121.12/16.54  cnf(p743, plain, ~lower_bounded_relstr(sk34) | ~upper_bounded_relstr(sk34) | bounded_relstr(sk34), inference(resolution, [status(thm)], [c56, c331])).
% 121.12/16.54  cnf(ssp114, plain, (spl129 | spl134 | spl135), inference(avatar_split_clause, [status(thm)], [p743, sdef129, sdef134, sdef135])).
% 121.12/16.54  fof(f24, axiom, ! [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) ) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc6_tops_1)).
% 121.12/16.54  fof(f24_nnf, plain, ! [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))))))), inference(nnf_transformation, [status(thm)], [f24])).
% 121.12/16.54  fof(f24_sk, plain, ! [A,B] : (((~(topological_space(A)) | ~(top_str(A))) | (~(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)))))), inference(skolemisation, [status(esa)], [f24_nnf])).
% 121.12/16.54  cnf(c57, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | empty(X1), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p745, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | empty(X0), inference(resolution, [status(thm)], [c57, c377])).
% 121.12/16.54  fof(sdef173, definition, (spl173 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | empty(X0))), introduced(definition, [new_symbols(naming, [spl173])], [avatar_definition])).
% 121.12/16.54  cnf(ssp115, plain, (spl138 | spl173), inference(avatar_split_clause, [status(thm)], [p745, sdef138, sdef173])).
% 121.12/16.54  cnf(c59, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | closed_subset(X1,X0), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p750, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | closed_subset(X0,sk43), inference(resolution, [status(thm)], [c59, c377])).
% 121.12/16.54  fof(sdef174, definition, (spl174 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | closed_subset(X0,sk43))), introduced(definition, [new_symbols(naming, [spl174])], [avatar_definition])).
% 121.12/16.54  cnf(ssp116, plain, (spl138 | spl174), inference(avatar_split_clause, [status(thm)], [p750, sdef138, sdef174])).
% 121.12/16.54  cnf(c60, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | v1_membered(X1), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p754, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v1_membered(X0), inference(resolution, [status(thm)], [c60, c377])).
% 121.12/16.54  fof(sdef175, definition, (spl175 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v1_membered(X0))), introduced(definition, [new_symbols(naming, [spl175])], [avatar_definition])).
% 121.12/16.54  cnf(ssp117, plain, (spl138 | spl175), inference(avatar_split_clause, [status(thm)], [p754, sdef138, sdef175])).
% 121.12/16.54  cnf(c61, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | v2_membered(X1), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p757, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v2_membered(X0), inference(resolution, [status(thm)], [c61, c377])).
% 121.12/16.54  fof(sdef176, definition, (spl176 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v2_membered(X0))), introduced(definition, [new_symbols(naming, [spl176])], [avatar_definition])).
% 121.12/16.54  cnf(ssp118, plain, (spl138 | spl176), inference(avatar_split_clause, [status(thm)], [p757, sdef138, sdef176])).
% 121.12/16.54  cnf(c62, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | v3_membered(X1), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p762, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v3_membered(X0), inference(resolution, [status(thm)], [c62, c377])).
% 121.12/16.54  fof(sdef177, definition, (spl177 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v3_membered(X0))), introduced(definition, [new_symbols(naming, [spl177])], [avatar_definition])).
% 121.12/16.54  cnf(ssp119, plain, (spl138 | spl177), inference(avatar_split_clause, [status(thm)], [p762, sdef138, sdef177])).
% 121.12/16.54  cnf(c63, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | v4_membered(X1), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p766, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v4_membered(X0), inference(resolution, [status(thm)], [c63, c377])).
% 121.12/16.54  fof(sdef178, definition, (spl178 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v4_membered(X0))), introduced(definition, [new_symbols(naming, [spl178])], [avatar_definition])).
% 121.12/16.54  cnf(ssp120, plain, (spl138 | spl178), inference(avatar_split_clause, [status(thm)], [p766, sdef138, sdef178])).
% 121.12/16.54  cnf(c64, plain, ~topological_space(X0) | ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~open_subset(X1,X0) | ~nowhere_dense(X1,X0) | v5_membered(X1), inference(cnf_transformation, [status(esa)], [f24_sk])).
% 121.12/16.54  cnf(p770, plain, ~top_str(sk43) | ~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v5_membered(X0), inference(resolution, [status(thm)], [c64, c377])).
% 121.12/16.54  fof(sdef179, definition, (spl179 <=> (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v5_membered(X0))), introduced(definition, [new_symbols(naming, [spl179])], [avatar_definition])).
% 121.12/16.54  cnf(ssp121, plain, (spl138 | spl179), inference(avatar_split_clause, [status(thm)], [p770, sdef138, sdef179])).
% 121.12/16.54  fof(f25, axiom, ! [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) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc9_waybel_0)).
% 121.12/16.54  fof(f25_nnf, plain, ! [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))))), inference(nnf_transformation, [status(thm)], [f25])).
% 121.12/16.54  fof(f25_sk, plain, ! [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))))), inference(skolemisation, [status(esa)], [f25_nnf])).
% 121.12/16.54  cnf(c70, plain, ~rel_str(X0) | ~reflexive_relstr(X0) | ~with_suprema_relstr(X0) | ~up_complete_relstr(X0) | upper_bounded_relstr(X0), inference(cnf_transformation, [status(esa)], [f25_sk])).
% 121.12/16.54  cnf(p783, plain, ~reflexive_relstr(sk0) | ~with_suprema_relstr(sk0) | ~up_complete_relstr(sk0) | upper_bounded_relstr(sk0), inference(resolution, [status(thm)], [c70, c90])).
% 121.12/16.54  cnf(ssp122, plain, (spl7 | spl42 | spl44 | spl66), inference(avatar_split_clause, [status(thm)], [p783, sdef7, sdef42, sdef44, sdef66])).
% 121.12/16.54  cnf(p784, plain, ~reflexive_relstr(sk10) | ~with_suprema_relstr(sk10) | ~up_complete_relstr(sk10) | upper_bounded_relstr(sk10), inference(resolution, [status(thm)], [c70, c206])).
% 121.12/16.54  cnf(ssp123, plain, (spl14 | spl48 | spl50 | spl67), inference(avatar_split_clause, [status(thm)], [p784, sdef14, sdef48, sdef50, sdef67])).
% 121.12/16.54  cnf(p785, plain, ~reflexive_relstr(sk13) | ~with_suprema_relstr(sk13) | ~up_complete_relstr(sk13) | upper_bounded_relstr(sk13), inference(resolution, [status(thm)], [c70, c228])).
% 121.12/16.54  cnf(ssp124, plain, (spl27 | spl54 | spl56 | spl68), inference(avatar_split_clause, [status(thm)], [p785, sdef27, sdef54, sdef56, sdef68])).
% 121.12/16.54  cnf(p786, plain, ~reflexive_relstr(sk19) | ~with_suprema_relstr(sk19) | ~up_complete_relstr(sk19) | upper_bounded_relstr(sk19), inference(resolution, [status(thm)], [c70, c261])).
% 121.12/16.54  cnf(ssp125, plain, (spl72 | spl80 | spl82 | spl83), inference(avatar_split_clause, [status(thm)], [p786, sdef72, sdef80, sdef82, sdef83])).
% 121.12/16.54  cnf(p787, plain, ~reflexive_relstr(sk20) | ~with_suprema_relstr(sk20) | ~up_complete_relstr(sk20) | upper_bounded_relstr(sk20), inference(resolution, [status(thm)], [c70, c271])).
% 121.12/16.54  cnf(ssp126, plain, (spl91 | spl99 | spl101 | spl102), inference(avatar_split_clause, [status(thm)], [p787, sdef91, sdef99, sdef101, sdef102])).
% 121.12/16.54  cnf(p788, plain, ~reflexive_relstr(sk34) | ~with_suprema_relstr(sk34) | ~up_complete_relstr(sk34) | upper_bounded_relstr(sk34), inference(resolution, [status(thm)], [c70, c331])).
% 121.12/16.54  cnf(ssp127, plain, (spl120 | spl128 | spl130 | spl133), inference(avatar_split_clause, [status(thm)], [p788, sdef120, sdef128, sdef130, sdef133])).
% 121.12/16.54  fof(f26, axiom, ! [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) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_yellow19)).
% 121.12/16.54  fof(f26_nnf, plain, ! [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))))), inference(nnf_transformation, [status(thm)], [f26])).
% 121.12/16.54  fof(f26_sk, plain, ! [A,B] : ((((empty_carrier(A) | ~(topological_space(A))) | ~(top_str(A))) | (~(element(B,the_carrier(A))) | neighborhood_system(A,B) = a_2_0_yellow19(A,B)))), inference(skolemisation, [status(esa)], [f26_nnf])).
% 121.12/16.54  cnf(c71, plain, empty_carrier(X0) | ~topological_space(X0) | ~top_str(X0) | ~element(X1,the_carrier(X0)) | neighborhood_system(X0,X1) = a_2_0_yellow19(X0,X1), inference(cnf_transformation, [status(esa)], [f26_sk])).
% 121.12/16.54  cnf(p792, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | neighborhood_system(sk43,X0) = a_2_0_yellow19(sk43,X0), inference(resolution, [status(thm)], [c71, c377])).
% 121.12/16.54  fof(sdef181, definition, (spl181 <=> (~element(X0,the_carrier(sk43)) | neighborhood_system(sk43,X0) = a_2_0_yellow19(sk43,X0))), introduced(definition, [new_symbols(naming, [spl181])], [avatar_definition])).
% 121.12/16.54  cnf(ssp128, plain, (spl138 | spl180 | spl181), inference(avatar_split_clause, [status(thm)], [p792, sdef138, sdef180, sdef181])).
% 121.12/16.54  fof(f29, axiom, ! [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))))) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k1_yellow19)).
% 121.12/16.54  fof(f29_nnf, plain, ! [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))))))), inference(nnf_transformation, [status(thm)], [f29])).
% 121.12/16.54  fof(f29_sk, plain, ! [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))))))), inference(skolemisation, [status(esa)], [f29_nnf])).
% 121.12/16.54  cnf(c75, plain, 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))))), inference(cnf_transformation, [status(esa)], [f29_sk])).
% 121.12/16.54  cnf(p797, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | element(neighborhood_system(sk43,X0),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sk43))))), inference(resolution, [status(thm)], [c75, c377])).
% 121.12/16.54  fof(sdef182, definition, (spl182 <=> (~element(X0,the_carrier(sk43)) | element(neighborhood_system(sk43,X0),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sk43))))))), introduced(definition, [new_symbols(naming, [spl182])], [avatar_definition])).
% 121.12/16.54  cnf(ssp129, plain, (spl138 | spl180 | spl182), inference(avatar_split_clause, [status(thm)], [p797, sdef138, sdef180, sdef182])).
% 121.12/16.54  fof(f35, axiom, ! [A] : ( top_str(A) => one_sorted_str(A) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_l1_pre_topc)).
% 121.12/16.54  fof(f35_nnf, plain, ! [A] : ((~(top_str(A)) | one_sorted_str(A))), inference(nnf_transformation, [status(thm)], [f35])).
% 121.12/16.54  fof(f35_sk, plain, ! [A] : ((~(top_str(A)) | one_sorted_str(A))), inference(skolemisation, [status(esa)], [f35_nnf])).
% 121.12/16.54  cnf(c82, plain, ~top_str(X0) | one_sorted_str(X0), inference(cnf_transformation, [status(esa)], [f35_sk])).
% 121.12/16.54  cnf(p817, plain, one_sorted_str(sk43), inference(resolution, [status(thm)], [c82, c378])).
% 121.12/16.54  fof(f31, axiom, ! [A] : ( one_sorted_str(A) => element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k2_pre_topc)).
% 121.12/16.54  fof(f31_nnf, plain, ! [A] : ((~(one_sorted_str(A)) | element(cast_as_carrier_subset(A),powerset(the_carrier(A))))), inference(nnf_transformation, [status(thm)], [f31])).
% 121.12/16.54  fof(f31_sk, plain, ! [A] : ((~(one_sorted_str(A)) | element(cast_as_carrier_subset(A),powerset(the_carrier(A))))), inference(skolemisation, [status(esa)], [f31_nnf])).
% 121.12/16.54  cnf(c77, plain, ~one_sorted_str(X0) | element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))), inference(cnf_transformation, [status(esa)], [f31_sk])).
% 121.12/16.54  cnf(p818, plain, element(cast_as_carrier_subset(sk43),powerset(the_carrier(sk43))), inference(resolution, [status(thm)], [p817, c77])).
% 121.12/16.54  cnf(p602, plain, (~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | open_subset(X0,sk43) | ~spl139), inference(avatar_component_clause, [status(thm)], [sdef139])).
% 121.12/16.54  cnf(p819, plain, (~empty(cast_as_carrier_subset(sk43)) | open_subset(cast_as_carrier_subset(sk43),sk43) | ~spl139), inference(resolution, [status(thm)], [p818, p602])).
% 121.12/16.54  cnf(ssp130, plain, (~spl139 | spl183 | spl184), inference(avatar_split_clause, [status(thm)], [p819, sdef183, sdef184])).
% 121.12/16.54  cnf(p607, plain, (~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | closed_subset(X0,sk43) | ~spl140), inference(avatar_component_clause, [status(thm)], [sdef140])).
% 121.12/16.54  cnf(p822, plain, (~empty(cast_as_carrier_subset(sk43)) | closed_subset(cast_as_carrier_subset(sk43),sk43) | ~spl140), inference(resolution, [status(thm)], [p818, p607])).
% 121.12/16.54  cnf(ssp131, plain, (~spl140 | spl183 | spl185), inference(avatar_split_clause, [status(thm)], [p822, sdef183, sdef185])).
% 121.12/16.54  fof(f15, axiom, ! [A] : ( top_str(A) => ! [B] : ( element(B,powerset(the_carrier(A))) => ( empty(B) => boundary_set(B,A) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_tops_1)).
% 121.12/16.54  fof(f15_nnf, plain, ! [A] : ((~(top_str(A)) | ! [B] : ((~(element(B,powerset(the_carrier(A)))) | (~(empty(B)) | boundary_set(B,A)))))), inference(nnf_transformation, [status(thm)], [f15])).
% 121.12/16.54  fof(f15_sk, plain, ! [A,B] : ((~(top_str(A)) | (~(element(B,powerset(the_carrier(A)))) | (~(empty(B)) | boundary_set(B,A))))), inference(skolemisation, [status(esa)], [f15_nnf])).
% 121.12/16.54  cnf(c39, plain, ~top_str(X0) | ~element(X1,powerset(the_carrier(X0))) | ~empty(X1) | boundary_set(X1,X0), inference(cnf_transformation, [status(esa)], [f15_sk])).
% 121.12/16.54  cnf(p631, plain, ~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | boundary_set(X0,sk43), inference(resolution, [status(thm)], [c39, c378])).
% 121.12/16.54  cnf(p824, plain, ~empty(cast_as_carrier_subset(sk43)) | boundary_set(cast_as_carrier_subset(sk43),sk43), inference(resolution, [status(thm)], [p818, p631])).
% 121.12/16.54  cnf(ssp132, plain, (spl183 | spl186), inference(avatar_split_clause, [status(thm)], [p824, sdef183, sdef186])).
% 121.12/16.54  cnf(p661, plain, (~element(X0,powerset(the_carrier(sk43))) | ~empty(X0) | nowhere_dense(X0,sk43) | ~spl148), inference(avatar_component_clause, [status(thm)], [sdef148])).
% 121.12/16.54  cnf(p826, plain, (~empty(cast_as_carrier_subset(sk43)) | nowhere_dense(cast_as_carrier_subset(sk43),sk43) | ~spl148), inference(resolution, [status(thm)], [p818, p661])).
% 121.12/16.54  cnf(ssp133, plain, (~spl148 | spl183 | spl187), inference(avatar_split_clause, [status(thm)], [p826, sdef183, sdef187])).
% 121.12/16.54  cnf(p674, plain, (~element(X0,powerset(the_carrier(sk43))) | ~nowhere_dense(X0,sk43) | boundary_set(X0,sk43) | ~spl149), inference(avatar_component_clause, [status(thm)], [sdef149])).
% 121.12/16.54  cnf(p828, plain, (~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | boundary_set(cast_as_carrier_subset(sk43),sk43) | ~spl149), inference(resolution, [status(thm)], [p818, p674])).
% 121.12/16.54  cnf(ssp134, plain, (~spl149 | spl186 | spl188), inference(avatar_split_clause, [status(thm)], [p828, sdef186, sdef188])).
% 121.12/16.54  cnf(p704, plain, (~element(X0,powerset(the_carrier(sk43))) | ~closed_subset(X0,sk43) | ~boundary_set(X0,sk43) | nowhere_dense(X0,sk43) | ~spl156), inference(avatar_component_clause, [status(thm)], [sdef156])).
% 121.12/16.54  cnf(p830, plain, (~closed_subset(cast_as_carrier_subset(sk43),sk43) | ~boundary_set(cast_as_carrier_subset(sk43),sk43) | nowhere_dense(cast_as_carrier_subset(sk43),sk43) | ~spl156), inference(resolution, [status(thm)], [p818, p704])).
% 121.12/16.54  cnf(ssp135, plain, (~spl156 | spl187 | spl189 | spl190), inference(avatar_split_clause, [status(thm)], [p830, sdef187, sdef189, sdef190])).
% 121.12/16.54  cnf(p746, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | empty(X0) | ~spl173), inference(avatar_component_clause, [status(thm)], [sdef173])).
% 121.12/16.54  cnf(p833, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | empty(cast_as_carrier_subset(sk43)) | ~spl173), inference(resolution, [status(thm)], [p818, p746])).
% 121.12/16.54  cnf(ssp136, plain, (~spl173 | spl188 | spl191 | spl192), inference(avatar_split_clause, [status(thm)], [p833, sdef188, sdef191, sdef192])).
% 121.12/16.54  cnf(p751, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | closed_subset(X0,sk43) | ~spl174), inference(avatar_component_clause, [status(thm)], [sdef174])).
% 121.12/16.54  cnf(p836, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | closed_subset(cast_as_carrier_subset(sk43),sk43) | ~spl174), inference(resolution, [status(thm)], [p818, p751])).
% 121.12/16.54  cnf(ssp137, plain, (~spl174 | spl185 | spl188 | spl191), inference(avatar_split_clause, [status(thm)], [p836, sdef185, sdef188, sdef191])).
% 121.12/16.54  cnf(p755, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v1_membered(X0) | ~spl175), inference(avatar_component_clause, [status(thm)], [sdef175])).
% 121.12/16.54  cnf(p837, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | v1_membered(cast_as_carrier_subset(sk43)) | ~spl175), inference(resolution, [status(thm)], [p818, p755])).
% 121.12/16.54  fof(sdef193, definition, (spl193 <=> (v1_membered(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl193])], [avatar_definition])).
% 121.12/16.54  cnf(ssp138, plain, (~spl175 | spl188 | spl191 | spl193), inference(avatar_split_clause, [status(thm)], [p837, sdef188, sdef191, sdef193])).
% 121.12/16.54  cnf(p758, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v2_membered(X0) | ~spl176), inference(avatar_component_clause, [status(thm)], [sdef176])).
% 121.12/16.54  cnf(p839, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | v2_membered(cast_as_carrier_subset(sk43)) | ~spl176), inference(resolution, [status(thm)], [p818, p758])).
% 121.12/16.54  fof(sdef194, definition, (spl194 <=> (v2_membered(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl194])], [avatar_definition])).
% 121.12/16.54  cnf(ssp139, plain, (~spl176 | spl188 | spl191 | spl194), inference(avatar_split_clause, [status(thm)], [p839, sdef188, sdef191, sdef194])).
% 121.12/16.54  cnf(p763, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v3_membered(X0) | ~spl177), inference(avatar_component_clause, [status(thm)], [sdef177])).
% 121.12/16.54  cnf(p841, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | v3_membered(cast_as_carrier_subset(sk43)) | ~spl177), inference(resolution, [status(thm)], [p818, p763])).
% 121.12/16.54  fof(sdef195, definition, (spl195 <=> (v3_membered(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl195])], [avatar_definition])).
% 121.12/16.54  cnf(ssp140, plain, (~spl177 | spl188 | spl191 | spl195), inference(avatar_split_clause, [status(thm)], [p841, sdef188, sdef191, sdef195])).
% 121.12/16.54  cnf(p767, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v4_membered(X0) | ~spl178), inference(avatar_component_clause, [status(thm)], [sdef178])).
% 121.12/16.54  cnf(p843, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | v4_membered(cast_as_carrier_subset(sk43)) | ~spl178), inference(resolution, [status(thm)], [p818, p767])).
% 121.12/16.54  fof(sdef196, definition, (spl196 <=> (v4_membered(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl196])], [avatar_definition])).
% 121.12/16.54  cnf(ssp141, plain, (~spl178 | spl188 | spl191 | spl196), inference(avatar_split_clause, [status(thm)], [p843, sdef188, sdef191, sdef196])).
% 121.12/16.54  cnf(p771, plain, (~element(X0,powerset(the_carrier(sk43))) | ~open_subset(X0,sk43) | ~nowhere_dense(X0,sk43) | v5_membered(X0) | ~spl179), inference(avatar_component_clause, [status(thm)], [sdef179])).
% 121.12/16.54  cnf(p845, plain, (~open_subset(cast_as_carrier_subset(sk43),sk43) | ~nowhere_dense(cast_as_carrier_subset(sk43),sk43) | v5_membered(cast_as_carrier_subset(sk43)) | ~spl179), inference(resolution, [status(thm)], [p818, p771])).
% 121.12/16.54  fof(sdef197, definition, (spl197 <=> (v5_membered(cast_as_carrier_subset(sk43)))), introduced(definition, [new_symbols(naming, [spl197])], [avatar_definition])).
% 121.12/16.54  cnf(ssp142, plain, (~spl179 | spl188 | spl191 | spl197), inference(avatar_split_clause, [status(thm)], [p845, sdef188, sdef191, sdef197])).
% 121.12/16.54  fof(f37, axiom, ! [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))) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_m1_connsp_2)).
% 121.12/16.54  fof(f37_nnf, plain, ! [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))))))), inference(nnf_transformation, [status(thm)], [f37])).
% 121.12/16.54  fof(f37_sk, plain, ! [A,B,C] : (((((empty_carrier(A) | ~(topological_space(A))) | ~(top_str(A))) | ~(element(B,the_carrier(A)))) | (~(point_neighbourhood(C,A,B)) | element(C,powerset(the_carrier(A)))))), inference(skolemisation, [status(esa)], [f37_nnf])).
% 121.12/16.54  cnf(c84, plain, 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))), inference(cnf_transformation, [status(esa)], [f37_sk])).
% 121.12/16.54  cnf(p850, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | ~point_neighbourhood(X1,sk43,X0) | element(X1,powerset(the_carrier(sk43))), inference(resolution, [status(thm)], [c84, c377])).
% 121.12/16.54  fof(sdef198, definition, (spl198 <=> (~element(X0,the_carrier(sk43)) | ~point_neighbourhood(X1,sk43,X0) | element(X1,powerset(the_carrier(sk43))))), introduced(definition, [new_symbols(naming, [spl198])], [avatar_definition])).
% 121.12/16.54  cnf(ssp143, plain, (spl138 | spl180 | spl198), inference(avatar_split_clause, [status(thm)], [p850, sdef138, sdef180, sdef198])).
% 121.12/16.54  fof(f46, axiom, ! [A,B] : ( ( ~ empty_carrier(A) & topological_space(A) & top_str(A) & element(B,the_carrier(A)) ) => ? [C] : point_neighbourhood(C,A,B) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', existence_m1_connsp_2)).
% 121.12/16.54  fof(f46_nnf, plain, ! [A,B] : (((((empty_carrier(A) | ~(topological_space(A))) | ~(top_str(A))) | ~(element(B,the_carrier(A)))) | ? [C] : (point_neighbourhood(C,A,B)))), inference(nnf_transformation, [status(thm)], [f46])).
% 121.12/16.54  fof(f46_sk, plain, ! [A,B] : (((((empty_carrier(A) | ~(topological_space(A))) | ~(top_str(A))) | ~(element(B,the_carrier(A)))) | point_neighbourhood(sk3(A,B),A,B))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk3])], [f46_nnf])).
% 121.12/16.54  cnf(c93, plain, empty_carrier(X0) | ~topological_space(X0) | ~top_str(X0) | ~element(X1,the_carrier(X0)) | point_neighbourhood(sk3(X0,X1),X0,X1), inference(cnf_transformation, [status(esa)], [f46_sk])).
% 121.12/16.54  cnf(p865, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | point_neighbourhood(sk3(sk43,X0),sk43,X0), inference(resolution, [status(thm)], [c93, c377])).
% 121.12/16.54  fof(sdef199, definition, (spl199 <=> (~element(X0,the_carrier(sk43)) | point_neighbourhood(sk3(sk43,X0),sk43,X0))), introduced(definition, [new_symbols(naming, [spl199])], [avatar_definition])).
% 121.12/16.54  cnf(ssp144, plain, (spl138 | spl180 | spl199), inference(avatar_split_clause, [status(thm)], [p865, sdef138, sdef180, sdef199])).
% 121.12/16.54  cnf(p851, plain, (~element(X0,the_carrier(sk43)) | ~point_neighbourhood(X1,sk43,X0) | element(X1,powerset(the_carrier(sk43))) | ~spl198), inference(avatar_component_clause, [status(thm)], [sdef198])).
% 121.12/16.54  cnf(c379, plain, element(sk44,the_carrier(sk43)), inference(cnf_transformation, [status(esa)], [f113_sk])).
% 121.12/16.54  cnf(p869, plain, (~point_neighbourhood(X0,sk43,sk44) | element(X0,powerset(the_carrier(sk43))) | ~spl198), inference(resolution, [status(thm)], [p851, c379])).
% 121.12/16.54  cnf(p866, plain, (~element(X0,the_carrier(sk43)) | point_neighbourhood(sk3(sk43,X0),sk43,X0) | ~spl199), inference(avatar_component_clause, [status(thm)], [sdef199])).
% 121.12/16.54  cnf(p868, plain, (point_neighbourhood(sk3(sk43,sk44),sk43,sk44) | ~spl199), inference(resolution, [status(thm)], [p866, c379])).
% 121.12/16.54  cnf(p872, plain, (element(sk3(sk43,sk44),powerset(the_carrier(sk43))) | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p869, p868])).
% 121.12/16.54  cnf(p873, plain, (~empty(sk3(sk43,sk44)) | open_subset(sk3(sk43,sk44),sk43) | ~spl139 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p602])).
% 121.12/16.54  cnf(ssp145, plain, (~spl139 | ~spl198 | ~spl199 | spl200 | spl201), inference(avatar_split_clause, [status(thm)], [p873, sdef200, sdef201])).
% 121.12/16.54  cnf(p876, plain, (~empty(sk3(sk43,sk44)) | closed_subset(sk3(sk43,sk44),sk43) | ~spl140 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p607])).
% 121.12/16.54  cnf(ssp146, plain, (~spl140 | ~spl198 | ~spl199 | spl200 | spl202), inference(avatar_split_clause, [status(thm)], [p876, sdef200, sdef202])).
% 121.12/16.54  cnf(p878, plain, (~empty(sk3(sk43,sk44)) | boundary_set(sk3(sk43,sk44),sk43) | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p631])).
% 121.12/16.54  cnf(ssp147, plain, (~spl198 | ~spl199 | spl200 | spl203), inference(avatar_split_clause, [status(thm)], [p878, sdef200, sdef203])).
% 121.12/16.54  cnf(p880, plain, (~empty(sk3(sk43,sk44)) | nowhere_dense(sk3(sk43,sk44),sk43) | ~spl148 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p661])).
% 121.12/16.54  cnf(ssp148, plain, (~spl148 | ~spl198 | ~spl199 | spl200 | spl204), inference(avatar_split_clause, [status(thm)], [p880, sdef200, sdef204])).
% 121.12/16.54  cnf(p882, plain, (~nowhere_dense(sk3(sk43,sk44),sk43) | boundary_set(sk3(sk43,sk44),sk43) | ~spl149 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p674])).
% 121.12/16.54  cnf(ssp149, plain, (~spl149 | ~spl198 | ~spl199 | spl203 | spl205), inference(avatar_split_clause, [status(thm)], [p882, sdef203, sdef205])).
% 121.12/16.54  cnf(p884, plain, (~closed_subset(sk3(sk43,sk44),sk43) | ~boundary_set(sk3(sk43,sk44),sk43) | nowhere_dense(sk3(sk43,sk44),sk43) | ~spl156 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p704])).
% 121.12/16.54  cnf(ssp150, plain, (~spl156 | ~spl198 | ~spl199 | spl204 | spl206 | spl207), inference(avatar_split_clause, [status(thm)], [p884, sdef204, sdef206, sdef207])).
% 121.12/16.54  cnf(p887, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | empty(sk3(sk43,sk44)) | ~spl173 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p746])).
% 121.12/16.54  cnf(ssp151, plain, (~spl173 | ~spl198 | ~spl199 | spl205 | spl208 | spl209), inference(avatar_split_clause, [status(thm)], [p887, sdef205, sdef208, sdef209])).
% 121.12/16.54  cnf(p890, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | closed_subset(sk3(sk43,sk44),sk43) | ~spl174 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p751])).
% 121.12/16.54  cnf(ssp152, plain, (~spl174 | ~spl198 | ~spl199 | spl202 | spl205 | spl208), inference(avatar_split_clause, [status(thm)], [p890, sdef202, sdef205, sdef208])).
% 121.12/16.54  cnf(p891, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | v1_membered(sk3(sk43,sk44)) | ~spl175 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p755])).
% 121.12/16.54  fof(sdef210, definition, (spl210 <=> (v1_membered(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl210])], [avatar_definition])).
% 121.12/16.54  cnf(ssp153, plain, (~spl175 | ~spl198 | ~spl199 | spl205 | spl208 | spl210), inference(avatar_split_clause, [status(thm)], [p891, sdef205, sdef208, sdef210])).
% 121.12/16.54  cnf(p893, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | v2_membered(sk3(sk43,sk44)) | ~spl176 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p758])).
% 121.12/16.54  fof(sdef211, definition, (spl211 <=> (v2_membered(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl211])], [avatar_definition])).
% 121.12/16.54  cnf(ssp154, plain, (~spl176 | ~spl198 | ~spl199 | spl205 | spl208 | spl211), inference(avatar_split_clause, [status(thm)], [p893, sdef205, sdef208, sdef211])).
% 121.12/16.54  cnf(p895, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | v3_membered(sk3(sk43,sk44)) | ~spl177 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p763])).
% 121.12/16.54  fof(sdef212, definition, (spl212 <=> (v3_membered(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl212])], [avatar_definition])).
% 121.12/16.54  cnf(ssp155, plain, (~spl177 | ~spl198 | ~spl199 | spl205 | spl208 | spl212), inference(avatar_split_clause, [status(thm)], [p895, sdef205, sdef208, sdef212])).
% 121.12/16.54  cnf(p897, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | v4_membered(sk3(sk43,sk44)) | ~spl178 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p767])).
% 121.12/16.54  fof(sdef213, definition, (spl213 <=> (v4_membered(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl213])], [avatar_definition])).
% 121.12/16.54  cnf(ssp156, plain, (~spl178 | ~spl198 | ~spl199 | spl205 | spl208 | spl213), inference(avatar_split_clause, [status(thm)], [p897, sdef205, sdef208, sdef213])).
% 121.12/16.54  cnf(p899, plain, (~open_subset(sk3(sk43,sk44),sk43) | ~nowhere_dense(sk3(sk43,sk44),sk43) | v5_membered(sk3(sk43,sk44)) | ~spl179 | ~spl198 | ~spl199), inference(resolution, [status(thm)], [p872, p771])).
% 121.12/16.54  fof(sdef214, definition, (spl214 <=> (v5_membered(sk3(sk43,sk44)))), introduced(definition, [new_symbols(naming, [spl214])], [avatar_definition])).
% 121.12/16.54  cnf(ssp157, plain, (~spl179 | ~spl198 | ~spl199 | spl205 | spl208 | spl214), inference(avatar_split_clause, [status(thm)], [p899, sdef205, sdef208, sdef214])).
% 121.12/16.54  fof(f48, axiom, ! [A] : ? [B] : element(B,A), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', existence_m1_subset_1)).
% 121.12/16.54  fof(f48_nnf, plain, ! [A] : (? [B] : (element(B,A))), inference(nnf_transformation, [status(thm)], [f48])).
% 121.12/16.54  fof(f48_sk, plain, ! [A] : (element(sk5(A),A)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk5])], [f48_nnf])).
% 121.12/16.54  cnf(c95, plain, element(sk5(X0),X0), inference(cnf_transformation, [status(esa)], [f48_sk])).
% 121.12/16.54  cnf(p905, plain, (~empty(sk5(powerset(the_carrier(sk43)))) | open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl139), inference(resolution, [status(thm)], [c95, p602])).
% 121.12/16.54  cnf(ssp158, plain, (~spl139 | spl215 | spl216), inference(avatar_split_clause, [status(thm)], [p905, sdef215, sdef216])).
% 121.12/16.54  cnf(p908, plain, (~empty(sk5(powerset(the_carrier(sk43)))) | closed_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl140), inference(resolution, [status(thm)], [c95, p607])).
% 121.12/16.54  cnf(ssp159, plain, (~spl140 | spl215 | spl217), inference(avatar_split_clause, [status(thm)], [p908, sdef215, sdef217])).
% 121.12/16.54  cnf(p910, plain, ~empty(sk5(powerset(the_carrier(sk43)))) | boundary_set(sk5(powerset(the_carrier(sk43))),sk43), inference(resolution, [status(thm)], [c95, p631])).
% 121.12/16.54  cnf(ssp160, plain, (spl215 | spl218), inference(avatar_split_clause, [status(thm)], [p910, sdef215, sdef218])).
% 121.12/16.54  cnf(p912, plain, (~empty(sk5(powerset(the_carrier(sk43)))) | nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | ~spl148), inference(resolution, [status(thm)], [c95, p661])).
% 121.12/16.54  cnf(ssp161, plain, (~spl148 | spl215 | spl219), inference(avatar_split_clause, [status(thm)], [p912, sdef215, sdef219])).
% 121.12/16.54  cnf(p914, plain, (~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | boundary_set(sk5(powerset(the_carrier(sk43))),sk43) | ~spl149), inference(resolution, [status(thm)], [c95, p674])).
% 121.12/16.54  cnf(ssp162, plain, (~spl149 | spl218 | spl220), inference(avatar_split_clause, [status(thm)], [p914, sdef218, sdef220])).
% 121.12/16.54  cnf(p916, plain, (~closed_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~boundary_set(sk5(powerset(the_carrier(sk43))),sk43) | nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | ~spl156), inference(resolution, [status(thm)], [c95, p704])).
% 121.12/16.54  cnf(ssp163, plain, (~spl156 | spl219 | spl221 | spl222), inference(avatar_split_clause, [status(thm)], [p916, sdef219, sdef221, sdef222])).
% 121.12/16.54  cnf(p919, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | empty(sk5(powerset(the_carrier(sk43)))) | ~spl173), inference(resolution, [status(thm)], [c95, p746])).
% 121.12/16.54  cnf(ssp164, plain, (~spl173 | spl220 | spl223 | spl224), inference(avatar_split_clause, [status(thm)], [p919, sdef220, sdef223, sdef224])).
% 121.12/16.54  cnf(p922, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | closed_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~spl174), inference(resolution, [status(thm)], [c95, p751])).
% 121.12/16.54  cnf(ssp165, plain, (~spl174 | spl217 | spl220 | spl223), inference(avatar_split_clause, [status(thm)], [p922, sdef217, sdef220, sdef223])).
% 121.12/16.54  cnf(p923, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | v1_membered(sk5(powerset(the_carrier(sk43)))) | ~spl175), inference(resolution, [status(thm)], [c95, p755])).
% 121.12/16.54  fof(sdef225, definition, (spl225 <=> (v1_membered(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl225])], [avatar_definition])).
% 121.12/16.54  cnf(ssp166, plain, (~spl175 | spl220 | spl223 | spl225), inference(avatar_split_clause, [status(thm)], [p923, sdef220, sdef223, sdef225])).
% 121.12/16.54  cnf(p925, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | v2_membered(sk5(powerset(the_carrier(sk43)))) | ~spl176), inference(resolution, [status(thm)], [c95, p758])).
% 121.12/16.54  fof(sdef226, definition, (spl226 <=> (v2_membered(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl226])], [avatar_definition])).
% 121.12/16.54  cnf(ssp167, plain, (~spl176 | spl220 | spl223 | spl226), inference(avatar_split_clause, [status(thm)], [p925, sdef220, sdef223, sdef226])).
% 121.12/16.54  cnf(p927, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | v3_membered(sk5(powerset(the_carrier(sk43)))) | ~spl177), inference(resolution, [status(thm)], [c95, p763])).
% 121.12/16.54  fof(sdef227, definition, (spl227 <=> (v3_membered(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl227])], [avatar_definition])).
% 121.12/16.54  cnf(ssp168, plain, (~spl177 | spl220 | spl223 | spl227), inference(avatar_split_clause, [status(thm)], [p927, sdef220, sdef223, sdef227])).
% 121.12/16.54  cnf(p929, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | v4_membered(sk5(powerset(the_carrier(sk43)))) | ~spl178), inference(resolution, [status(thm)], [c95, p767])).
% 121.12/16.54  fof(sdef228, definition, (spl228 <=> (v4_membered(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl228])], [avatar_definition])).
% 121.12/16.54  cnf(ssp169, plain, (~spl178 | spl220 | spl223 | spl228), inference(avatar_split_clause, [status(thm)], [p929, sdef220, sdef223, sdef228])).
% 121.12/16.54  cnf(p931, plain, (~open_subset(sk5(powerset(the_carrier(sk43))),sk43) | ~nowhere_dense(sk5(powerset(the_carrier(sk43))),sk43) | v5_membered(sk5(powerset(the_carrier(sk43)))) | ~spl179), inference(resolution, [status(thm)], [c95, p771])).
% 121.12/16.54  fof(sdef229, definition, (spl229 <=> (v5_membered(sk5(powerset(the_carrier(sk43)))))), introduced(definition, [new_symbols(naming, [spl229])], [avatar_definition])).
% 121.12/16.54  cnf(ssp170, plain, (~spl179 | spl220 | spl223 | spl229), inference(avatar_split_clause, [status(thm)], [p931, sdef220, sdef223, sdef229])).
% 121.12/16.54  fof(f52, axiom, ! [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) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc15_waybel_0)).
% 121.12/16.54  fof(f52_nnf, plain, ! [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)))), inference(nnf_transformation, [status(thm)], [f52])).
% 121.12/16.54  fof(f52_sk, plain, ! [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)))), inference(skolemisation, [status(esa)], [f52_nnf])).
% 121.12/16.54  cnf(c101, plain, empty_carrier(X0) | ~rel_str(X0) | ~empty(cast_as_carrier_subset(X0)), inference(cnf_transformation, [status(esa)], [f52_sk])).
% 121.12/16.54  cnf(p945, plain, empty_carrier(sk0) | ~empty(cast_as_carrier_subset(sk0)), inference(resolution, [status(thm)], [c101, c90])).
% 121.12/16.54  fof(sdef230, definition, (spl230 <=> (~empty(cast_as_carrier_subset(sk0)))), introduced(definition, [new_symbols(naming, [spl230])], [avatar_definition])).
% 121.12/16.54  cnf(ssp171, plain, (spl6 | spl230), inference(avatar_split_clause, [status(thm)], [p945, sdef6, sdef230])).
% 121.12/16.54  cnf(p947, plain, empty_carrier(sk10) | ~empty(cast_as_carrier_subset(sk10)), inference(resolution, [status(thm)], [c101, c206])).
% 121.12/16.54  fof(sdef231, definition, (spl231 <=> (~empty(cast_as_carrier_subset(sk10)))), introduced(definition, [new_symbols(naming, [spl231])], [avatar_definition])).
% 121.12/16.54  cnf(ssp172, plain, (spl13 | spl231), inference(avatar_split_clause, [status(thm)], [p947, sdef13, sdef231])).
% 121.12/16.54  cnf(p949, plain, empty_carrier(sk11) | ~empty(cast_as_carrier_subset(sk11)), inference(resolution, [status(thm)], [c101, c212])).
% 121.12/16.54  fof(sdef232, definition, (spl232 <=> (~empty(cast_as_carrier_subset(sk11)))), introduced(definition, [new_symbols(naming, [spl232])], [avatar_definition])).
% 121.12/16.54  cnf(ssp173, plain, (spl158 | spl232), inference(avatar_split_clause, [status(thm)], [p949, sdef158, sdef232])).
% 121.12/16.54  cnf(p951, plain, empty_carrier(sk13) | ~empty(cast_as_carrier_subset(sk13)), inference(resolution, [status(thm)], [c101, c228])).
% 121.12/16.54  fof(sdef233, definition, (spl233 <=> (~empty(cast_as_carrier_subset(sk13)))), introduced(definition, [new_symbols(naming, [spl233])], [avatar_definition])).
% 121.12/16.54  cnf(ssp174, plain, (spl26 | spl233), inference(avatar_split_clause, [status(thm)], [p951, sdef26, sdef233])).
% 121.12/16.54  cnf(p953, plain, empty_carrier(sk18) | ~empty(cast_as_carrier_subset(sk18)), inference(resolution, [status(thm)], [c101, c244])).
% 121.12/16.54  fof(sdef234, definition, (spl234 <=> (~empty(cast_as_carrier_subset(sk18)))), introduced(definition, [new_symbols(naming, [spl234])], [avatar_definition])).
% 121.12/16.54  cnf(ssp175, plain, (spl35 | spl234), inference(avatar_split_clause, [status(thm)], [p953, sdef35, sdef234])).
% 121.12/16.54  cnf(p955, plain, empty_carrier(sk19) | ~empty(cast_as_carrier_subset(sk19)), inference(resolution, [status(thm)], [c101, c261])).
% 121.12/16.54  fof(sdef235, definition, (spl235 <=> (~empty(cast_as_carrier_subset(sk19)))), introduced(definition, [new_symbols(naming, [spl235])], [avatar_definition])).
% 121.12/16.54  cnf(ssp176, plain, (spl71 | spl235), inference(avatar_split_clause, [status(thm)], [p955, sdef71, sdef235])).
% 121.12/16.54  cnf(p957, plain, empty_carrier(sk20) | ~empty(cast_as_carrier_subset(sk20)), inference(resolution, [status(thm)], [c101, c271])).
% 121.12/16.54  fof(sdef236, definition, (spl236 <=> (~empty(cast_as_carrier_subset(sk20)))), introduced(definition, [new_symbols(naming, [spl236])], [avatar_definition])).
% 121.12/16.54  cnf(ssp177, plain, (spl90 | spl236), inference(avatar_split_clause, [status(thm)], [p957, sdef90, sdef236])).
% 121.12/16.54  cnf(p959, plain, empty_carrier(sk26) | ~empty(cast_as_carrier_subset(sk26)), inference(resolution, [status(thm)], [c101, c295])).
% 121.12/16.54  fof(sdef237, definition, (spl237 <=> (~empty(cast_as_carrier_subset(sk26)))), introduced(definition, [new_symbols(naming, [spl237])], [avatar_definition])).
% 121.12/16.54  cnf(ssp178, plain, (spl106 | spl237), inference(avatar_split_clause, [status(thm)], [p959, sdef106, sdef237])).
% 121.12/16.54  cnf(p961, plain, empty_carrier(sk34) | ~empty(cast_as_carrier_subset(sk34)), inference(resolution, [status(thm)], [c101, c331])).
% 121.12/16.54  fof(sdef238, definition, (spl238 <=> (~empty(cast_as_carrier_subset(sk34)))), introduced(definition, [new_symbols(naming, [spl238])], [avatar_definition])).
% 121.12/16.54  cnf(ssp179, plain, (spl119 | spl238), inference(avatar_split_clause, [status(thm)], [p961, sdef119, sdef238])).
% 121.12/16.54  cnf(c102, plain, empty_carrier(X0) | ~rel_str(X0) | lower_relstr_subset(cast_as_carrier_subset(X0),X0), inference(cnf_transformation, [status(esa)], [f52_sk])).
% 121.12/16.54  cnf(p968, plain, empty_carrier(sk0) | lower_relstr_subset(cast_as_carrier_subset(sk0),sk0), inference(resolution, [status(thm)], [c102, c90])).
% 121.12/16.54  fof(sdef239, definition, (spl239 <=> (lower_relstr_subset(cast_as_carrier_subset(sk0),sk0))), introduced(definition, [new_symbols(naming, [spl239])], [avatar_definition])).
% 121.12/16.54  cnf(ssp180, plain, (spl6 | spl239), inference(avatar_split_clause, [status(thm)], [p968, sdef6, sdef239])).
% 121.12/16.54  cnf(p970, plain, empty_carrier(sk10) | lower_relstr_subset(cast_as_carrier_subset(sk10),sk10), inference(resolution, [status(thm)], [c102, c206])).
% 121.12/16.54  fof(sdef240, definition, (spl240 <=> (lower_relstr_subset(cast_as_carrier_subset(sk10),sk10))), introduced(definition, [new_symbols(naming, [spl240])], [avatar_definition])).
% 121.12/16.54  cnf(ssp181, plain, (spl13 | spl240), inference(avatar_split_clause, [status(thm)], [p970, sdef13, sdef240])).
% 121.12/16.54  cnf(p972, plain, empty_carrier(sk11) | lower_relstr_subset(cast_as_carrier_subset(sk11),sk11), inference(resolution, [status(thm)], [c102, c212])).
% 121.12/16.54  fof(sdef241, definition, (spl241 <=> (lower_relstr_subset(cast_as_carrier_subset(sk11),sk11))), introduced(definition, [new_symbols(naming, [spl241])], [avatar_definition])).
% 121.12/16.54  cnf(ssp182, plain, (spl158 | spl241), inference(avatar_split_clause, [status(thm)], [p972, sdef158, sdef241])).
% 121.12/16.54  cnf(p974, plain, empty_carrier(sk13) | lower_relstr_subset(cast_as_carrier_subset(sk13),sk13), inference(resolution, [status(thm)], [c102, c228])).
% 121.12/16.54  fof(sdef242, definition, (spl242 <=> (lower_relstr_subset(cast_as_carrier_subset(sk13),sk13))), introduced(definition, [new_symbols(naming, [spl242])], [avatar_definition])).
% 121.12/16.54  cnf(ssp183, plain, (spl26 | spl242), inference(avatar_split_clause, [status(thm)], [p974, sdef26, sdef242])).
% 121.12/16.54  cnf(p976, plain, empty_carrier(sk18) | lower_relstr_subset(cast_as_carrier_subset(sk18),sk18), inference(resolution, [status(thm)], [c102, c244])).
% 121.12/16.54  fof(sdef243, definition, (spl243 <=> (lower_relstr_subset(cast_as_carrier_subset(sk18),sk18))), introduced(definition, [new_symbols(naming, [spl243])], [avatar_definition])).
% 121.12/16.54  cnf(ssp184, plain, (spl35 | spl243), inference(avatar_split_clause, [status(thm)], [p976, sdef35, sdef243])).
% 121.12/16.54  cnf(p978, plain, empty_carrier(sk19) | lower_relstr_subset(cast_as_carrier_subset(sk19),sk19), inference(resolution, [status(thm)], [c102, c261])).
% 121.12/16.54  fof(sdef244, definition, (spl244 <=> (lower_relstr_subset(cast_as_carrier_subset(sk19),sk19))), introduced(definition, [new_symbols(naming, [spl244])], [avatar_definition])).
% 121.12/16.54  cnf(ssp185, plain, (spl71 | spl244), inference(avatar_split_clause, [status(thm)], [p978, sdef71, sdef244])).
% 121.12/16.54  cnf(p980, plain, empty_carrier(sk20) | lower_relstr_subset(cast_as_carrier_subset(sk20),sk20), inference(resolution, [status(thm)], [c102, c271])).
% 121.12/16.54  fof(sdef245, definition, (spl245 <=> (lower_relstr_subset(cast_as_carrier_subset(sk20),sk20))), introduced(definition, [new_symbols(naming, [spl245])], [avatar_definition])).
% 121.12/16.54  cnf(ssp186, plain, (spl90 | spl245), inference(avatar_split_clause, [status(thm)], [p980, sdef90, sdef245])).
% 121.12/16.54  cnf(p982, plain, empty_carrier(sk26) | lower_relstr_subset(cast_as_carrier_subset(sk26),sk26), inference(resolution, [status(thm)], [c102, c295])).
% 121.12/16.54  fof(sdef246, definition, (spl246 <=> (lower_relstr_subset(cast_as_carrier_subset(sk26),sk26))), introduced(definition, [new_symbols(naming, [spl246])], [avatar_definition])).
% 121.12/16.54  cnf(ssp187, plain, (spl106 | spl246), inference(avatar_split_clause, [status(thm)], [p982, sdef106, sdef246])).
% 121.12/16.54  cnf(p984, plain, empty_carrier(sk34) | lower_relstr_subset(cast_as_carrier_subset(sk34),sk34), inference(resolution, [status(thm)], [c102, c331])).
% 121.12/16.54  fof(sdef247, definition, (spl247 <=> (lower_relstr_subset(cast_as_carrier_subset(sk34),sk34))), introduced(definition, [new_symbols(naming, [spl247])], [avatar_definition])).
% 121.12/16.54  cnf(ssp188, plain, (spl119 | spl247), inference(avatar_split_clause, [status(thm)], [p984, sdef119, sdef247])).
% 121.12/16.54  cnf(c103, plain, empty_carrier(X0) | ~rel_str(X0) | upper_relstr_subset(cast_as_carrier_subset(X0),X0), inference(cnf_transformation, [status(esa)], [f52_sk])).
% 121.12/16.54  cnf(p987, plain, empty_carrier(sk0) | upper_relstr_subset(cast_as_carrier_subset(sk0),sk0), inference(resolution, [status(thm)], [c103, c90])).
% 121.12/16.54  fof(sdef248, definition, (spl248 <=> (upper_relstr_subset(cast_as_carrier_subset(sk0),sk0))), introduced(definition, [new_symbols(naming, [spl248])], [avatar_definition])).
% 121.12/16.54  cnf(ssp189, plain, (spl6 | spl248), inference(avatar_split_clause, [status(thm)], [p987, sdef6, sdef248])).
% 121.12/16.54  cnf(p989, plain, empty_carrier(sk10) | upper_relstr_subset(cast_as_carrier_subset(sk10),sk10), inference(resolution, [status(thm)], [c103, c206])).
% 121.12/16.54  fof(sdef249, definition, (spl249 <=> (upper_relstr_subset(cast_as_carrier_subset(sk10),sk10))), introduced(definition, [new_symbols(naming, [spl249])], [avatar_definition])).
% 121.12/16.54  cnf(ssp190, plain, (spl13 | spl249), inference(avatar_split_clause, [status(thm)], [p989, sdef13, sdef249])).
% 121.12/16.54  cnf(p991, plain, empty_carrier(sk11) | upper_relstr_subset(cast_as_carrier_subset(sk11),sk11), inference(resolution, [status(thm)], [c103, c212])).
% 121.12/16.54  fof(sdef250, definition, (spl250 <=> (upper_relstr_subset(cast_as_carrier_subset(sk11),sk11))), introduced(definition, [new_symbols(naming, [spl250])], [avatar_definition])).
% 121.12/16.54  cnf(ssp191, plain, (spl158 | spl250), inference(avatar_split_clause, [status(thm)], [p991, sdef158, sdef250])).
% 121.12/16.54  cnf(p993, plain, empty_carrier(sk13) | upper_relstr_subset(cast_as_carrier_subset(sk13),sk13), inference(resolution, [status(thm)], [c103, c228])).
% 121.12/16.54  fof(sdef251, definition, (spl251 <=> (upper_relstr_subset(cast_as_carrier_subset(sk13),sk13))), introduced(definition, [new_symbols(naming, [spl251])], [avatar_definition])).
% 121.12/16.54  cnf(ssp192, plain, (spl26 | spl251), inference(avatar_split_clause, [status(thm)], [p993, sdef26, sdef251])).
% 121.12/16.54  cnf(p995, plain, empty_carrier(sk18) | upper_relstr_subset(cast_as_carrier_subset(sk18),sk18), inference(resolution, [status(thm)], [c103, c244])).
% 121.12/16.54  fof(sdef252, definition, (spl252 <=> (upper_relstr_subset(cast_as_carrier_subset(sk18),sk18))), introduced(definition, [new_symbols(naming, [spl252])], [avatar_definition])).
% 121.12/16.54  cnf(ssp193, plain, (spl35 | spl252), inference(avatar_split_clause, [status(thm)], [p995, sdef35, sdef252])).
% 121.12/16.54  cnf(p997, plain, empty_carrier(sk19) | upper_relstr_subset(cast_as_carrier_subset(sk19),sk19), inference(resolution, [status(thm)], [c103, c261])).
% 121.12/16.54  fof(sdef253, definition, (spl253 <=> (upper_relstr_subset(cast_as_carrier_subset(sk19),sk19))), introduced(definition, [new_symbols(naming, [spl253])], [avatar_definition])).
% 121.12/16.54  cnf(ssp194, plain, (spl71 | spl253), inference(avatar_split_clause, [status(thm)], [p997, sdef71, sdef253])).
% 121.12/16.54  cnf(p999, plain, empty_carrier(sk20) | upper_relstr_subset(cast_as_carrier_subset(sk20),sk20), inference(resolution, [status(thm)], [c103, c271])).
% 121.12/16.54  fof(sdef254, definition, (spl254 <=> (upper_relstr_subset(cast_as_carrier_subset(sk20),sk20))), introduced(definition, [new_symbols(naming, [spl254])], [avatar_definition])).
% 121.12/16.54  cnf(ssp195, plain, (spl90 | spl254), inference(avatar_split_clause, [status(thm)], [p999, sdef90, sdef254])).
% 121.12/16.54  cnf(p1001, plain, empty_carrier(sk26) | upper_relstr_subset(cast_as_carrier_subset(sk26),sk26), inference(resolution, [status(thm)], [c103, c295])).
% 121.12/16.54  fof(sdef255, definition, (spl255 <=> (upper_relstr_subset(cast_as_carrier_subset(sk26),sk26))), introduced(definition, [new_symbols(naming, [spl255])], [avatar_definition])).
% 121.12/16.54  cnf(ssp196, plain, (spl106 | spl255), inference(avatar_split_clause, [status(thm)], [p1001, sdef106, sdef255])).
% 121.12/16.54  fof(f56, axiom, ! [A] : ( ( ~ empty_carrier(A) & one_sorted_str(A) ) => ~ empty(cast_as_carrier_subset(A)) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc2_pre_topc)).
% 121.12/16.54  fof(f56_nnf, plain, ! [A] : (((empty_carrier(A) | ~(one_sorted_str(A))) | ~(empty(cast_as_carrier_subset(A))))), inference(nnf_transformation, [status(thm)], [f56])).
% 121.12/16.54  fof(f56_sk, plain, ! [A] : (((empty_carrier(A) | ~(one_sorted_str(A))) | ~(empty(cast_as_carrier_subset(A))))), inference(skolemisation, [status(esa)], [f56_nnf])).
% 121.12/16.54  cnf(c124, plain, empty_carrier(X0) | ~one_sorted_str(X0) | ~empty(cast_as_carrier_subset(X0)), inference(cnf_transformation, [status(esa)], [f56_sk])).
% 121.12/16.54  cnf(p1032, plain, empty_carrier(sk43) | ~empty(cast_as_carrier_subset(sk43)), inference(resolution, [status(thm)], [c124, p817])).
% 121.12/16.54  cnf(ssp197, plain, (spl180 | spl183), inference(avatar_split_clause, [status(thm)], [p1032, sdef180, sdef183])).
% 121.12/16.54  fof(f64, axiom, ! [A] : ( ( topological_space(A) & top_str(A) ) => closed_subset(cast_as_carrier_subset(A),A) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc5_pre_topc)).
% 121.12/16.54  fof(f64_nnf, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | closed_subset(cast_as_carrier_subset(A),A))), inference(nnf_transformation, [status(thm)], [f64])).
% 121.12/16.54  fof(f64_sk, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | closed_subset(cast_as_carrier_subset(A),A))), inference(skolemisation, [status(esa)], [f64_nnf])).
% 121.12/16.54  cnf(c154, plain, ~topological_space(X0) | ~top_str(X0) | closed_subset(cast_as_carrier_subset(X0),X0), inference(cnf_transformation, [status(esa)], [f64_sk])).
% 121.12/16.54  cnf(p1122, plain, ~top_str(sk43) | closed_subset(cast_as_carrier_subset(sk43),sk43), inference(resolution, [status(thm)], [c154, c377])).
% 121.12/16.54  cnf(ssp198, plain, (spl138 | spl185), inference(avatar_split_clause, [status(thm)], [p1122, sdef138, sdef185])).
% 121.12/16.54  fof(f67, axiom, ! [A] : ( ( topological_space(A) & top_str(A) ) => ( open_subset(cast_as_carrier_subset(A),A) & closed_subset(cast_as_carrier_subset(A),A) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc8_tops_1)).
% 121.12/16.54  fof(f67_nnf, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | (open_subset(cast_as_carrier_subset(A),A) & closed_subset(cast_as_carrier_subset(A),A)))), inference(nnf_transformation, [status(thm)], [f67])).
% 121.12/16.54  fof(f67_sk, plain, ! [A] : (((~(topological_space(A)) | ~(top_str(A))) | (open_subset(cast_as_carrier_subset(A),A) & closed_subset(cast_as_carrier_subset(A),A)))), inference(skolemisation, [status(esa)], [f67_nnf])).
% 121.12/16.54  cnf(c162, plain, ~topological_space(X0) | ~top_str(X0) | open_subset(cast_as_carrier_subset(X0),X0), inference(cnf_transformation, [status(esa)], [f67_sk])).
% 121.12/16.54  cnf(p1143, plain, ~top_str(sk43) | open_subset(cast_as_carrier_subset(sk43),sk43), inference(resolution, [status(thm)], [c162, c377])).
% 121.12/16.54  cnf(ssp199, plain, (spl138 | spl184), inference(avatar_split_clause, [status(thm)], [p1143, sdef138, sdef184])).
% 121.12/16.54  cnf(p794, plain, (~element(X0,the_carrier(sk43)) | neighborhood_system(sk43,X0) = a_2_0_yellow19(sk43,X0) | ~spl181), inference(avatar_component_clause, [status(thm)], [sdef181])).
% 121.12/16.54  cnf(p796, plain, (neighborhood_system(sk43,sk44) = a_2_0_yellow19(sk43,sk44) | ~spl181), inference(resolution, [status(thm)], [p794, c379])).
% 121.12/16.54  fof(f71, axiom, ! [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 ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fraenkel_a_2_0_yellow19)).
% 121.12/16.54  fof(f71_nnf, plain, ! [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)))))), inference(nnf_transformation, [status(thm)], [f71])).
% 121.12/16.54  fof(f71_sk, plain, ! [B,C,A,D] : (((((empty_carrier(B) | ~(topological_space(B))) | ~(top_str(B))) | ~(element(C,the_carrier(B)))) | ((~(in(A,a_2_0_yellow19(B,C))) | (point_neighbourhood(sk7(A,B,C),B,C) & A = sk7(A,B,C))) & (in(A,a_2_0_yellow19(B,C)) | (~(point_neighbourhood(D,B,C)) | A != D))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk7])], [f71_nnf])).
% 121.12/16.54  cnf(c192, plain, empty_carrier(X1) | ~topological_space(X1) | ~top_str(X1) | ~element(X2,the_carrier(X1)) | ~in(X0,a_2_0_yellow19(X1,X2)) | X0 = sk7(X0,X1,X2), inference(cnf_transformation, [status(esa)], [f71_sk])).
% 121.12/16.54  cnf(p1152, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | ~in(X1,a_2_0_yellow19(sk43,X0)) | X1 = sk7(X1,sk43,X0), inference(resolution, [status(thm)], [c192, c377])).
% 121.12/16.54  cnf(p1172, plain, empty_carrier(sk43) | ~element(X0,the_carrier(sk43)) | ~in(X1,a_2_0_yellow19(sk43,X0)) | X1 = sk7(X1,sk43,X0), inference(resolution, [status(thm)], [p1152, c378])).
% 121.12/16.54  cnf(p1181, plain, empty_carrier(sk43) | ~in(X0,a_2_0_yellow19(sk43,sk44)) | X0 = sk7(X0,sk43,sk44), inference(resolution, [status(thm)], [p1172, c379])).
% 121.12/16.54  cnf(p1183, plain, (empty_carrier(sk43) | ~in(X0,neighborhood_system(sk43,sk44)) | X0 = sk7(X0,sk43,sk44) | ~spl181), inference(superposition, [status(thm)], [p796, p1181])).
% 121.12/16.54  cnf(p1184, plain, (empty_carrier(sk43) | sk45 = sk7(sk45,sk43,sk44) | ~spl0 | ~spl181), inference(resolution, [status(thm)], [p1183, p381])).
% 121.12/16.54  cnf(c191, plain, empty_carrier(X1) | ~topological_space(X1) | ~top_str(X1) | ~element(X2,the_carrier(X1)) | ~in(X0,a_2_0_yellow19(X1,X2)) | point_neighbourhood(sk7(X0,X1,X2),X1,X2), inference(cnf_transformation, [status(esa)], [f71_sk])).
% 121.12/16.54  cnf(p1146, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | ~in(X1,a_2_0_yellow19(sk43,X0)) | point_neighbourhood(sk7(X1,sk43,X0),sk43,X0), inference(resolution, [status(thm)], [c191, c377])).
% 121.12/16.54  cnf(p1147, plain, empty_carrier(sk43) | ~element(X0,the_carrier(sk43)) | ~in(X1,a_2_0_yellow19(sk43,X0)) | point_neighbourhood(sk7(X1,sk43,X0),sk43,X0), inference(resolution, [status(thm)], [p1146, c378])).
% 121.12/16.54  cnf(p1148, plain, empty_carrier(sk43) | ~in(X0,a_2_0_yellow19(sk43,sk44)) | point_neighbourhood(sk7(X0,sk43,sk44),sk43,sk44), inference(resolution, [status(thm)], [p1147, c379])).
% 121.12/16.54  cnf(p1150, plain, (empty_carrier(sk43) | ~in(X0,neighborhood_system(sk43,sk44)) | point_neighbourhood(sk7(X0,sk43,sk44),sk43,sk44) | ~spl181), inference(superposition, [status(thm)], [p796, p1148])).
% 121.12/16.54  cnf(p1151, plain, (empty_carrier(sk43) | point_neighbourhood(sk7(sk45,sk43,sk44),sk43,sk44) | ~spl0 | ~spl181), inference(resolution, [status(thm)], [p1150, p381])).
% 121.12/16.54  cnf(p1185, plain, (empty_carrier(sk43) | empty_carrier(sk43) | point_neighbourhood(sk45,sk43,sk44) | ~spl0 | ~spl181), inference(superposition, [status(thm)], [p1184, p1151])).
% 121.12/16.54  cnf(ssp200, plain, (~spl0 | ~spl181 | spl2 | spl180), inference(avatar_split_clause, [status(thm)], [p1185, sdef2, sdef180])).
% 121.12/16.54  cnf(c193, plain, empty_carrier(X1) | ~topological_space(X1) | ~top_str(X1) | ~element(X2,the_carrier(X1)) | in(X0,a_2_0_yellow19(X1,X2)) | ~point_neighbourhood(X3,X1,X2) | X0 != X3, inference(cnf_transformation, [status(esa)], [f71_sk])).
% 121.12/16.54  cnf(p1168, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | in(X1,a_2_0_yellow19(sk43,X0)) | ~point_neighbourhood(X2,sk43,X0) | X1 != X2, inference(resolution, [status(thm)], [c193, c377])).
% 121.12/16.54  cnf(p1241, plain, empty_carrier(sk43) | ~top_str(sk43) | ~element(X0,the_carrier(sk43)) | in(X1,a_2_0_yellow19(sk43,X0)) | ~point_neighbourhood(X1,sk43,X0), inference(equality_resolution, [status(thm)], [p1168])).
% 121.12/16.54  cnf(p1243, plain, empty_carrier(sk43) | ~element(X0,the_carrier(sk43)) | in(X1,a_2_0_yellow19(sk43,X0)) | ~point_neighbourhood(X1,sk43,X0), inference(resolution, [status(thm)], [p1241, c378])).
% 121.12/16.54  cnf(p1252, plain, empty_carrier(sk43) | in(X0,a_2_0_yellow19(sk43,sk44)) | ~point_neighbourhood(X0,sk43,sk44), inference(resolution, [status(thm)], [p1243, c379])).
% 121.12/16.54  cnf(p1254, plain, (empty_carrier(sk43) | in(sk45,a_2_0_yellow19(sk43,sk44)) | ~spl2), inference(resolution, [status(thm)], [p1252, p384])).
% 121.12/16.54  cnf(p1257, plain, (empty_carrier(sk43) | in(sk45,neighborhood_system(sk43,sk44)) | ~spl2 | ~spl181), inference(superposition, [status(thm)], [p796, p1254])).
% 121.12/16.54  cnf(ssp201, plain, (~spl2 | ~spl181 | spl0 | spl180), inference(avatar_split_clause, [status(thm)], [p1257, sdef0, sdef180])).
% 121.12/16.54  cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, ssp142, ssp143, ssp144, ssp145, ssp146, ssp147, ssp148, ssp149, ssp150, ssp151, ssp152, ssp153, ssp154, ssp155, ssp156, ssp157, ssp158, ssp159, ssp160, ssp161, ssp162, ssp163, ssp164, ssp165, ssp166, ssp167, ssp168, ssp169, ssp170, ssp171, ssp172, ssp173, ssp174, ssp175, ssp176, ssp177, ssp178, ssp179, ssp180, ssp181, ssp182, ssp183, ssp184, ssp185, ssp186, ssp187, ssp188, ssp189, ssp190, ssp191, ssp192, ssp193, ssp194, ssp195, ssp196, ssp197, ssp198, ssp199, ssp200, ssp201, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20, sct21, sct22, sct23, sct24, sct25, sct26, sct27, sct28, sct29, sct30, sct31, sct32, sct33, sct34, sct35, sct36, sct37, sct38, sct39, sct40, sct41, sct42, sct43, sct44, sct45, sct46, sct47, sct48, sct49, sct50, sct51, sct52, sct53, sct54, sct55, sct56, sct57, sct58, sct59, sct60, sct61, sct62, sct63, sct64, sct65, sct66, sct67, sct68, sct69, sct70, sct71, sct72, sct73, sct74, sct75, sct76, sct77, sct78, sct79, sct80, sct81, sct82, sct83, sct84, sct85, sct86, sct87, sct88, sct89, sct90, sct91, sct92, sct93, sct94, sct95, sct96, sct97, sct98, sct99, sct100, sct101, sct102, sct103])).
% 121.12/16.54  % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------