%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : TOP016-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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 : 600s
% DateTime : Thu Jul 21 21:34:57 EDT 2022
% Result : Satisfiable 0.43s 0.61s
% Output : Saturation 0.45s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 114)
% Comments :
%------------------------------------------------------------------------------
cnf(1349,plain,
( ~ element_of_set(u,f16(v,w,x,y))
| ~ limit_point(u,z,x1,x2)
| ~ limit_point(v,z,x,y)
| ~ hausdorff(intersection_of_sets(f16(v,w,x,y),z),x3)
| limit_point(v,w,x,y)
| eq(f15(u,z,x1,x2,f16(v,w,x,y)),f15(v,z,x,y,f16(v,w,x,y))) ),
inference(res,[status(thm),theory(equality)],[577,1348]),
[iquote('6:Res:577.1,1348.0')] ).
cnf(1351,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(intersection_of_sets(f16(u,y,w,x),v),z)
| limit_point(u,y,w,x)
| eq(f15(u,v,w,x,f16(u,y,w,x)),f15(u,v,w,x,f16(u,y,w,x))) ),
inference(obv,[status(thm),theory(equality)],[1350]),
[iquote('6:Obv:1350.3')] ).
cnf(1348,plain,
( ~ neighborhood(f16(u,v,w,x),y,z,x1)
| ~ limit_point(y,x2,z,x1)
| ~ limit_point(u,x2,w,x)
| ~ hausdorff(intersection_of_sets(f16(u,v,w,x),x2),x3)
| limit_point(u,v,w,x)
| eq(f15(y,x2,z,x1,f16(u,v,w,x)),f15(u,x2,w,x,f16(u,v,w,x))) ),
inference(res,[status(thm),theory(equality)],[68,1218]),
[iquote('6:Res:68.2,1218.1')] ).
cnf(1346,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(intersection_of_sets(f16(u,y,w,x),v),z)
| hausdorff(intersection_of_sets(f16(u,y,w,x),v),x1)
| limit_point(u,y,w,x)
| eq(f20(intersection_of_sets(f16(u,y,w,x),v),x1),f15(u,v,w,x,f16(u,y,w,x))) ),
inference(res,[status(thm),theory(equality)],[469,1218]),
[iquote('6:Res:469.1,1218.1')] ).
cnf(1347,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(intersection_of_sets(f16(u,y,w,x),v),z)
| hausdorff(intersection_of_sets(f16(u,y,w,x),v),x1)
| limit_point(u,y,w,x)
| eq(f19(intersection_of_sets(f16(u,y,w,x),v),x1),f15(u,v,w,x,f16(u,y,w,x))) ),
inference(res,[status(thm),theory(equality)],[471,1218]),
[iquote('6:Res:471.1,1218.1')] ).
cnf(1343,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(intersection_of_sets(f16(u,y,w,x),v),z)
| limit_point(u,y,w,x)
| hausdorff(intersection_of_sets(f16(u,y,w,x),v),x1)
| eq(f15(u,v,w,x,f16(u,y,w,x)),f19(intersection_of_sets(f16(u,y,w,x),v),x1)) ),
inference(res,[status(thm),theory(equality)],[586,905]),
[iquote('6:Res:586.1,905.0')] ).
cnf(1337,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(intersection_of_sets(f16(u,y,w,x),v),z)
| limit_point(u,y,w,x)
| hausdorff(intersection_of_sets(f16(u,y,w,x),v),x1)
| eq(f15(u,v,w,x,f16(u,y,w,x)),f20(intersection_of_sets(f16(u,y,w,x),v),x1)) ),
inference(res,[status(thm),theory(equality)],[586,884]),
[iquote('6:Res:586.1,884.0')] ).
cnf(1236,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ neighborhood(z,x1,x2,x3)
| ~ limit_point(x1,x4,x2,x3)
| ~ hausdorff(interior(x5,x6,x7),x8)
| eq(f15(v,y,w,x,u),f15(x1,x4,x2,x3,z)) ),
inference(res,[status(thm),theory(equality)],[738,910]),
[iquote('6:Res:738.2,910.2')] ).
cnf(1218,plain,
( ~ limit_point(u,v,w,x)
| ~ element_of_set(y,intersection_of_sets(f16(u,z,w,x),v))
| ~ hausdorff(intersection_of_sets(f16(u,z,w,x),v),x1)
| limit_point(u,z,w,x)
| eq(y,f15(u,v,w,x,f16(u,z,w,x))) ),
inference(res,[status(thm),theory(equality)],[586,863]),
[iquote('6:Res:586.1,863.0')] ).
cnf(1204,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| ~ hausdorff(f6(v,y,u,w,x),z)
| hausdorff(f6(v,y,u,w,x),x1)
| eq(f20(f6(v,y,u,w,x),x1),u) ),
inference(res,[status(thm),theory(equality)],[469,850]),
[iquote('6:Res:469.1,850.2')] ).
cnf(1205,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| ~ hausdorff(f6(v,y,u,w,x),z)
| hausdorff(f6(v,y,u,w,x),x1)
| eq(f19(f6(v,y,u,w,x),x1),u) ),
inference(res,[status(thm),theory(equality)],[471,850]),
[iquote('6:Res:471.1,850.2')] ).
cnf(892,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| ~ hausdorff(f6(v,y,u,w,x),z)
| hausdorff(f6(v,y,u,w,x),x1)
| eq(u,f19(f6(v,y,u,w,x),x1)) ),
inference(res,[status(thm),theory(equality)],[605,852]),
[iquote('6:Res:605.2,852.0')] ).
cnf(871,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| ~ hausdorff(f6(v,y,u,w,x),z)
| hausdorff(f6(v,y,u,w,x),x1)
| eq(u,f20(f6(v,y,u,w,x),x1)) ),
inference(res,[status(thm),theory(equality)],[605,851]),
[iquote('6:Res:605.2,851.0')] ).
cnf(1342,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ hausdorff(intersection_of_sets(v,w),z)
| hausdorff(intersection_of_sets(v,w),x1)
| eq(f15(u,w,x,y,v),f19(intersection_of_sets(v,w),x1)) ),
inference(res,[status(thm),theory(equality)],[577,905]),
[iquote('6:Res:577.1,905.0')] ).
cnf(905,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(intersection_of_sets(u,y),z)
| hausdorff(intersection_of_sets(u,y),x1)
| eq(f15(v,y,w,x,u),f19(intersection_of_sets(u,y),x1)) ),
inference(res,[status(thm),theory(equality)],[68,852]),
[iquote('6:Res:68.2,852.0')] ).
cnf(1327,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(union_of_members(y),z)
| limit_point(u,x1,w,x)
| limit_point(x2,x3,x4,x5)
| eq(f15(u,v,w,x,f16(u,x1,w,x)),x2) ),
inference(res,[status(thm),theory(equality)],[586,1001]),
[iquote('6:Res:586.1,1001.0')] ).
cnf(1336,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ hausdorff(intersection_of_sets(v,w),z)
| hausdorff(intersection_of_sets(v,w),x1)
| eq(f15(u,w,x,y,v),f20(intersection_of_sets(v,w),x1)) ),
inference(res,[status(thm),theory(equality)],[577,884]),
[iquote('6:Res:577.1,884.0')] ).
cnf(884,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(intersection_of_sets(u,y),z)
| hausdorff(intersection_of_sets(u,y),x1)
| eq(f15(v,y,w,x,u),f20(intersection_of_sets(u,y),x1)) ),
inference(res,[status(thm),theory(equality)],[68,851]),
[iquote('6:Res:68.2,851.0')] ).
cnf(1323,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(union_of_members(y),z)
| limit_point(u,x1,w,x)
| hausdorff(x2,x3)
| eq(f15(u,v,w,x,f16(u,x1,w,x)),f19(x2,x3)) ),
inference(res,[status(thm),theory(equality)],[586,945]),
[iquote('6:Res:586.1,945.0')] ).
cnf(1319,plain,
( ~ limit_point(u,v,w,x)
| ~ hausdorff(union_of_members(y),z)
| limit_point(u,x1,w,x)
| hausdorff(x2,x3)
| eq(f15(u,v,w,x,f16(u,x1,w,x)),f20(x2,x3)) ),
inference(res,[status(thm),theory(equality)],[586,933]),
[iquote('6:Res:586.1,933.0')] ).
cnf(1194,plain,
( ~ limit_point(u,v,w,x)
| ~ element_of_set(y,union_of_members(z))
| ~ hausdorff(union_of_members(z),x1)
| limit_point(u,x2,w,x)
| eq(y,f15(u,v,w,x,f16(u,x2,w,x))) ),
inference(res,[status(thm),theory(equality)],[586,864]),
[iquote('6:Res:586.1,864.0')] ).
cnf(1227,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(interior(z,x1,x2),x3)
| limit_point(x4,x5,x6,x7)
| eq(x4,f15(v,y,w,x,u)) ),
inference(res,[status(thm),theory(equality)],[676,910]),
[iquote('6:Res:676.1,910.2')] ).
cnf(1174,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(interior(z,x1,x2),x3)
| limit_point(x4,x5,x6,x7)
| eq(f15(v,y,w,x,u),x4) ),
inference(res,[status(thm),theory(equality)],[738,846]),
[iquote('6:Res:738.2,846.0')] ).
cnf(1230,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(interior(z,x1,x2),x3)
| hausdorff(x4,x5)
| eq(f20(x4,x5),f15(v,y,w,x,u)) ),
inference(res,[status(thm),theory(equality)],[643,910]),
[iquote('6:Res:643.1,910.2')] ).
cnf(1231,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(interior(z,x1,x2),x3)
| hausdorff(x4,x5)
| eq(f19(x4,x5),f15(v,y,w,x,u)) ),
inference(res,[status(thm),theory(equality)],[644,910]),
[iquote('6:Res:644.1,910.2')] ).
cnf(1164,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(interior(z,x1,x2),x3)
| hausdorff(x4,x5)
| eq(f15(v,y,w,x,u),f20(x4,x5)) ),
inference(res,[status(thm),theory(equality)],[738,857]),
[iquote('6:Res:738.2,857.0')] ).
cnf(1154,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(interior(z,x1,x2),x3)
| hausdorff(x4,x5)
| eq(f15(v,y,w,x,u),f19(x4,x5)) ),
inference(res,[status(thm),theory(equality)],[738,858]),
[iquote('6:Res:738.2,858.0')] ).
cnf(1184,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(f13(v,w,x,u),y)
| hausdorff(f13(v,w,x,u),z)
| eq(f20(f13(v,w,x,u),z),u) ),
inference(res,[status(thm),theory(equality)],[469,847]),
[iquote('6:Res:469.1,847.1')] ).
cnf(1185,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(f13(v,w,x,u),y)
| hausdorff(f13(v,w,x,u),z)
| eq(f19(f13(v,w,x,u),z),u) ),
inference(res,[status(thm),theory(equality)],[471,847]),
[iquote('6:Res:471.1,847.1')] ).
cnf(889,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(f13(v,w,x,u),y)
| hausdorff(f13(v,w,x,u),z)
| eq(u,f19(f13(v,w,x,u),z)) ),
inference(res,[status(thm),theory(equality)],[52,852]),
[iquote('6:Res:52.1,852.0')] ).
cnf(868,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(f13(v,w,x,u),y)
| hausdorff(f13(v,w,x,u),z)
| eq(u,f20(f13(v,w,x,u),z)) ),
inference(res,[status(thm),theory(equality)],[52,851]),
[iquote('6:Res:52.1,851.0')] ).
cnf(1326,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ hausdorff(union_of_members(z),x1)
| limit_point(x2,x3,x4,x5)
| eq(f15(u,w,x,y,v),x2) ),
inference(res,[status(thm),theory(equality)],[577,1001]),
[iquote('6:Res:577.1,1001.0')] ).
cnf(1001,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(union_of_members(z),x1)
| limit_point(x2,x3,x4,x5)
| eq(f15(v,y,w,x,u),x2) ),
inference(res,[status(thm),theory(equality)],[739,844]),
[iquote('6:Res:739.2,844.0')] ).
cnf(1322,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ hausdorff(union_of_members(z),x1)
| hausdorff(x2,x3)
| eq(f15(u,w,x,y,v),f19(x2,x3)) ),
inference(res,[status(thm),theory(equality)],[577,945]),
[iquote('6:Res:577.1,945.0')] ).
cnf(945,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(union_of_members(z),x1)
| hausdorff(x2,x3)
| eq(f15(v,y,w,x,u),f19(x2,x3)) ),
inference(res,[status(thm),theory(equality)],[739,854]),
[iquote('6:Res:739.2,854.0')] ).
cnf(1318,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ hausdorff(union_of_members(z),x1)
| hausdorff(x2,x3)
| eq(f15(u,w,x,y,v),f20(x2,x3)) ),
inference(res,[status(thm),theory(equality)],[577,933]),
[iquote('6:Res:577.1,933.0')] ).
cnf(933,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ hausdorff(union_of_members(z),x1)
| hausdorff(x2,x3)
| eq(f15(v,y,w,x,u),f20(x2,x3)) ),
inference(res,[status(thm),theory(equality)],[739,853]),
[iquote('6:Res:739.2,853.0')] ).
cnf(1217,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ element_of_set(z,intersection_of_sets(v,w))
| ~ hausdorff(intersection_of_sets(v,w),x1)
| eq(z,f15(u,w,x,y,v)) ),
inference(res,[status(thm),theory(equality)],[577,863]),
[iquote('6:Res:577.1,863.0')] ).
cnf(1176,plain,
( ~ hausdorff(f16(u,v,w,x),y)
| hausdorff(f16(u,v,w,x),z)
| limit_point(u,v,w,x)
| eq(f20(f16(u,v,w,x),z),u) ),
inference(res,[status(thm),theory(equality)],[469,849]),
[iquote('6:Res:469.1,849.0')] ).
cnf(1177,plain,
( ~ hausdorff(f16(u,v,w,x),y)
| hausdorff(f16(u,v,w,x),z)
| limit_point(u,v,w,x)
| eq(f19(f16(u,v,w,x),z),u) ),
inference(res,[status(thm),theory(equality)],[471,849]),
[iquote('6:Res:471.1,849.0')] ).
cnf(891,plain,
( ~ hausdorff(f16(u,v,w,x),y)
| limit_point(u,v,w,x)
| hausdorff(f16(u,v,w,x),z)
| eq(u,f19(f16(u,v,w,x),z)) ),
inference(res,[status(thm),theory(equality)],[675,852]),
[iquote('6:Res:675.1,852.0')] ).
cnf(1311,plain,
hausdorff(closure(u,v,w),x),
inference(obv,[status(thm),theory(equality)],[1310]),
[iquote('6:Obv:1310.1')] ).
cnf(870,plain,
( ~ hausdorff(f16(u,v,w,x),y)
| limit_point(u,v,w,x)
| hausdorff(f16(u,v,w,x),z)
| eq(u,f20(f16(u,v,w,x),z)) ),
inference(res,[status(thm),theory(equality)],[675,851]),
[iquote('6:Res:675.1,851.0')] ).
cnf(1294,plain,
hausdorff(boundary(u,v,w),x),
inference(obv,[status(thm),theory(equality)],[1293]),
[iquote('6:Obv:1293.1')] ).
cnf(1193,plain,
( ~ element_of_set(u,v)
| ~ limit_point(u,w,x,y)
| ~ element_of_set(z,union_of_members(x1))
| ~ hausdorff(union_of_members(x1),x2)
| eq(z,f15(u,w,x,y,v)) ),
inference(res,[status(thm),theory(equality)],[577,864]),
[iquote('6:Res:577.1,864.0')] ).
cnf(1058,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(f10(w,v,u),x)
| hausdorff(f10(w,v,u),y)
| eq(f20(f10(w,v,u),y),u) ),
inference(res,[status(thm),theory(equality)],[469,848]),
[iquote('6:Res:469.1,848.1')] ).
cnf(1059,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(f10(w,v,u),x)
| hausdorff(f10(w,v,u),y)
| eq(f19(f10(w,v,u),y),u) ),
inference(res,[status(thm),theory(equality)],[471,848]),
[iquote('6:Res:471.1,848.1')] ).
cnf(890,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(f10(w,v,u),x)
| hausdorff(f10(w,v,u),y)
| eq(u,f19(f10(w,v,u),y)) ),
inference(res,[status(thm),theory(equality)],[537,852]),
[iquote('6:Res:537.1,852.0')] ).
cnf(869,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(f10(w,v,u),x)
| hausdorff(f10(w,v,u),y)
| eq(u,f20(f10(w,v,u),y)) ),
inference(res,[status(thm),theory(equality)],[537,851]),
[iquote('6:Res:537.1,851.0')] ).
cnf(910,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ element_of_set(z,interior(x1,x2,x3))
| ~ hausdorff(interior(x1,x2,x3),x4)
| eq(z,f15(v,y,w,x,u)) ),
inference(res,[status(thm),theory(equality)],[738,843]),
[iquote('6:Res:738.2,843.0')] ).
cnf(863,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ element_of_set(z,intersection_of_sets(u,y))
| ~ hausdorff(intersection_of_sets(u,y),x1)
| eq(z,f15(v,y,w,x,u)) ),
inference(res,[status(thm),theory(equality)],[68,843]),
[iquote('6:Res:68.2,843.0')] ).
cnf(1210,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| ~ hausdorff(f6(v,y,u,w,x),z)
| eq(u,u) ),
inference(obv,[status(thm),theory(equality)],[1203]),
[iquote('6:Obv:1203.1')] ).
cnf(850,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| ~ element_of_set(y,f6(v,z,u,w,x))
| ~ hausdorff(f6(v,z,u,w,x),x1)
| eq(y,u) ),
inference(res,[status(thm),theory(equality)],[605,843]),
[iquote('6:Res:605.2,843.0')] ).
cnf(864,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| ~ element_of_set(z,union_of_members(x1))
| ~ hausdorff(union_of_members(x1),x2)
| eq(z,f15(v,y,w,x,u)) ),
inference(res,[status(thm),theory(equality)],[739,843]),
[iquote('6:Res:739.2,843.0')] ).
cnf(1038,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(f1(v,u),w)
| hausdorff(f1(v,u),x)
| eq(f20(f1(v,u),x),u) ),
inference(res,[status(thm),theory(equality)],[469,845]),
[iquote('6:Res:469.1,845.1')] ).
cnf(1039,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(f1(v,u),w)
| hausdorff(f1(v,u),x)
| eq(f19(f1(v,u),x),u) ),
inference(res,[status(thm),theory(equality)],[471,845]),
[iquote('6:Res:471.1,845.1')] ).
cnf(1190,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(f13(v,w,x,u),y)
| eq(u,u) ),
inference(obv,[status(thm),theory(equality)],[1183]),
[iquote('6:Obv:1183.0')] ).
cnf(847,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ element_of_set(y,f13(v,w,x,u))
| ~ hausdorff(f13(v,w,x,u),z)
| eq(y,u) ),
inference(res,[status(thm),theory(equality)],[52,843]),
[iquote('6:Res:52.1,843.0')] ).
cnf(887,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(f1(v,u),w)
| hausdorff(f1(v,u),x)
| eq(u,f19(f1(v,u),x)) ),
inference(res,[status(thm),theory(equality)],[4,852]),
[iquote('6:Res:4.1,852.0')] ).
cnf(866,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(f1(v,u),w)
| hausdorff(f1(v,u),x)
| eq(u,f20(f1(v,u),x)) ),
inference(res,[status(thm),theory(equality)],[4,851]),
[iquote('6:Res:4.1,851.0')] ).
cnf(1165,plain,
( ~ hausdorff(interior(u,v,w),x)
| limit_point(y,z,x1,x2)
| limit_point(x3,x4,x5,x6)
| eq(y,x3) ),
inference(res,[status(thm),theory(equality)],[676,846]),
[iquote('6:Res:676.1,846.0')] ).
cnf(1182,plain,
( ~ hausdorff(f16(u,v,w,x),y)
| limit_point(u,v,w,x)
| eq(u,u) ),
inference(obv,[status(thm),theory(equality)],[1175]),
[iquote('6:Obv:1175.1')] ).
cnf(849,plain,
( ~ element_of_set(u,f16(v,w,x,y))
| ~ hausdorff(f16(v,w,x,y),z)
| limit_point(v,w,x,y)
| eq(u,v) ),
inference(res,[status(thm),theory(equality)],[675,843]),
[iquote('6:Res:675.1,843.0')] ).
cnf(1168,plain,
( ~ hausdorff(interior(u,v,w),x)
| hausdorff(y,z)
| limit_point(x1,x2,x3,x4)
| eq(f20(y,z),x1) ),
inference(res,[status(thm),theory(equality)],[643,846]),
[iquote('6:Res:643.1,846.0')] ).
cnf(1169,plain,
( ~ hausdorff(interior(u,v,w),x)
| hausdorff(y,z)
| limit_point(x1,x2,x3,x4)
| eq(f19(y,z),x1) ),
inference(res,[status(thm),theory(equality)],[644,846]),
[iquote('6:Res:644.1,846.0')] ).
cnf(846,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(interior(v,w,x),y)
| limit_point(z,x1,x2,x3)
| eq(u,z) ),
inference(res,[status(thm),theory(equality)],[676,843]),
[iquote('6:Res:676.1,843.0')] ).
cnf(1155,plain,
( ~ hausdorff(interior(u,v,w),x)
| limit_point(y,z,x1,x2)
| hausdorff(x3,x4)
| eq(y,f20(x3,x4)) ),
inference(res,[status(thm),theory(equality)],[676,857]),
[iquote('6:Res:676.1,857.0')] ).
cnf(814,plain,
( ~ element_of_set(f20(u,v),w)
| ~ element_of_set(f20(u,v),intersection_of_sets(x,y))
| ~ disjoint_s(union_of_members(z),f6(w,x1,f20(u,v),x,y))
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[605,764]),
[iquote('4:Res:605.2,764.0')] ).
cnf(1158,plain,
( ~ hausdorff(interior(u,v,w),x)
| hausdorff(y,z)
| hausdorff(x1,x2)
| eq(f20(y,z),f20(x1,x2)) ),
inference(res,[status(thm),theory(equality)],[643,857]),
[iquote('6:Res:643.1,857.0')] ).
cnf(1159,plain,
( ~ hausdorff(interior(u,v,w),x)
| hausdorff(y,z)
| hausdorff(x1,x2)
| eq(f19(y,z),f20(x1,x2)) ),
inference(res,[status(thm),theory(equality)],[644,857]),
[iquote('6:Res:644.1,857.0')] ).
cnf(857,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(interior(v,w,x),y)
| hausdorff(z,x1)
| eq(u,f20(z,x1)) ),
inference(res,[status(thm),theory(equality)],[643,843]),
[iquote('6:Res:643.1,843.0')] ).
cnf(1145,plain,
( ~ hausdorff(interior(u,v,w),x)
| limit_point(y,z,x1,x2)
| hausdorff(x3,x4)
| eq(y,f19(x3,x4)) ),
inference(res,[status(thm),theory(equality)],[676,858]),
[iquote('6:Res:676.1,858.0')] ).
cnf(790,plain,
( ~ element_of_set(f20(u,v),w)
| ~ element_of_set(f20(u,v),intersection_of_sets(x,y))
| ~ disjoint_s(u,f6(w,z,f20(u,v),x,y))
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[605,763]),
[iquote('4:Res:605.2,763.0')] ).
cnf(1148,plain,
( ~ hausdorff(interior(u,v,w),x)
| hausdorff(y,z)
| hausdorff(x1,x2)
| eq(f20(y,z),f19(x1,x2)) ),
inference(res,[status(thm),theory(equality)],[643,858]),
[iquote('6:Res:643.1,858.0')] ).
cnf(1149,plain,
( ~ hausdorff(interior(u,v,w),x)
| hausdorff(y,z)
| hausdorff(x1,x2)
| eq(f19(y,z),f19(x1,x2)) ),
inference(res,[status(thm),theory(equality)],[644,858]),
[iquote('6:Res:644.1,858.0')] ).
cnf(858,plain,
( ~ element_of_set(u,interior(v,w,x))
| ~ hausdorff(interior(v,w,x),y)
| hausdorff(z,x1)
| eq(u,f19(z,x1)) ),
inference(res,[status(thm),theory(equality)],[644,843]),
[iquote('6:Res:644.1,843.0')] ).
cnf(756,plain,
( ~ element_of_set(f19(u,v),w)
| ~ element_of_set(f19(u,v),intersection_of_sets(x,y))
| ~ element_of_set(f20(u,v),z)
| ~ disjoint_s(f6(w,x1,f19(u,v),x,y),z)
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[605,748]),
[iquote('4:Res:605.2,748.0')] ).
cnf(813,plain,
( ~ disjoint_s(union_of_members(u),f16(f20(v,w),x,y,z))
| limit_point(f20(v,w),x,y,z)
| hausdorff(v,w) ),
inference(res,[status(thm),theory(equality)],[675,764]),
[iquote('4:Res:675.1,764.0')] ).
cnf(755,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(f16(f19(u,v),x,y,z),w)
| limit_point(f19(u,v),x,y,z)
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[675,748]),
[iquote('4:Res:675.1,748.0')] ).
cnf(1064,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(f10(w,v,u),x)
| eq(u,u) ),
inference(obv,[status(thm),theory(equality)],[1057]),
[iquote('6:Obv:1057.0')] ).
cnf(848,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(w,f10(x,v,u))
| ~ hausdorff(f10(x,v,u),y)
| eq(w,u) ),
inference(res,[status(thm),theory(equality)],[537,843]),
[iquote('6:Res:537.1,843.0')] ).
cnf(1056,plain,
( ~ subset_collections(u,f24(v,u))
| ~ compact_space(w,f24(v,u))
| compact_space(v,u) ),
inference(res,[status(thm),theory(equality)],[578,1055]),
[iquote('4:Res:578.1,1055.1')] ).
cnf(1055,plain,
( ~ compact_space(u,f24(v,w))
| ~ open_covering(w,u,f24(v,w))
| compact_space(v,w) ),
inference(obv,[status(thm),theory(equality)],[1054]),
[iquote('4:Obv:1054.1')] ).
cnf(1035,plain,
( ~ subset_collections(f23(u,f24(v,w),x),w)
| ~ compact_space(u,f24(v,w))
| ~ open_covering(x,u,f24(v,w))
| compact_space(v,w) ),
inference(res,[status(thm),theory(equality)],[578,708]),
[iquote('4:Res:578.1,708.2')] ).
cnf(1049,plain,
hausdorff(intersection_of_members(u),v),
inference(obv,[status(thm),theory(equality)],[1048]),
[iquote('6:Obv:1048.1')] ).
cnf(789,plain,
( ~ disjoint_s(u,f16(f20(u,v),w,x,y))
| limit_point(f20(u,v),w,x,y)
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[675,763]),
[iquote('4:Res:675.1,763.0')] ).
cnf(754,plain,
( ~ element_of_set(f19(u,v),w)
| ~ element_of_set(f20(u,v),x)
| ~ disjoint_s(f10(y,w,f19(u,v)),x)
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[537,748]),
[iquote('4:Res:537.1,748.0')] ).
cnf(1046,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(f1(v,u),w)
| eq(u,u) ),
inference(obv,[status(thm),theory(equality)],[1037]),
[iquote('6:Obv:1037.0')] ).
cnf(845,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ element_of_set(w,f1(v,u))
| ~ hausdorff(f1(v,u),x)
| eq(w,u) ),
inference(res,[status(thm),theory(equality)],[4,843]),
[iquote('6:Res:4.1,843.0')] ).
cnf(773,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(f13(x,y,z,f19(u,v)),w)
| hausdorff(u,v) ),
inference(mrr,[status(thm)],[753,644]),
[iquote('4:MRR:753.0,644.1')] ).
cnf(708,plain,
( ~ compact_space(u,f24(v,w))
| ~ open_covering(x,u,f24(v,w))
| ~ open_covering(f23(u,f24(v,w),x),v,w)
| compact_space(v,w) ),
inference(mrr,[status(thm)],[706,104]),
[iquote('0:MRR:706.0,104.2')] ).
cnf(1031,plain,
( ~ compact_set(u,v,w)
| compact_space(x,subspace_topology(v,w,u)) ),
inference(res,[status(thm),theory(equality)],[111,1029]),
[iquote('4:Res:111.1,1029.0')] ).
cnf(1030,plain,
compact_space(u,ct),
inference(res,[status(thm),theory(equality)],[185,1029]),
[iquote('4:Res:185.0,1029.0')] ).
cnf(1029,plain,
( ~ compact_space(u,v)
| compact_space(w,v) ),
inference(mrr,[status(thm)],[1028,473]),
[iquote('4:MRR:1028.0,473.1')] ).
cnf(919,plain,
( ~ subset_collections(f23(u,v,f24(w,x)),x)
| ~ compact_space(u,v)
| ~ open_covering(f24(w,x),u,v)
| compact_space(w,x) ),
inference(res,[status(thm),theory(equality)],[578,707]),
[iquote('4:Res:578.1,707.2')] ).
cnf(1010,plain,
( ~ limit_point(u,v,w,x)
| limit_point(u,v,y,z) ),
inference(mrr,[status(thm)],[1008,675]),
[iquote('4:MRR:1008.0,675.1')] ).
cnf(740,plain,
( ~ neighborhood(f16(u,v,w,x),y,z,x1)
| ~ limit_point(y,v,z,x1)
| eq(f15(y,v,z,x1,f16(u,v,w,x)),u)
| limit_point(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[68,594]),
[iquote('4:Res:68.2,594.0')] ).
cnf(990,plain,
( ~ hausdorff(union_of_members(u),v)
| limit_point(w,x,y,z)
| limit_point(x1,x2,x3,x4)
| eq(w,x1) ),
inference(res,[status(thm),theory(equality)],[677,844]),
[iquote('6:Res:677.1,844.0')] ).
cnf(994,plain,
( ~ hausdorff(union_of_members(u),v)
| hausdorff(w,x)
| limit_point(y,z,x1,x2)
| eq(f19(w,x),y) ),
inference(res,[status(thm),theory(equality)],[616,844]),
[iquote('6:Res:616.1,844.0')] ).
cnf(993,plain,
( ~ hausdorff(union_of_members(u),v)
| hausdorff(w,x)
| limit_point(y,z,x1,x2)
| eq(f20(w,x),y) ),
inference(res,[status(thm),theory(equality)],[613,844]),
[iquote('6:Res:613.1,844.0')] ).
cnf(934,plain,
( ~ hausdorff(union_of_members(u),v)
| limit_point(w,x,y,z)
| hausdorff(x1,x2)
| eq(w,f19(x1,x2)) ),
inference(res,[status(thm),theory(equality)],[677,854]),
[iquote('6:Res:677.1,854.0')] ).
cnf(747,plain,
( ~ disjoint_s(u,f16(f20(v,w),x,v,w))
| ~ neighborhood(u,f19(v,w),v,w)
| limit_point(f20(v,w),x,v,w)
| hausdorff(v,w) ),
inference(res,[status(thm),theory(equality)],[586,118]),
[iquote('4:Res:586.1,118.1')] ).
cnf(922,plain,
( ~ hausdorff(union_of_members(u),v)
| limit_point(w,x,y,z)
| hausdorff(x1,x2)
| eq(w,f20(x1,x2)) ),
inference(res,[status(thm),theory(equality)],[677,853]),
[iquote('6:Res:677.1,853.0')] ).
cnf(938,plain,
( ~ hausdorff(union_of_members(u),v)
| hausdorff(w,x)
| hausdorff(y,z)
| eq(f19(w,x),f19(y,z)) ),
inference(res,[status(thm),theory(equality)],[616,854]),
[iquote('6:Res:616.1,854.0')] ).
cnf(937,plain,
( ~ hausdorff(union_of_members(u),v)
| hausdorff(w,x)
| hausdorff(y,z)
| eq(f20(w,x),f19(y,z)) ),
inference(res,[status(thm),theory(equality)],[613,854]),
[iquote('6:Res:613.1,854.0')] ).
cnf(926,plain,
( ~ hausdorff(union_of_members(u),v)
| hausdorff(w,x)
| hausdorff(y,z)
| eq(f19(w,x),f20(y,z)) ),
inference(res,[status(thm),theory(equality)],[616,853]),
[iquote('6:Res:616.1,853.0')] ).
cnf(713,plain,
( hausdorff(intersection_of_sets(f16(u,v,w,x),v),y)
| eq(f20(intersection_of_sets(f16(u,v,w,x),v),y),u)
| limit_point(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[469,594]),
[iquote('4:Res:469.1,594.0')] ).
cnf(925,plain,
( ~ hausdorff(union_of_members(u),v)
| hausdorff(w,x)
| hausdorff(y,z)
| eq(f20(w,x),f20(y,z)) ),
inference(res,[status(thm),theory(equality)],[613,853]),
[iquote('6:Res:613.1,853.0')] ).
cnf(844,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(union_of_members(v),w)
| limit_point(x,y,z,x1)
| eq(u,x) ),
inference(res,[status(thm),theory(equality)],[677,843]),
[iquote('6:Res:677.1,843.0')] ).
cnf(714,plain,
( hausdorff(intersection_of_sets(f16(u,v,w,x),v),y)
| eq(f19(intersection_of_sets(f16(u,v,w,x),v),y),u)
| limit_point(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[471,594]),
[iquote('4:Res:471.1,594.0')] ).
cnf(854,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(union_of_members(v),w)
| hausdorff(x,y)
| eq(u,f19(x,y)) ),
inference(res,[status(thm),theory(equality)],[616,843]),
[iquote('6:Res:616.1,843.0')] ).
cnf(853,plain,
( ~ element_of_set(u,union_of_members(v))
| ~ hausdorff(union_of_members(v),w)
| hausdorff(x,y)
| eq(u,f20(x,y)) ),
inference(res,[status(thm),theory(equality)],[613,843]),
[iquote('6:Res:613.1,843.0')] ).
cnf(894,plain,
( ~ hausdorff(u,v)
| hausdorff(u,w)
| hausdorff(u,x)
| eq(f19(u,w),f19(u,x)) ),
inference(res,[status(thm),theory(equality)],[471,852]),
[iquote('6:Res:471.1,852.0')] ).
cnf(893,plain,
( ~ hausdorff(u,v)
| hausdorff(u,w)
| hausdorff(u,x)
| eq(f20(u,w),f19(u,x)) ),
inference(res,[status(thm),theory(equality)],[469,852]),
[iquote('6:Res:469.1,852.0')] ).
cnf(707,plain,
( ~ compact_space(u,v)
| ~ open_covering(f24(w,x),u,v)
| ~ open_covering(f23(u,v,f24(w,x)),w,x)
| compact_space(w,x) ),
inference(mrr,[status(thm)],[704,104]),
[iquote('0:MRR:704.0,104.2')] ).
cnf(915,plain,
hausdorff(cx,u),
inference(obv,[status(thm),theory(equality)],[914]),
[iquote('6:Obv:914.1')] ).
cnf(873,plain,
( ~ hausdorff(u,v)
| hausdorff(u,w)
| hausdorff(u,x)
| eq(f19(u,w),f20(u,x)) ),
inference(res,[status(thm),theory(equality)],[471,851]),
[iquote('6:Res:471.1,851.0')] ).
cnf(738,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| element_of_set(f15(v,y,w,x,u),interior(z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[68,584]),
[iquote('4:Res:68.2,584.0')] ).
cnf(872,plain,
( ~ hausdorff(u,v)
| hausdorff(u,w)
| hausdorff(u,x)
| eq(f20(u,w),f20(u,x)) ),
inference(res,[status(thm),theory(equality)],[469,851]),
[iquote('6:Res:469.1,851.0')] ).
cnf(852,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(v,w)
| hausdorff(v,x)
| eq(u,f19(v,x)) ),
inference(res,[status(thm),theory(equality)],[471,843]),
[iquote('6:Res:471.1,843.0')] ).
cnf(851,plain,
( ~ element_of_set(u,v)
| ~ hausdorff(v,w)
| hausdorff(v,x)
| eq(u,f20(v,x)) ),
inference(res,[status(thm),theory(equality)],[469,843]),
[iquote('6:Res:469.1,843.0')] ).
cnf(843,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(w,v)
| ~ hausdorff(v,x)
| eq(w,u) ),
inference(spt,[],[832]),
[iquote('6:Spt:832.0,832.1,832.2,832.3')] ).
cnf(812,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(union_of_members(x),f10(y,w,f20(u,v)))
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[537,764]),
[iquote('4:Res:537.1,764.0')] ).
cnf(788,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(u,f10(x,w,f20(u,v)))
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[537,763]),
[iquote('4:Res:537.1,763.0')] ).
cnf(768,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(f1(x,f19(u,v)),w)
| hausdorff(u,v) ),
inference(mrr,[status(thm)],[751,616]),
[iquote('4:MRR:751.0,616.1')] ).
cnf(767,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(interior(x,y,z),w)
| hausdorff(u,v) ),
inference(obv,[status(thm),theory(equality)],[760]),
[iquote('4:Obv:760.2')] ).
cnf(828,plain,
( ~ disjoint_s(union_of_members(u),f13(v,w,x,f20(y,z)))
| hausdorff(y,z) ),
inference(mrr,[status(thm)],[811,643]),
[iquote('4:MRR:811.0,643.1')] ).
cnf(827,plain,
( ~ disjoint_s(union_of_members(u),f1(v,f20(w,x)))
| hausdorff(w,x) ),
inference(mrr,[status(thm)],[809,613]),
[iquote('4:MRR:809.0,613.1')] ).
cnf(824,plain,
( ~ disjoint_s(union_of_members(u),interior(v,w,x))
| hausdorff(y,z) ),
inference(obv,[status(thm),theory(equality)],[818]),
[iquote('4:Obv:818.1')] ).
cnf(822,plain,
( ~ disjoint_s(union_of_members(u),union_of_members(v))
| hausdorff(w,x) ),
inference(obv,[status(thm),theory(equality)],[816]),
[iquote('4:Obv:816.1')] ).
cnf(821,plain,
( ~ disjoint_s(union_of_members(u),v)
| hausdorff(v,w) ),
inference(obv,[status(thm),theory(equality)],[815]),
[iquote('4:Obv:815.1')] ).
cnf(764,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(union_of_members(x),w)
| hausdorff(u,v) ),
inference(obv,[status(thm),theory(equality)],[758]),
[iquote('4:Obv:758.2')] ).
cnf(804,plain,
( ~ disjoint_s(u,f13(v,w,x,f20(u,y)))
| hausdorff(u,y) ),
inference(mrr,[status(thm)],[787,643]),
[iquote('4:MRR:787.0,643.1')] ).
cnf(801,plain,
( ~ disjoint_s(u,f1(v,f20(u,w)))
| hausdorff(u,w) ),
inference(mrr,[status(thm)],[785,613]),
[iquote('4:MRR:785.0,613.1')] ).
cnf(800,plain,
( ~ disjoint_s(u,interior(v,w,x))
| hausdorff(u,y) ),
inference(obv,[status(thm),theory(equality)],[794]),
[iquote('4:Obv:794.1')] ).
cnf(798,plain,
( ~ disjoint_s(u,union_of_members(v))
| hausdorff(u,w) ),
inference(obv,[status(thm),theory(equality)],[792]),
[iquote('4:Obv:792.1')] ).
cnf(797,plain,
( ~ disjoint_s(u,u)
| hausdorff(u,v) ),
inference(obv,[status(thm),theory(equality)],[791]),
[iquote('4:Obv:791.1')] ).
cnf(763,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(u,w)
| hausdorff(u,v) ),
inference(obv,[status(thm),theory(equality)],[757]),
[iquote('4:Obv:757.2')] ).
cnf(779,plain,
( ~ disjoint_s(u,v)
| equal_sets(v,empty_set)
| equal_sets(u,empty_set) ),
inference(mrr,[status(thm)],[733,775]),
[iquote('5:MRR:733.1,775.0')] ).
cnf(776,plain,
~ separation(u,v,w,x),
inference(mrr,[status(thm)],[93,775]),
[iquote('5:MRR:93.0,775.0')] ).
cnf(777,plain,
connected_set(u,v,w),
inference(mrr,[status(thm)],[582,775]),
[iquote('5:MRR:582.0,775.0')] ).
cnf(775,plain,
connected_space(u,v),
inference(spt,[],[774]),
[iquote('5:Spt:774.0')] ).
cnf(748,plain,
( ~ element_of_set(f19(u,v),w)
| ~ element_of_set(f20(u,v),x)
| ~ disjoint_s(w,x)
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[577,746]),
[iquote('4:Res:577.1,746.2')] ).
cnf(746,plain,
( ~ element_of_set(f20(u,v),w)
| ~ disjoint_s(x,w)
| ~ neighborhood(x,f19(u,v),u,v)
| hausdorff(u,v) ),
inference(res,[status(thm),theory(equality)],[577,118]),
[iquote('4:Res:577.1,118.1')] ).
cnf(118,plain,
( ~ disjoint_s(u,v)
| ~ neighborhood(v,f20(w,x),w,x)
| ~ neighborhood(u,f19(w,x),w,x)
| hausdorff(w,x) ),
inference(mrr,[status(thm)],[83,62]),
[iquote('0:MRR:83.0,62.1')] ).
cnf(739,plain,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| element_of_set(f15(v,y,w,x,u),union_of_members(z)) ),
inference(res,[status(thm),theory(equality)],[68,470]),
[iquote('4:Res:68.2,470.0')] ).
cnf(68,axiom,
( ~ neighborhood(u,v,w,x)
| ~ limit_point(v,y,w,x)
| element_of_set(f15(v,y,w,x,u),intersection_of_sets(u,y)) ),
file('TOP016-1.p',unknown),
[] ).
cnf(69,axiom,
( ~ eq(f15(u,v,w,x,y),u)
| ~ neighborhood(y,u,w,x)
| ~ limit_point(u,v,w,x) ),
file('TOP016-1.p',unknown),
[] ).
cnf(594,plain,
( ~ element_of_set(u,intersection_of_sets(f16(v,w,x,y),w))
| eq(u,v)
| limit_point(v,w,x,y) ),
inference(mrr,[status(thm)],[503,481]),
[iquote('4:MRR:503.0,481.0')] ).
cnf(605,plain,
( ~ element_of_set(u,v)
| ~ element_of_set(u,intersection_of_sets(w,x))
| element_of_set(u,f6(v,y,u,w,x)) ),
inference(mrr,[status(thm)],[539,596]),
[iquote('4:MRR:539.1,596.0')] ).
cnf(115,plain,
( ~ finite(u)
| ~ subset_collections(u,f24(v,w))
| ~ open_covering(u,v,w)
| compact_space(v,w) ),
inference(mrr,[status(thm)],[108,99]),
[iquote('0:MRR:108.1,99.1')] ).
cnf(689,plain,
( ~ compact_space(u,v)
| ~ open_covering(w,u,v)
| subset_collections(f23(u,v,w),v) ),
inference(res,[status(thm),theory(equality)],[106,100]),
[iquote('0:Res:106.2,100.0')] ).
cnf(106,axiom,
( ~ compact_space(u,v)
| ~ open_covering(w,u,v)
| open_covering(f23(u,v,w),u,v) ),
file('TOP016-1.p',unknown),
[] ).
cnf(676,plain,
( limit_point(u,v,w,x)
| element_of_set(u,interior(y,z,x1)) ),
inference(res,[status(thm),theory(equality)],[675,584]),
[iquote('4:Res:675.1,584.0')] ).
cnf(677,plain,
( limit_point(u,v,w,x)
| element_of_set(u,union_of_members(y)) ),
inference(res,[status(thm),theory(equality)],[675,470]),
[iquote('4:Res:675.1,470.0')] ).
cnf(675,plain,
( limit_point(u,v,w,x)
| element_of_set(u,f16(u,v,w,x)) ),
inference(res,[status(thm),theory(equality)],[586,64]),
[iquote('4:Res:586.1,64.0')] ).
cnf(586,plain,
( limit_point(u,v,w,x)
| neighborhood(f16(u,v,w,x),u,w,x) ),
inference(mrr,[status(thm)],[500,481]),
[iquote('4:MRR:500.0,481.0')] ).
cnf(587,plain,
( ~ element_of_set(u,f14(v,w,x,u))
| element_of_set(u,closure(v,w,x)) ),
inference(mrr,[status(thm)],[501,481]),
[iquote('4:MRR:501.0,481.0')] ).
cnf(644,plain,
( hausdorff(u,v)
| element_of_set(f19(u,v),interior(w,x,y)) ),
inference(res,[status(thm),theory(equality)],[471,584]),
[iquote('4:Res:471.1,584.0')] ).
cnf(643,plain,
( hausdorff(u,v)
| element_of_set(f20(u,v),interior(w,x,y)) ),
inference(res,[status(thm),theory(equality)],[469,584]),
[iquote('4:Res:469.1,584.0')] ).
cnf(581,plain,
( ~ compact_space(u,subspace_topology(v,w,u))
| compact_set(u,v,w) ),
inference(mrr,[status(thm)],[497,481]),
[iquote('4:MRR:497.0,481.0')] ).
cnf(476,plain,
( ~ eq(f19(u,v),f20(u,v))
| hausdorff(u,v) ),
inference(mrr,[status(thm)],[82,464]),
[iquote('4:MRR:82.0,464.0')] ).
cnf(633,plain,
( ~ element_of_set(u,boundary(v,w,x))
| element_of_set(u,y) ),
inference(res,[status(thm),theory(equality)],[74,583]),
[iquote('4:Res:74.1,583.0')] ).
cnf(584,plain,
( ~ element_of_set(u,v)
| element_of_set(u,interior(w,x,y)) ),
inference(mrr,[status(thm)],[559,576]),
[iquote('4:MRR:559.1,576.0')] ).
cnf(583,plain,
( ~ element_of_set(u,closure(v,w,x))
| element_of_set(u,y) ),
inference(mrr,[status(thm)],[558,480]),
[iquote('4:MRR:558.1,480.0')] ).
cnf(537,plain,
( ~ element_of_set(u,v)
| element_of_set(u,f10(w,v,u)) ),
inference(mrr,[status(thm)],[40,467]),
[iquote('4:MRR:40.1,467.0')] ).
cnf(577,plain,
( ~ element_of_set(u,v)
| neighborhood(v,u,w,x) ),
inference(mrr,[status(thm)],[114,576]),
[iquote('4:MRR:114.1,576.0')] ).
cnf(542,plain,
equal_sets(u,intersection_of_sets(v,f12(w,x,v,u))),
inference(mrr,[status(thm)],[48,467]),
[iquote('4:MRR:48.0,467.0')] ).
cnf(616,plain,
( hausdorff(u,v)
| element_of_set(f19(u,v),union_of_members(w)) ),
inference(res,[status(thm),theory(equality)],[471,470]),
[iquote('4:Res:471.1,470.0')] ).
cnf(613,plain,
( hausdorff(u,v)
| element_of_set(f20(u,v),union_of_members(w)) ),
inference(res,[status(thm),theory(equality)],[469,470]),
[iquote('4:Res:469.1,470.0')] ).
cnf(472,plain,
( compact_space(u,v)
| open_covering(f24(u,v),u,v) ),
inference(mrr,[status(thm)],[107,464]),
[iquote('4:MRR:107.0,464.0')] ).
cnf(578,plain,
( ~ subset_collections(u,v)
| open_covering(u,w,v) ),
inference(mrr,[status(thm)],[515,468]),
[iquote('4:MRR:515.1,468.0')] ).
cnf(514,plain,
( ~ subset_collections(u,v)
| finer(v,u,w) ),
inference(mrr,[status(thm)],[30,464]),
[iquote('4:MRR:30.1,30.2,464.0')] ).
cnf(473,plain,
( compact_space(u,v)
| subset_collections(f24(u,v),v) ),
inference(mrr,[status(thm)],[305,464]),
[iquote('4:MRR:305.0,464.0')] ).
cnf(471,plain,
( hausdorff(u,v)
| element_of_set(f19(u,v),u) ),
inference(mrr,[status(thm)],[80,464]),
[iquote('4:MRR:80.0,464.0')] ).
cnf(469,plain,
( hausdorff(u,v)
| element_of_set(f20(u,v),u) ),
inference(mrr,[status(thm)],[81,464]),
[iquote('4:MRR:81.0,464.0')] ).
cnf(533,plain,
( ~ element_of_set(u,intersection_of_members(v))
| element_of_set(u,w) ),
inference(mrr,[status(thm)],[7,467]),
[iquote('4:MRR:7.0,467.0')] ).
cnf(470,plain,
( ~ element_of_set(u,v)
| element_of_set(u,union_of_members(w)) ),
inference(mrr,[status(thm)],[220,464]),
[iquote('4:MRR:220.0,464.0')] ).
cnf(576,plain,
open(u,v,w),
inference(mrr,[status(thm)],[478,467]),
[iquote('4:MRR:478.0,467.0')] ).
cnf(480,plain,
closed(u,v,w),
inference(mrr,[status(thm)],[326,464]),
[iquote('4:MRR:326.0,326.1,464.0')] ).
cnf(468,plain,
equal_sets(union_of_members(u),v),
inference(mrr,[status(thm)],[10,464]),
[iquote('4:MRR:10.0,464.0')] ).
cnf(596,plain,
basis(u,v),
inference(mrr,[status(thm)],[564,595]),
[iquote('4:MRR:564.1,595.0')] ).
cnf(481,plain,
subset_sets(u,v),
inference(mrr,[status(thm)],[187,464]),
[iquote('4:MRR:187.0,464.0')] ).
cnf(467,plain,
element_of_collection(u,v),
inference(mrr,[status(thm)],[12,464]),
[iquote('4:MRR:12.0,464.0')] ).
cnf(464,plain,
topological_space(u,v),
inference(spt,[],[461]),
[iquote('4:Spt:461.1')] ).
cnf(105,axiom,
( ~ compact_space(u,v)
| ~ open_covering(w,u,v)
| subset_collections(f23(u,v,w),w) ),
file('TOP016-1.p',unknown),
[] ).
cnf(3,axiom,
~ equal_sets(union_of_sets(interior(a,cx,ct),boundary(a,cx,ct)),closure(a,cx,ct)),
file('TOP016-1.p',unknown),
[] ).
cnf(52,axiom,
( ~ element_of_set(u,interior(v,w,x))
| element_of_set(u,f13(v,w,x,u)) ),
file('TOP016-1.p',unknown),
[] ).
cnf(104,axiom,
( ~ compact_space(u,v)
| ~ open_covering(w,u,v)
| finite(f23(u,v,w)) ),
file('TOP016-1.p',unknown),
[] ).
cnf(9,axiom,
( ~ element_of_set(u,f2(v,u))
| element_of_set(u,intersection_of_members(v)) ),
file('TOP016-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ element_of_set(u,union_of_members(v))
| element_of_set(u,f1(v,u)) ),
file('TOP016-1.p',unknown),
[] ).
cnf(64,axiom,
( ~ neighborhood(u,v,w,x)
| element_of_set(v,u) ),
file('TOP016-1.p',unknown),
[] ).
cnf(100,axiom,
( ~ open_covering(u,v,w)
| subset_collections(u,w) ),
file('TOP016-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ finer(u,v,w)
| subset_collections(v,u) ),
file('TOP016-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : TOP016-1 : TPTP v8.1.0. Released v1.0.0.
% 0.10/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun May 29 13:39:28 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.43/0.61
% 0.43/0.61 SPASS V 3.9
% 0.43/0.61 SPASS beiseite: Completion found.
% 0.43/0.61 % SZS status CounterSatisfiable
% 0.43/0.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.43/0.61 SPASS derived 1149 clauses, backtracked 0 clauses, performed 6 splits and kept 780 clauses.
% 0.43/0.61 SPASS allocated 77178 KBytes.
% 0.43/0.61 SPASS spent 0:00:00.27 on the problem.
% 0.43/0.61 0:00:00.05 for the input.
% 0.43/0.61 0:00:00.00 for the FLOTTER CNF translation.
% 0.43/0.61 0:00:00.02 for inferences.
% 0.43/0.61 0:00:00.00 for the backtracking.
% 0.43/0.61 0:00:00.14 for the reduction.
% 0.43/0.61
% 0.43/0.61
% 0.43/0.61 The saturated set of worked-off clauses is :
% 0.43/0.61 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------