%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU341+1 : TPTP v9.2.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:11:32 PM UTC 2026
% Result : Theorem 0.43s 1.62s
% Output : CNFRefutation 1.14s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 323)
% Comments :
%------------------------------------------------------------------------------
fof(d1_connsp_2,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,powerset(the_carrier(X1)))
=> ( point_neighbourhood(X3,X1,X2)
<=> in(X2,interior(X1,X3)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_connsp_2) ).
fof(dt_m1_connsp_2,axiom,
! [X1,X2] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& element(X2,the_carrier(X1)) )
=> ! [X3] :
( point_neighbourhood(X3,X1,X2)
=> element(X3,powerset(the_carrier(X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_connsp_2) ).
fof(existence_m1_connsp_2,axiom,
! [X1,X2] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& element(X2,the_carrier(X1)) )
=> ? [X3] : point_neighbourhood(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_connsp_2) ).
fof(t5_connsp_2,conjecture,
! [X1] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1) )
=> ! [X2] :
( element(X2,powerset(the_carrier(X1)))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( ( open_subset(X2,X1)
& in(X3,X2) )
=> point_neighbourhood(X2,X1,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_connsp_2) ).
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(rc1_subset_1,axiom,
! [X1] :
( ~ empty(X1)
=> ? [X2] :
( element(X2,powerset(X1))
& ~ empty(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(fc1_subset_1,axiom,
! [X1] : ~ empty(powerset(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(rc1_membered,axiom,
? [X1] :
( ~ empty(X1)
& v1_membered(X1)
& v2_membered(X1)
& v3_membered(X1)
& v4_membered(X1)
& v5_membered(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_membered) ).
fof(t55_tops_1,axiom,
! [X1] :
( ( topological_space(X1)
& top_str(X1) )
=> ! [X2] :
( top_str(X2)
=> ! [X3] :
( element(X3,powerset(the_carrier(X1)))
=> ! [X4] :
( element(X4,powerset(the_carrier(X2)))
=> ( ( open_subset(X4,X2)
=> interior(X2,X4) = X4 )
& ( interior(X1,X3) = X3
=> open_subset(X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t55_tops_1) ).
fof(dt_k1_tops_1,axiom,
! [X1,X2] :
( ( top_str(X1)
& element(X2,powerset(the_carrier(X1))) )
=> element(interior(X1,X2),powerset(the_carrier(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_tops_1) ).
fof(t4_subset,axiom,
! [X1,X2,X3] :
( ( in(X1,X2)
& element(X2,powerset(X3)) )
=> element(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( in(X1,X2)
& element(X2,powerset(X3))
& empty(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(t3_subset,axiom,
! [X1,X2] :
( element(X1,powerset(X2))
<=> subset(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(cc20_membered,axiom,
! [X1] :
( v5_membered(X1)
=> ! [X2] :
( element(X2,powerset(X1))
=> ( v1_membered(X2)
& v2_membered(X2)
& v3_membered(X2)
& v4_membered(X2)
& v5_membered(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc20_membered) ).
fof(cc19_membered,axiom,
! [X1] :
( v4_membered(X1)
=> ! [X2] :
( element(X2,powerset(X1))
=> ( v1_membered(X2)
& v2_membered(X2)
& v3_membered(X2)
& v4_membered(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc19_membered) ).
fof(cc18_membered,axiom,
! [X1] :
( v3_membered(X1)
=> ! [X2] :
( element(X2,powerset(X1))
=> ( v1_membered(X2)
& v2_membered(X2)
& v3_membered(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc18_membered) ).
fof(cc17_membered,axiom,
! [X1] :
( v2_membered(X1)
=> ! [X2] :
( element(X2,powerset(X1))
=> ( v1_membered(X2)
& v2_membered(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc17_membered) ).
fof(cc16_membered,axiom,
! [X1] :
( v1_membered(X1)
=> ! [X2] :
( element(X2,powerset(X1))
=> v1_membered(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc16_membered) ).
fof(t2_subset,axiom,
! [X1,X2] :
( element(X1,X2)
=> ( empty(X2)
| in(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(t1_subset,axiom,
! [X1,X2] :
( in(X1,X2)
=> element(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(cc14_membered,axiom,
! [X1] :
( v5_membered(X1)
=> ! [X2] :
( element(X2,X1)
=> ( v1_xcmplx_0(X2)
& natural(X2)
& v1_xreal_0(X2)
& v1_int_1(X2)
& v1_rat_1(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc14_membered) ).
fof(cc13_membered,axiom,
! [X1] :
( v4_membered(X1)
=> ! [X2] :
( element(X2,X1)
=> ( v1_xcmplx_0(X2)
& v1_xreal_0(X2)
& v1_int_1(X2)
& v1_rat_1(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc13_membered) ).
fof(cc12_membered,axiom,
! [X1] :
( v3_membered(X1)
=> ! [X2] :
( element(X2,X1)
=> ( v1_xcmplx_0(X2)
& v1_xreal_0(X2)
& v1_rat_1(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc12_membered) ).
fof(cc11_membered,axiom,
! [X1] :
( v2_membered(X1)
=> ! [X2] :
( element(X2,X1)
=> ( v1_xcmplx_0(X2)
& v1_xreal_0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc11_membered) ).
fof(cc10_membered,axiom,
! [X1] :
( v1_membered(X1)
=> ! [X2] :
( element(X2,X1)
=> v1_xcmplx_0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc10_membered) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( element(X2,powerset(X1))
& empty(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : element(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( empty(X1)
& X1 != X2
& empty(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : subset(X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(dt_l1_pre_topc,axiom,
! [X1] :
( top_str(X1)
=> one_sorted_str(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(cc15_membered,axiom,
! [X1] :
( empty(X1)
=> ( v1_membered(X1)
& v2_membered(X1)
& v3_membered(X1)
& v4_membered(X1)
& v5_membered(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc15_membered) ).
fof(cc1_membered,axiom,
! [X1] :
( v5_membered(X1)
=> v4_membered(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_membered) ).
fof(cc2_membered,axiom,
! [X1] :
( v4_membered(X1)
=> v3_membered(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_membered) ).
fof(cc3_membered,axiom,
! [X1] :
( v3_membered(X1)
=> v2_membered(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc3_membered) ).
fof(cc4_membered,axiom,
! [X1] :
( v2_membered(X1)
=> v1_membered(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc4_membered) ).
fof(t6_boole,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(existence_l1_struct_0,axiom,
? [X1] : one_sorted_str(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_l1_struct_0) ).
fof(existence_l1_pre_topc,axiom,
? [X1] : top_str(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_l1_pre_topc) ).
fof(fc6_membered,axiom,
( empty(empty_set)
& v1_membered(empty_set)
& v2_membered(empty_set)
& v3_membered(empty_set)
& v4_membered(empty_set)
& v5_membered(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_membered) ).
fof(i_0_40,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,powerset(the_carrier(X1)))
=> ( point_neighbourhood(X3,X1,X2)
<=> in(X2,interior(X1,X3)) ) ) ) ),
inference(fof_simplification,[status(thm)],[d1_connsp_2]) ).
fof(i_0_41,plain,
! [X1,X2] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& element(X2,the_carrier(X1)) )
=> ! [X3] :
( point_neighbourhood(X3,X1,X2)
=> element(X3,powerset(the_carrier(X1))) ) ),
inference(fof_simplification,[status(thm)],[dt_m1_connsp_2]) ).
fof(i_0_42,plain,
! [X1,X2] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& element(X2,the_carrier(X1)) )
=> ? [X3] : point_neighbourhood(X3,X1,X2) ),
inference(fof_simplification,[status(thm)],[existence_m1_connsp_2]) ).
fof(i_0_43,negated_conjecture,
~ ! [X1] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1) )
=> ! [X2] :
( element(X2,powerset(the_carrier(X1)))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( ( open_subset(X2,X1)
& in(X3,X2) )
=> point_neighbourhood(X2,X1,X3) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t5_connsp_2])]) ).
fof(i_0_44,plain,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_45,plain,
! [X1] :
( ~ empty(X1)
=> ? [X2] :
( element(X2,powerset(X1))
& ~ empty(X2) ) ),
inference(fof_simplification,[status(thm)],[rc1_subset_1]) ).
fof(i_0_46,plain,
! [X1] : ~ empty(powerset(X1)),
inference(fof_simplification,[status(thm)],[fc1_subset_1]) ).
fof(i_0_47,plain,
? [X1] :
( ~ empty(X1)
& v1_membered(X1)
& v2_membered(X1)
& v3_membered(X1)
& v4_membered(X1)
& v5_membered(X1) ),
inference(fof_simplification,[status(thm)],[rc1_membered]) ).
fof(i_0_48,plain,
! [X107,X108,X109] :
( ( ~ point_neighbourhood(X109,X107,X108)
| in(X108,interior(X107,X109))
| ~ element(X109,powerset(the_carrier(X107)))
| ~ element(X108,the_carrier(X107))
| empty_carrier(X107)
| ~ topological_space(X107)
| ~ top_str(X107) )
& ( ~ in(X108,interior(X107,X109))
| point_neighbourhood(X109,X107,X108)
| ~ element(X109,powerset(the_carrier(X107)))
| ~ element(X108,the_carrier(X107))
| empty_carrier(X107)
| ~ topological_space(X107)
| ~ top_str(X107) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_40])])])]) ).
fof(i_0_49,plain,
! [X113,X114,X115] :
( empty_carrier(X113)
| ~ topological_space(X113)
| ~ top_str(X113)
| ~ element(X114,the_carrier(X113))
| ~ point_neighbourhood(X115,X113,X114)
| element(X115,powerset(the_carrier(X113))) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_41])])]) ).
fof(i_0_50,plain,
! [X139,X140,X141,X142] :
( ( ~ open_subset(X142,X140)
| interior(X140,X142) = X142
| ~ element(X142,powerset(the_carrier(X140)))
| ~ element(X141,powerset(the_carrier(X139)))
| ~ top_str(X140)
| ~ topological_space(X139)
| ~ top_str(X139) )
& ( interior(X139,X141) != X141
| open_subset(X141,X139)
| ~ element(X142,powerset(the_carrier(X140)))
| ~ element(X141,powerset(the_carrier(X139)))
| ~ top_str(X140)
| ~ topological_space(X139)
| ~ top_str(X139) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t55_tops_1])])])]) ).
fof(i_0_51,plain,
! [X118,X119] :
( empty_carrier(X118)
| ~ topological_space(X118)
| ~ top_str(X118)
| ~ element(X119,the_carrier(X118))
| point_neighbourhood(esk3_2(X118,X119),X118,X119) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_42])])]) ).
fof(i_0_52,plain,
! [X110,X111] :
( ~ top_str(X110)
| ~ element(X111,powerset(the_carrier(X110)))
| element(interior(X110,X111),powerset(the_carrier(X110))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_k1_tops_1])]) ).
fof(i_0_53,negated_conjecture,
( ~ empty_carrier(esk8_0)
& topological_space(esk8_0)
& top_str(esk8_0)
& element(esk9_0,powerset(the_carrier(esk8_0)))
& element(esk10_0,the_carrier(esk8_0))
& open_subset(esk9_0,esk8_0)
& in(esk10_0,esk9_0)
& ~ point_neighbourhood(esk9_0,esk8_0,esk10_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_43])])]) ).
fof(i_0_54,plain,
! [X136,X137,X138] :
( ~ in(X136,X137)
| ~ element(X137,powerset(X138))
| element(X136,X138) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t4_subset])]) ).
fof(i_0_55,plain,
! [X146,X147,X148] :
( ~ in(X146,X147)
| ~ element(X147,powerset(X148))
| ~ empty(X148) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
fof(i_0_56,plain,
! [X134,X135] :
( ( ~ element(X134,powerset(X135))
| subset(X134,X135) )
& ( ~ subset(X134,X135)
| element(X134,powerset(X135)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
fof(i_0_57,plain,
! [X80,X81] :
( ~ in(X80,X81)
| ~ in(X81,X80) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_44])]) ).
fof(i_0_58,plain,
! [X102,X103] :
( ( v1_membered(X103)
| ~ element(X103,powerset(X102))
| ~ v5_membered(X102) )
& ( v2_membered(X103)
| ~ element(X103,powerset(X102))
| ~ v5_membered(X102) )
& ( v3_membered(X103)
| ~ element(X103,powerset(X102))
| ~ v5_membered(X102) )
& ( v4_membered(X103)
| ~ element(X103,powerset(X102))
| ~ v5_membered(X102) )
& ( v5_membered(X103)
| ~ element(X103,powerset(X102))
| ~ v5_membered(X102) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc20_membered])])])]) ).
fof(i_0_59,plain,
! [X99,X100] :
( ( v1_membered(X100)
| ~ element(X100,powerset(X99))
| ~ v4_membered(X99) )
& ( v2_membered(X100)
| ~ element(X100,powerset(X99))
| ~ v4_membered(X99) )
& ( v3_membered(X100)
| ~ element(X100,powerset(X99))
| ~ v4_membered(X99) )
& ( v4_membered(X100)
| ~ element(X100,powerset(X99))
| ~ v4_membered(X99) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc19_membered])])])]) ).
fof(i_0_60,plain,
! [X97,X98] :
( ( v1_membered(X98)
| ~ element(X98,powerset(X97))
| ~ v3_membered(X97) )
& ( v2_membered(X98)
| ~ element(X98,powerset(X97))
| ~ v3_membered(X97) )
& ( v3_membered(X98)
| ~ element(X98,powerset(X97))
| ~ v3_membered(X97) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc18_membered])])])]) ).
fof(i_0_61,plain,
! [X95,X96] :
( ( v1_membered(X96)
| ~ element(X96,powerset(X95))
| ~ v2_membered(X95) )
& ( v2_membered(X96)
| ~ element(X96,powerset(X95))
| ~ v2_membered(X95) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc17_membered])])])]) ).
fof(i_0_62,plain,
! [X93,X94] :
( ~ v1_membered(X93)
| ~ element(X94,powerset(X93))
| v1_membered(X94) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc16_membered])])]) ).
fof(i_0_63,plain,
! [X132,X133] :
( ~ element(X132,X133)
| empty(X133)
| in(X132,X133) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
fof(i_0_64,plain,
! [X130,X131] :
( ~ in(X130,X131)
| element(X130,X131) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])]) ).
fof(i_0_65,plain,
! [X90,X91] :
( ( v1_xcmplx_0(X91)
| ~ element(X91,X90)
| ~ v5_membered(X90) )
& ( natural(X91)
| ~ element(X91,X90)
| ~ v5_membered(X90) )
& ( v1_xreal_0(X91)
| ~ element(X91,X90)
| ~ v5_membered(X90) )
& ( v1_int_1(X91)
| ~ element(X91,X90)
| ~ v5_membered(X90) )
& ( v1_rat_1(X91)
| ~ element(X91,X90)
| ~ v5_membered(X90) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc14_membered])])])]) ).
fof(i_0_66,plain,
! [X88,X89] :
( ( v1_xcmplx_0(X89)
| ~ element(X89,X88)
| ~ v4_membered(X88) )
& ( v1_xreal_0(X89)
| ~ element(X89,X88)
| ~ v4_membered(X88) )
& ( v1_int_1(X89)
| ~ element(X89,X88)
| ~ v4_membered(X88) )
& ( v1_rat_1(X89)
| ~ element(X89,X88)
| ~ v4_membered(X88) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc13_membered])])])]) ).
fof(i_0_67,plain,
! [X86,X87] :
( ( v1_xcmplx_0(X87)
| ~ element(X87,X86)
| ~ v3_membered(X86) )
& ( v1_xreal_0(X87)
| ~ element(X87,X86)
| ~ v3_membered(X86) )
& ( v1_rat_1(X87)
| ~ element(X87,X86)
| ~ v3_membered(X86) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc12_membered])])])]) ).
fof(i_0_68,plain,
! [X84,X85] :
( ( v1_xcmplx_0(X85)
| ~ element(X85,X84)
| ~ v2_membered(X84) )
& ( v1_xreal_0(X85)
| ~ element(X85,X84)
| ~ v2_membered(X84) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc11_membered])])])]) ).
fof(i_0_69,plain,
! [X82,X83] :
( ~ v1_membered(X82)
| ~ element(X83,X82)
| v1_xcmplx_0(X83) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc10_membered])])]) ).
fof(i_0_70,plain,
! [X125] :
( ( element(esk6_1(X125),powerset(X125))
| empty(X125) )
& ( ~ empty(esk6_1(X125))
| empty(X125) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_45])])])]) ).
fof(i_0_71,plain,
! [X150,X151] :
( ~ in(X150,X151)
| ~ empty(X151) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(i_0_72,plain,
! [X127] :
( element(esk7_1(X127),powerset(X127))
& empty(esk7_1(X127)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(i_0_73,plain,
! [X121] : element(esk4_1(X121),X121),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
fof(i_0_74,plain,
! [X123] : ~ empty(powerset(X123)),
inference(variable_rename,[status(thm)],[i_0_46]) ).
fof(i_0_75,plain,
! [X152,X153] :
( ~ empty(X152)
| X152 = X153
| ~ empty(X153) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(i_0_76,plain,
! [X129] : subset(X129,X129),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_77,plain,
! [X112] :
( ~ top_str(X112)
| one_sorted_str(X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l1_pre_topc])]) ).
fof(i_0_78,plain,
! [X92] :
( ( v1_membered(X92)
| ~ empty(X92) )
& ( v2_membered(X92)
| ~ empty(X92) )
& ( v3_membered(X92)
| ~ empty(X92) )
& ( v4_membered(X92)
| ~ empty(X92) )
& ( v5_membered(X92)
| ~ empty(X92) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc15_membered])])]) ).
fof(i_0_79,plain,
! [X101] :
( ~ v5_membered(X101)
| v4_membered(X101) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_membered])]) ).
fof(i_0_80,plain,
! [X104] :
( ~ v4_membered(X104)
| v3_membered(X104) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc2_membered])]) ).
fof(i_0_81,plain,
! [X105] :
( ~ v3_membered(X105)
| v2_membered(X105) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc3_membered])]) ).
fof(i_0_82,plain,
! [X106] :
( ~ v2_membered(X106)
| v1_membered(X106) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc4_membered])]) ).
fof(i_0_83,plain,
! [X149] :
( ~ empty(X149)
| X149 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(i_0_84,plain,
( ~ empty(esk5_0)
& v1_membered(esk5_0)
& v2_membered(esk5_0)
& v3_membered(esk5_0)
& v4_membered(esk5_0)
& v5_membered(esk5_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_47])]) ).
fof(i_0_85,plain,
one_sorted_str(esk2_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_l1_struct_0])]) ).
fof(i_0_86,plain,
top_str(esk1_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_l1_pre_topc])]) ).
cnf(i_0_87,plain,
( in(X3,interior(X2,X1))
| empty_carrier(X2)
| ~ point_neighbourhood(X1,X2,X3)
| ~ element(X1,powerset(the_carrier(X2)))
| ~ element(X3,the_carrier(X2))
| ~ topological_space(X2)
| ~ top_str(X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_88,plain,
( point_neighbourhood(X3,X2,X1)
| empty_carrier(X2)
| ~ in(X1,interior(X2,X3))
| ~ element(X3,powerset(the_carrier(X2)))
| ~ element(X1,the_carrier(X2))
| ~ topological_space(X2)
| ~ top_str(X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_89,plain,
( empty_carrier(X1)
| element(X3,powerset(the_carrier(X1)))
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1))
| ~ point_neighbourhood(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_90,plain,
( open_subset(X2,X1)
| interior(X1,X2) != X2
| ~ element(X3,powerset(the_carrier(X4)))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ top_str(X4)
| ~ topological_space(X1)
| ~ top_str(X1) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_91,plain,
( interior(X2,X1) = X1
| ~ open_subset(X1,X2)
| ~ element(X1,powerset(the_carrier(X2)))
| ~ element(X3,powerset(the_carrier(X4)))
| ~ top_str(X2)
| ~ topological_space(X4)
| ~ top_str(X4) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_92,plain,
( empty_carrier(X1)
| point_neighbourhood(esk3_2(X1,X2),X1,X2)
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_93,plain,
( element(interior(X1,X2),powerset(the_carrier(X1)))
| ~ top_str(X1)
| ~ element(X2,powerset(the_carrier(X1))) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_94,negated_conjecture,
~ point_neighbourhood(esk9_0,esk8_0,esk10_0),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_95,plain,
( element(X1,X3)
| ~ in(X1,X2)
| ~ element(X2,powerset(X3)) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_96,plain,
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| ~ empty(X3) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_97,plain,
( subset(X1,X2)
| ~ element(X1,powerset(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_98,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_99,plain,
( v5_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_100,plain,
( v4_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_101,plain,
( v4_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_102,plain,
( v3_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_103,plain,
( v3_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_104,plain,
( v3_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v3_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_105,plain,
( v2_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_106,plain,
( v2_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_107,plain,
( v2_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v3_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_108,plain,
( v2_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v2_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_109,plain,
( v1_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_110,plain,
( v1_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_111,plain,
( v1_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v3_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_112,plain,
( v1_membered(X1)
| ~ element(X1,powerset(X2))
| ~ v2_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_113,plain,
( v1_membered(X2)
| ~ v1_membered(X1)
| ~ element(X2,powerset(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_114,plain,
( element(X1,powerset(X2))
| ~ subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_115,plain,
( empty(X2)
| in(X1,X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_116,plain,
( element(X1,X2)
| ~ in(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_117,plain,
( natural(X1)
| ~ element(X1,X2)
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_118,plain,
( v1_int_1(X1)
| ~ element(X1,X2)
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_119,plain,
( v1_int_1(X1)
| ~ element(X1,X2)
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_120,plain,
( v1_rat_1(X1)
| ~ element(X1,X2)
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_121,plain,
( v1_rat_1(X1)
| ~ element(X1,X2)
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_122,plain,
( v1_rat_1(X1)
| ~ element(X1,X2)
| ~ v3_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_123,plain,
( v1_xreal_0(X1)
| ~ element(X1,X2)
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_124,plain,
( v1_xreal_0(X1)
| ~ element(X1,X2)
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_125,plain,
( v1_xreal_0(X1)
| ~ element(X1,X2)
| ~ v3_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_126,plain,
( v1_xreal_0(X1)
| ~ element(X1,X2)
| ~ v2_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_127,plain,
( v1_xcmplx_0(X1)
| ~ element(X1,X2)
| ~ v5_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_128,plain,
( v1_xcmplx_0(X1)
| ~ element(X1,X2)
| ~ v4_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_129,plain,
( v1_xcmplx_0(X1)
| ~ element(X1,X2)
| ~ v3_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_130,plain,
( v1_xcmplx_0(X1)
| ~ element(X1,X2)
| ~ v2_membered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_131,plain,
( v1_xcmplx_0(X2)
| ~ v1_membered(X1)
| ~ element(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_132,plain,
( element(esk6_1(X1),powerset(X1))
| empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_133,plain,
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_134,plain,
element(esk7_1(X1),powerset(X1)),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_135,negated_conjecture,
element(esk9_0,powerset(the_carrier(esk8_0))),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_136,plain,
( empty(X1)
| ~ empty(esk6_1(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_137,plain,
element(esk4_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_138,plain,
~ empty(powerset(X1)),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_139,plain,
( X1 = X2
| ~ empty(X1)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_140,negated_conjecture,
element(esk10_0,the_carrier(esk8_0)),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_141,plain,
subset(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_142,plain,
( one_sorted_str(X1)
| ~ top_str(X1) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_143,plain,
( v5_membered(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_144,plain,
( v4_membered(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_145,plain,
( v4_membered(X1)
| ~ v5_membered(X1) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_146,plain,
( v3_membered(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_147,plain,
( v3_membered(X1)
| ~ v4_membered(X1) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_148,plain,
( v2_membered(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_149,plain,
( v2_membered(X1)
| ~ v3_membered(X1) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_150,plain,
( v1_membered(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_151,plain,
( v1_membered(X1)
| ~ v2_membered(X1) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_152,negated_conjecture,
open_subset(esk9_0,esk8_0),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_153,negated_conjecture,
in(esk10_0,esk9_0),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_154,plain,
empty(esk7_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_155,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_156,negated_conjecture,
~ empty_carrier(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_157,plain,
~ empty(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_158,plain,
one_sorted_str(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_159,negated_conjecture,
top_str(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_160,plain,
top_str(esk1_0),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_161,negated_conjecture,
topological_space(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_162,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc6_membered]),
[final] ).
cnf(i_0_163,plain,
v5_membered(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_164,plain,
v5_membered(empty_set),
inference(split_conjunct,[status(thm)],[fc6_membered]),
[final] ).
cnf(i_0_165,plain,
v4_membered(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_166,plain,
v4_membered(empty_set),
inference(split_conjunct,[status(thm)],[fc6_membered]),
[final] ).
cnf(i_0_167,plain,
v3_membered(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_168,plain,
v3_membered(empty_set),
inference(split_conjunct,[status(thm)],[fc6_membered]),
[final] ).
cnf(i_0_169,plain,
v2_membered(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_170,plain,
v2_membered(empty_set),
inference(split_conjunct,[status(thm)],[fc6_membered]),
[final] ).
cnf(i_0_171,plain,
v1_membered(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_172,plain,
v1_membered(empty_set),
inference(split_conjunct,[status(thm)],[fc6_membered]),
[final] ).
cnf(i_0_173,axiom,
X1 = X1 ).
cnf(i_0_174,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_175,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_176,axiom,
( X1 != X2
| interior(X1,X3) = interior(X2,X3) ) ).
cnf(i_0_177,axiom,
( X1 != X2
| interior(X3,X1) = interior(X3,X2) ) ).
cnf(i_0_178,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_179,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ~ v5_membered(X1)
| v5_membered(X2) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ~ v4_membered(X1)
| v4_membered(X2) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ~ v3_membered(X1)
| v3_membered(X2) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| ~ v2_membered(X1)
| v2_membered(X2) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| ~ v1_membered(X1)
| v1_membered(X2) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| ~ natural(X1)
| natural(X2) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ~ v1_int_1(X1)
| v1_int_1(X2) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ~ v1_rat_1(X1)
| v1_rat_1(X2) ) ).
cnf(i_0_188,axiom,
( X1 != X2
| ~ v1_xreal_0(X1)
| v1_xreal_0(X2) ) ).
cnf(i_0_189,axiom,
( X1 != X2
| ~ v1_xcmplx_0(X1)
| v1_xcmplx_0(X2) ) ).
cnf(i_0_190,axiom,
( X1 != X2
| ~ empty_carrier(X1)
| empty_carrier(X2) ) ).
cnf(i_0_191,axiom,
( X1 != X2
| ~ one_sorted_str(X1)
| one_sorted_str(X2) ) ).
cnf(i_0_192,axiom,
( X1 != X2
| ~ point_neighbourhood(X1,X3,X4)
| point_neighbourhood(X2,X3,X4) ) ).
cnf(i_0_193,axiom,
( X1 != X2
| ~ point_neighbourhood(X3,X1,X4)
| point_neighbourhood(X3,X2,X4) ) ).
cnf(i_0_194,axiom,
( X1 != X2
| ~ point_neighbourhood(X3,X4,X1)
| point_neighbourhood(X3,X4,X2) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| ~ element(X1,X3)
| element(X2,X3) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| ~ element(X3,X1)
| element(X3,X2) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| ~ topological_space(X1)
| topological_space(X2) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| ~ top_str(X1)
| top_str(X2) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ open_subset(X1,X3)
| open_subset(X2,X3) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ open_subset(X3,X1)
| open_subset(X3,X2) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_173_001,axiom,
X1 = X1 ).
cnf(i_0_174_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_175_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_176_004,axiom,
( X1 != X2
| interior(X1,X3) = interior(X2,X3) ) ).
cnf(i_0_177_005,axiom,
( X1 != X2
| interior(X3,X1) = interior(X3,X2) ) ).
cnf(i_0_178_006,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_179_007,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_180_008,axiom,
( X1 != X2
| ~ v5_membered(X1)
| v5_membered(X2) ) ).
cnf(i_0_181_009,axiom,
( X1 != X2
| ~ v4_membered(X1)
| v4_membered(X2) ) ).
cnf(i_0_182_010,axiom,
( X1 != X2
| ~ v3_membered(X1)
| v3_membered(X2) ) ).
cnf(i_0_183_011,axiom,
( X1 != X2
| ~ v2_membered(X1)
| v2_membered(X2) ) ).
cnf(i_0_184_012,axiom,
( X1 != X2
| ~ v1_membered(X1)
| v1_membered(X2) ) ).
cnf(i_0_185_013,axiom,
( X1 != X2
| ~ natural(X1)
| natural(X2) ) ).
cnf(i_0_186_014,axiom,
( X1 != X2
| ~ v1_int_1(X1)
| v1_int_1(X2) ) ).
cnf(i_0_187_015,axiom,
( X1 != X2
| ~ v1_rat_1(X1)
| v1_rat_1(X2) ) ).
cnf(i_0_188_016,axiom,
( X1 != X2
| ~ v1_xreal_0(X1)
| v1_xreal_0(X2) ) ).
cnf(i_0_189_017,axiom,
( X1 != X2
| ~ v1_xcmplx_0(X1)
| v1_xcmplx_0(X2) ) ).
cnf(i_0_190_018,axiom,
( X1 != X2
| ~ empty_carrier(X1)
| empty_carrier(X2) ) ).
cnf(i_0_191_019,axiom,
( X1 != X2
| ~ one_sorted_str(X1)
| one_sorted_str(X2) ) ).
cnf(i_0_192_020,axiom,
( X1 != X2
| ~ point_neighbourhood(X1,X3,X4)
| point_neighbourhood(X2,X3,X4) ) ).
cnf(i_0_193_021,axiom,
( X1 != X2
| ~ point_neighbourhood(X3,X1,X4)
| point_neighbourhood(X3,X2,X4) ) ).
cnf(i_0_194_022,axiom,
( X1 != X2
| ~ point_neighbourhood(X3,X4,X1)
| point_neighbourhood(X3,X4,X2) ) ).
cnf(i_0_195_023,axiom,
( X1 != X2
| ~ element(X1,X3)
| element(X2,X3) ) ).
cnf(i_0_196_024,axiom,
( X1 != X2
| ~ element(X3,X1)
| element(X3,X2) ) ).
cnf(i_0_197_025,axiom,
( X1 != X2
| ~ topological_space(X1)
| topological_space(X2) ) ).
cnf(i_0_198_026,axiom,
( X1 != X2
| ~ top_str(X1)
| top_str(X2) ) ).
cnf(i_0_199_027,axiom,
( X1 != X2
| ~ open_subset(X1,X3)
| open_subset(X2,X3) ) ).
cnf(i_0_200_028,axiom,
( X1 != X2
| ~ open_subset(X3,X1)
| open_subset(X3,X2) ) ).
cnf(i_0_201_029,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_202_030,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_203_031,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_204,plain,
subset(esk9_0,the_carrier(esk8_0)),
inference(scs_inference,[],[i_0_135,i_0_97]) ).
cnf(i_0_205,plain,
( ~ element(X1,powerset(X2))
| subset(X1,X2) ),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_206,plain,
~ in(esk9_0,esk10_0),
inference(scs_inference,[],[i_0_153,i_0_135,i_0_97,i_0_98]) ).
cnf(i_0_207,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_98]) ).
cnf(i_0_208,plain,
element(esk10_0,esk9_0),
inference(scs_inference,[],[i_0_153,i_0_135,i_0_97,i_0_98,i_0_116]) ).
cnf(i_0_209,plain,
( ~ in(X1,X2)
| element(X1,X2) ),
inference(rename_variables,[],[i_0_116]) ).
cnf(i_0_210,plain,
~ in(X1,empty_set),
inference(scs_inference,[],[i_0_153,i_0_135,i_0_162,i_0_97,i_0_98,i_0_116,i_0_133]) ).
cnf(i_0_211,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_212,plain,
one_sorted_str(esk8_0),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142]) ).
cnf(i_0_213,plain,
( ~ top_str(X1)
| one_sorted_str(X1) ),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_214,plain,
v5_membered(esk7_1(X1)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143]) ).
cnf(i_0_215,plain,
( ~ empty(X1)
| v5_membered(X1) ),
inference(rename_variables,[],[i_0_143]) ).
cnf(i_0_216,plain,
v4_membered(esk7_1(X1)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144]) ).
cnf(i_0_217,plain,
( ~ empty(X1)
| v4_membered(X1) ),
inference(rename_variables,[],[i_0_144]) ).
cnf(i_0_218,plain,
v3_membered(esk7_1(X1)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146]) ).
cnf(i_0_219,plain,
( ~ empty(X1)
| v3_membered(X1) ),
inference(rename_variables,[],[i_0_146]) ).
cnf(i_0_220,plain,
v2_membered(esk7_1(X1)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148]) ).
cnf(i_0_221,plain,
( ~ empty(X1)
| v2_membered(X1) ),
inference(rename_variables,[],[i_0_148]) ).
cnf(i_0_222,plain,
v1_membered(esk7_1(X1)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150]) ).
cnf(i_0_223,plain,
( ~ empty(X1)
| v1_membered(X1) ),
inference(rename_variables,[],[i_0_150]) ).
cnf(i_0_224,plain,
element(interior(esk8_0,esk9_0),powerset(the_carrier(esk8_0))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93]) ).
cnf(i_0_225,plain,
( ~ element(X1,powerset(the_carrier(X2)))
| element(interior(X2,X1),powerset(the_carrier(X2)))
| ~ top_str(X2) ),
inference(rename_variables,[],[i_0_93]) ).
cnf(i_0_226,plain,
~ empty(the_carrier(esk8_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_162,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96]) ).
cnf(i_0_227,plain,
( ~ element(X1,powerset(X2))
| ~ empty(X2)
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_228,plain,
v5_membered(esk4_1(powerset(esk5_0))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_137,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99]) ).
cnf(i_0_229,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_230,plain,
( ~ element(X1,powerset(X2))
| ~ v5_membered(X2)
| v5_membered(X1) ),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_231,plain,
v4_membered(esk4_1(powerset(esk5_0))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_137,i_0_229,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100]) ).
cnf(i_0_232,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_233,plain,
( ~ element(X1,powerset(X2))
| ~ v5_membered(X2)
| v4_membered(X1) ),
inference(rename_variables,[],[i_0_100]) ).
cnf(i_0_234,plain,
v3_membered(esk4_1(powerset(esk5_0))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_137,i_0_229,i_0_232,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102]) ).
cnf(i_0_235,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_236,plain,
( ~ element(X1,powerset(X2))
| ~ v5_membered(X2)
| v3_membered(X1) ),
inference(rename_variables,[],[i_0_102]) ).
cnf(i_0_237,plain,
v2_membered(esk4_1(powerset(esk5_0))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105]) ).
cnf(i_0_238,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_239,plain,
( ~ element(X1,powerset(X2))
| ~ v5_membered(X2)
| v2_membered(X1) ),
inference(rename_variables,[],[i_0_105]) ).
cnf(i_0_240,plain,
v1_membered(esk4_1(powerset(esk5_0))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109]) ).
cnf(i_0_241,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_242,plain,
( ~ element(X1,powerset(X2))
| ~ v5_membered(X2)
| v1_membered(X1) ),
inference(rename_variables,[],[i_0_109]) ).
cnf(i_0_243,plain,
in(esk10_0,the_carrier(esk8_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115]) ).
cnf(i_0_244,plain,
( ~ element(X1,X2)
| empty(X2)
| in(X1,X2) ),
inference(rename_variables,[],[i_0_115]) ).
cnf(i_0_245,plain,
natural(esk4_1(esk5_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117]) ).
cnf(i_0_246,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_247,plain,
( ~ v5_membered(X1)
| natural(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_117]) ).
cnf(i_0_248,plain,
v1_int_1(esk4_1(esk5_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_162,i_0_163,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118]) ).
cnf(i_0_249,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_250,plain,
( ~ v5_membered(X1)
| v1_int_1(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_251,plain,
v1_int_1(esk4_1(empty_set)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119]) ).
cnf(i_0_252,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_253,plain,
( ~ v4_membered(X1)
| v1_int_1(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_254,plain,
v1_rat_1(esk4_1(esk5_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120]) ).
cnf(i_0_255,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_256,plain,
( ~ v5_membered(X1)
| v1_rat_1(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_257,plain,
v1_rat_1(esk4_1(empty_set)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121]) ).
cnf(i_0_258,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_259,plain,
( ~ v4_membered(X1)
| v1_rat_1(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_121]) ).
cnf(i_0_260,plain,
v1_rat_1(esk4_1(esk7_1(X1))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122]) ).
cnf(i_0_261,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_262,plain,
( ~ v3_membered(X1)
| v1_rat_1(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_263,plain,
v1_xreal_0(esk4_1(esk5_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123]) ).
cnf(i_0_264,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_265,plain,
( ~ v5_membered(X1)
| v1_xreal_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_266,plain,
v1_xreal_0(esk4_1(empty_set)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124]) ).
cnf(i_0_267,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_268,plain,
( ~ v4_membered(X1)
| v1_xreal_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_269,plain,
v1_xreal_0(esk4_1(esk7_1(X1))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125]) ).
cnf(i_0_270,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_271,plain,
( ~ v3_membered(X1)
| v1_xreal_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_125]) ).
cnf(i_0_272,plain,
v1_xcmplx_0(esk4_1(esk5_0)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127]) ).
cnf(i_0_273,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_274,plain,
( ~ v5_membered(X1)
| v1_xcmplx_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_127]) ).
cnf(i_0_275,plain,
v1_xcmplx_0(esk4_1(empty_set)),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128]) ).
cnf(i_0_276,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_277,plain,
( ~ v4_membered(X1)
| v1_xcmplx_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_128]) ).
cnf(i_0_278,plain,
v1_xcmplx_0(esk4_1(esk7_1(X1))),
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129]) ).
cnf(i_0_279,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_280,plain,
( ~ v3_membered(X1)
| v1_xcmplx_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_281,plain,
esk9_0 != empty_set,
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179]) ).
cnf(i_0_282,plain,
empty_set != esk5_0,
inference(scs_inference,[],[i_0_153,i_0_159,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201]) ).
cnf(i_0_283,plain,
point_neighbourhood(esk3_2(esk8_0,esk10_0),esk8_0,esk10_0),
inference(scs_inference,[],[i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92]) ).
cnf(i_0_284,plain,
( ~ element(X1,the_carrier(X2))
| point_neighbourhood(esk3_2(X2,X1),X2,X1)
| ~ topological_space(X2)
| ~ top_str(X2)
| empty_carrier(X2) ),
inference(rename_variables,[],[i_0_92]) ).
cnf(i_0_285,plain,
~ in(esk10_0,interior(esk8_0,esk9_0)),
inference(scs_inference,[],[i_0_94,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88]) ).
cnf(i_0_286,plain,
( ~ element(X1,powerset(the_carrier(X2)))
| ~ in(X3,interior(X2,X1))
| ~ element(X3,the_carrier(X2))
| empty_carrier(X2)
| ~ topological_space(X2)
| ~ top_str(X2)
| point_neighbourhood(X1,X2,X3) ),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_287,plain,
interior(esk8_0,esk9_0) = esk9_0,
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91]) ).
cnf(i_0_288,plain,
( ~ element(X1,powerset(the_carrier(X2)))
| ~ element(X3,powerset(the_carrier(X4)))
| interior(X2,X1) = X1
| ~ open_subset(X1,X2)
| ~ top_str(X2)
| ~ topological_space(X4)
| ~ top_str(X4) ),
inference(rename_variables,[],[i_0_91]) ).
cnf(i_0_289,plain,
~ empty(esk9_0),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155]) ).
cnf(i_0_290,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_291,plain,
esk9_0 = interior(esk8_0,esk9_0),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174]) ).
cnf(i_0_292,plain,
( element(X1,X2)
| ~ in(X1,esk7_1(X2)) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95]) ).
cnf(i_0_293,plain,
( ~ element(X1,powerset(X2))
| element(X3,X2)
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_95]) ).
cnf(i_0_294,plain,
( v4_membered(X1)
| ~ in(X1,esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101]) ).
cnf(i_0_295,plain,
( ~ element(X1,powerset(X2))
| ~ v4_membered(X2)
| v4_membered(X1) ),
inference(rename_variables,[],[i_0_101]) ).
cnf(i_0_296,plain,
( v3_membered(esk9_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103]) ).
cnf(i_0_297,plain,
( ~ element(X1,powerset(X2))
| ~ v4_membered(X2)
| v3_membered(X1) ),
inference(rename_variables,[],[i_0_103]) ).
cnf(i_0_298,plain,
( v3_membered(the_carrier(esk8_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104]) ).
cnf(i_0_299,plain,
( ~ element(X1,powerset(X2))
| ~ v3_membered(X2)
| v3_membered(X1) ),
inference(rename_variables,[],[i_0_104]) ).
cnf(i_0_300,plain,
( v2_membered(esk9_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106]) ).
cnf(i_0_301,plain,
( ~ element(X1,powerset(X2))
| ~ v4_membered(X2)
| v2_membered(X1) ),
inference(rename_variables,[],[i_0_106]) ).
cnf(i_0_302,plain,
( v2_membered(interior(esk8_0,esk9_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107]) ).
cnf(i_0_303,plain,
( ~ element(X1,powerset(X2))
| ~ v3_membered(X2)
| v2_membered(X1) ),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_304,plain,
( v2_membered(the_carrier(esk8_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108]) ).
cnf(i_0_305,plain,
( ~ element(X1,powerset(X2))
| ~ v2_membered(X2)
| v2_membered(X1) ),
inference(rename_variables,[],[i_0_108]) ).
cnf(i_0_306,plain,
( v1_membered(esk9_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110]) ).
cnf(i_0_307,plain,
( ~ element(X1,powerset(X2))
| ~ v4_membered(X2)
| v1_membered(X1) ),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_308,plain,
( v1_membered(interior(esk8_0,esk9_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111]) ).
cnf(i_0_309,plain,
( ~ element(X1,powerset(X2))
| ~ v3_membered(X2)
| v1_membered(X1) ),
inference(rename_variables,[],[i_0_111]) ).
cnf(i_0_310,plain,
( v1_membered(the_carrier(esk8_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112]) ).
cnf(i_0_311,plain,
( ~ element(X1,powerset(X2))
| ~ v2_membered(X2)
| v1_membered(X1) ),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_312,plain,
( v1_xreal_0(esk4_1(esk9_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126]) ).
cnf(i_0_313,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_314,plain,
( ~ v2_membered(X1)
| v1_xreal_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_126]) ).
cnf(i_0_315,plain,
( v1_xcmplx_0(esk4_1(esk9_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_313,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126,i_0_130]) ).
cnf(i_0_316,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_317,plain,
( ~ v2_membered(X1)
| v1_xcmplx_0(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_130]) ).
cnf(i_0_318,plain,
( v1_xcmplx_0(esk10_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_313,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126,i_0_130,i_0_131]) ).
cnf(i_0_319,plain,
( ~ element(X1,X2)
| v1_xcmplx_0(X1)
| ~ v1_membered(X2) ),
inference(rename_variables,[],[i_0_131]) ).
cnf(i_0_320,plain,
( ~ in(interior(esk8_0,esk9_0),esk10_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_313,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126,i_0_130,i_0_131,i_0_178]) ).
cnf(i_0_321,plain,
( ~ point_neighbourhood(interior(esk8_0,esk9_0),esk8_0,esk10_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_313,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126,i_0_130,i_0_131,i_0_178,i_0_192]) ).
cnf(i_0_322,plain,
( v3_membered(interior(esk8_0,esk9_0))
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_313,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126,i_0_130,i_0_131,i_0_178,i_0_192,i_0_182]) ).
cnf(i_0_323,plain,
( v5_membered(X1)
| esk5_0 != X1
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(scs_inference,[],[i_0_94,i_0_152,i_0_153,i_0_156,i_0_159,i_0_161,i_0_140,i_0_135,i_0_134,i_0_137,i_0_229,i_0_232,i_0_235,i_0_238,i_0_241,i_0_246,i_0_249,i_0_252,i_0_255,i_0_258,i_0_261,i_0_264,i_0_267,i_0_270,i_0_273,i_0_276,i_0_279,i_0_313,i_0_157,i_0_162,i_0_163,i_0_165,i_0_166,i_0_167,i_0_169,i_0_154,i_0_97,i_0_98,i_0_116,i_0_133,i_0_142,i_0_143,i_0_144,i_0_146,i_0_148,i_0_150,i_0_93,i_0_96,i_0_99,i_0_100,i_0_102,i_0_105,i_0_109,i_0_115,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_127,i_0_128,i_0_129,i_0_179,i_0_201,i_0_92,i_0_88,i_0_91,i_0_155,i_0_174,i_0_95,i_0_101,i_0_103,i_0_104,i_0_106,i_0_107,i_0_108,i_0_110,i_0_111,i_0_112,i_0_126,i_0_130,i_0_131,i_0_178,i_0_192,i_0_182,i_0_180]) ).
cnf(i_0_324,plain,
( v5_membered(esk5_0)
| ~ in(the_carrier(esk8_0),esk7_1(powerset(esk5_0))) ),
inference(equality_inference,[],[323]) ).
cnf(i_0_325,plain,
subset(interior(esk8_0,esk9_0),the_carrier(esk8_0)),
inference(scs_inference,[],[i_0_224,i_0_97]) ).
cnf(i_0_326,plain,
( ~ element(X1,powerset(X2))
| subset(X1,X2) ),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_327,plain,
~ in(the_carrier(esk8_0),esk10_0),
inference(scs_inference,[],[i_0_224,i_0_243,i_0_97,i_0_98]) ).
cnf(i_0_328,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_98]) ).
cnf(i_0_329,plain,
~ in(X1,esk7_1(X2)),
inference(scs_inference,[],[i_0_224,i_0_243,i_0_154,i_0_97,i_0_98,i_0_133]) ).
cnf(i_0_330,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_331,plain,
one_sorted_str(esk1_0),
inference(scs_inference,[],[i_0_224,i_0_243,i_0_160,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142]) ).
cnf(i_0_332,plain,
( ~ top_str(X1)
| one_sorted_str(X1) ),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_333,plain,
~ in(X1,esk4_1(powerset(empty_set))),
inference(scs_inference,[],[i_0_224,i_0_243,i_0_160,i_0_137,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96]) ).
cnf(i_0_334,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_335,plain,
( ~ element(X1,powerset(X2))
| ~ empty(X2)
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_96]) ).
cnf(i_0_336,plain,
in(esk9_0,powerset(the_carrier(esk8_0))),
inference(scs_inference,[],[i_0_135,i_0_224,i_0_243,i_0_160,i_0_137,i_0_138,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96,i_0_115]) ).
cnf(i_0_337,plain,
~ empty(powerset(X1)),
inference(rename_variables,[],[i_0_138]) ).
cnf(i_0_338,plain,
( ~ element(X1,X2)
| empty(X2)
| in(X1,X2) ),
inference(rename_variables,[],[i_0_115]) ).
cnf(i_0_339,plain,
natural(esk4_1(empty_set)),
inference(scs_inference,[],[i_0_135,i_0_224,i_0_243,i_0_160,i_0_137,i_0_334,i_0_164,i_0_138,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96,i_0_115,i_0_117]) ).
cnf(i_0_340,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_341,plain,
( ~ v5_membered(X1)
| natural(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_117]) ).
cnf(i_0_342,plain,
v1_int_1(esk4_1(esk7_1(X1))),
inference(scs_inference,[],[i_0_135,i_0_224,i_0_243,i_0_160,i_0_137,i_0_334,i_0_340,i_0_164,i_0_214,i_0_138,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96,i_0_115,i_0_117,i_0_118]) ).
cnf(i_0_343,plain,
element(esk4_1(X1),X1),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_344,plain,
( ~ v5_membered(X1)
| v1_int_1(X2)
| ~ element(X2,X1) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_345,plain,
element(interior(esk8_0,interior(esk8_0,esk9_0)),powerset(the_carrier(esk8_0))),
inference(scs_inference,[],[i_0_135,i_0_159,i_0_224,i_0_243,i_0_160,i_0_137,i_0_334,i_0_340,i_0_164,i_0_214,i_0_138,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96,i_0_115,i_0_117,i_0_118,i_0_93]) ).
cnf(i_0_346,plain,
( ~ element(X1,powerset(the_carrier(X2)))
| element(interior(X2,X1),powerset(the_carrier(X2)))
| ~ top_str(X2) ),
inference(rename_variables,[],[i_0_93]) ).
cnf(i_0_347,plain,
~ in(interior(esk8_0,esk9_0),esk10_0),
inference(scs_inference,[],[i_0_135,i_0_159,i_0_224,i_0_287,i_0_243,i_0_206,i_0_160,i_0_137,i_0_334,i_0_340,i_0_164,i_0_214,i_0_138,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96,i_0_115,i_0_117,i_0_118,i_0_93,i_0_178]) ).
cnf(i_0_348,plain,
$false,
inference(scs_inference,[],[i_0_135,i_0_153,i_0_159,i_0_224,i_0_287,i_0_285,i_0_243,i_0_206,i_0_291,i_0_160,i_0_137,i_0_334,i_0_340,i_0_164,i_0_214,i_0_138,i_0_162,i_0_154,i_0_97,i_0_98,i_0_133,i_0_142,i_0_96,i_0_115,i_0_117,i_0_118,i_0_93,i_0_178,i_0_179]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU341+1 : TPTP v9.2.1. Released v3.3.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n029.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:58:44 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.43/1.62 % Version : CSE_E---1.7
% 0.43/1.62 % Problem : theBenchmark.p
% 0.43/1.62 % SZS status Theorem for theBenchmark.p
% 0.43/1.62 % SZS output start CNFRefutation
% See solution above
% 1.14/2.36 % Total time : 1.271s
%------------------------------------------------------------------------------