%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU324+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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 : Fri May 19 12:03:08 EDT 2023
% Result : Theorem 0.51s 1.39s
% Output : Proof 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU324+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 18 12:51:52 EDT 2023
% 0.14/0.34 % CPUTime :
% 0.51/1.39
% 0.51/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.51/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/1.39 %-----------------------------------------------------
% 0.51/1.39 ncf(matrix, plain, [(393 ^ _64803) ^ [] : [-(topological_space(391 ^ []))], (395 ^ _64803) ^ [] : [-(top_str(391 ^ []))], (398 ^ _64803) ^ [] : [-(top_str(396 ^ []))], (401 ^ _64803) ^ [] : [-(element(399 ^ [], powerset(the_carrier(391 ^ []))))], (404 ^ _64803) ^ [] : [-(element(402 ^ [], powerset(the_carrier(396 ^ []))))], (406 ^ _64803) ^ [] : [407 ^ _64803 : [(408 ^ _64803) ^ [] : [-(open_subset(402 ^ [], 396 ^ []))], (410 ^ _64803) ^ [] : [interior(396 ^ [], 402 ^ []) = 402 ^ []]], 411 ^ _64803 : [(412 ^ _64803) ^ [] : [-(interior(391 ^ [], 399 ^ []) = 399 ^ [])], (414 ^ _64803) ^ [] : [open_subset(399 ^ [], 391 ^ [])]]], (106 ^ _64803) ^ [_68258, _68260, _68262, _68264] : [-(subset_complement(_68264, _68260) = subset_complement(_68262, _68258)), _68264 = _68262, _68260 = _68258], (116 ^ _64803) ^ [_68617, _68619, _68621, _68623] : [-(topstr_closure(_68623, _68619) = topstr_closure(_68621, _68617)), _68623 = _68621, _68619 = _68617], (126 ^ _64803) ^ [_68948, _68950] : [_68950 = _68948, -(powerset(_68950) = powerset(_68948))], (132 ^ _64803) ^ [_69166, _69168] : [_69168 = _69166, -(the_carrier(_69168) = the_carrier(_69166))], (138 ^ _64803) ^ [_69392, _69394, _69396, _69398] : [-(interior(_69398, _69394) = interior(_69396, _69392)), _69398 = _69396, _69394 = _69392], (2 ^ _64803) ^ [_64947] : [-(_64947 = _64947)], (4 ^ _64803) ^ [_65054, _65056] : [_65056 = _65054, -(_65054 = _65056)], (10 ^ _64803) ^ [_65258, _65260, _65262] : [-(_65262 = _65258), _65262 = _65260, _65260 = _65258], (20 ^ _64803) ^ [_65571, _65573] : [-(one_sorted_str(_65571)), _65573 = _65571, one_sorted_str(_65573)], (30 ^ _64803) ^ [_65894, _65896, _65898, _65900] : [-(subset(_65898, _65894)), subset(_65900, _65896), _65900 = _65898, _65896 = _65894], (44 ^ _64803) ^ [_66338, _66340, _66342, _66344] : [-(closed_subset(_66342, _66338)), closed_subset(_66344, _66340), _66344 = _66342, _66340 = _66338], (58 ^ _64803) ^ [_66754, _66756] : [-(topological_space(_66754)), _66756 = _66754, topological_space(_66756)], (68 ^ _64803) ^ [_67049, _67051] : [-(top_str(_67049)), _67051 = _67049, top_str(_67051)], (78 ^ _64803) ^ [_67372, _67374, _67376, _67378] : [-(element(_67376, _67372)), element(_67378, _67374), _67378 = _67376, _67374 = _67372], (92 ^ _64803) ^ [_67796, _67798, _67800, _67802] : [-(open_subset(_67800, _67796)), open_subset(_67802, _67798), _67802 = _67800, _67798 = _67796], (148 ^ _64803) ^ [_69727] : [top_str(_69727), 151 ^ _64803 : [(152 ^ _64803) ^ [_69878] : [element(_69878, powerset(the_carrier(_69727))), -(interior(_69727, _69878) = subset_complement(the_carrier(_69727), topstr_closure(_69727, subset_complement(the_carrier(_69727), _69878))))]]], (158 ^ _64803) ^ [_70135, _70137] : [-(element(interior(_70137, _70135), powerset(the_carrier(_70137)))), top_str(_70137), element(_70135, powerset(the_carrier(_70137)))], (168 ^ _64803) ^ [] : [true___, -(true___)], (174 ^ _64803) ^ [_70573, _70575] : [element(_70573, powerset(_70575)), -(element(subset_complement(_70575, _70573), powerset(_70575)))], (180 ^ _64803) ^ [_70797, _70799] : [-(element(topstr_closure(_70799, _70797), powerset(the_carrier(_70799)))), top_str(_70799), element(_70797, powerset(the_carrier(_70799)))], (190 ^ _64803) ^ [_71102] : [top_str(_71102), -(one_sorted_str(_71102))], (196 ^ _64803) ^ [] : [true___, -(true___)], (202 ^ _64803) ^ [] : [true___, -(true___)], (208 ^ _64803) ^ [] : [true___, -(true___)], (215 ^ _64803) ^ [] : [-(top_str(213 ^ []))], (218 ^ _64803) ^ [] : [-(one_sorted_str(216 ^ []))], (221 ^ _64803) ^ [_71847] : [-(element(219 ^ [_71847], _71847))], (223 ^ _64803) ^ [_71959, _71961] : [-(closed_subset(topstr_closure(_71961, _71959), _71961)), topological_space(_71961), top_str(_71961), element(_71959, powerset(the_carrier(_71961)))], (237 ^ _64803) ^ [_72357, _72359] : [-(open_subset(subset_complement(the_carrier(_72359), _72357), _72359)), topological_space(_72359), top_str(_72359), closed_subset(_72357, _72359), element(_72357, powerset(the_carrier(_72359)))], (255 ^ _64803) ^ [_72848, _72850] : [-(closed_subset(subset_complement(the_carrier(_72850), _72848), _72850)), topological_space(_72850), top_str(_72850), open_subset(_72848, _72850), element(_72848, powerset(the_carrier(_72850)))], (273 ^ _64803) ^ [_73339, _73341] : [-(open_subset(interior(_73341, _73339), _73341)), topological_space(_73341), top_str(_73341), element(_73339, powerset(the_carrier(_73341)))], (287 ^ _64803) ^ [_73737, _73739] : [element(_73737, powerset(_73739)), -(subset_complement(_73739, subset_complement(_73739, _73737)) = _73737)], (293 ^ _64803) ^ [_73949] : [301 ^ _64803 : [(302 ^ _64803) ^ [] : [-(element(300 ^ [_73949], powerset(the_carrier(_73949))))], (304 ^ _64803) ^ [] : [-(open_subset(300 ^ [_73949], _73949))]], topological_space(_73949), top_str(_73949)], (306 ^ _64803) ^ [_74367] : [314 ^ _64803 : [(315 ^ _64803) ^ [] : [-(element(313 ^ [_74367], powerset(the_carrier(_74367))))], (317 ^ _64803) ^ [] : [-(open_subset(313 ^ [_74367], _74367))], (319 ^ _64803) ^ [] : [-(closed_subset(313 ^ [_74367], _74367))]], topological_space(_74367), top_str(_74367)], (321 ^ _64803) ^ [_74868] : [329 ^ _64803 : [(330 ^ _64803) ^ [] : [-(element(328 ^ [_74868], powerset(the_carrier(_74868))))], (332 ^ _64803) ^ [] : [-(closed_subset(328 ^ [_74868], _74868))]], topological_space(_74868), top_str(_74868)], (334 ^ _64803) ^ [_75285, _75287] : [-(subset(_75287, _75287))], (336 ^ _64803) ^ [_75380] : [top_str(_75380), 339 ^ _64803 : [(340 ^ _64803) ^ [_75526] : [element(_75526, powerset(the_carrier(_75380))), 343 ^ _64803 : [(344 ^ _64803) ^ [] : [open_subset(_75526, _75380), -(closed_subset(subset_complement(the_carrier(_75380), _75526), _75380))], (350 ^ _64803) ^ [] : [closed_subset(subset_complement(the_carrier(_75380), _75526), _75380), -(open_subset(_75526, _75380))]]]]], (356 ^ _64803) ^ [_76045, _76047] : [element(_76047, powerset(_76045)), -(subset(_76047, _76045))], (362 ^ _64803) ^ [_76211, _76213] : [subset(_76213, _76211), -(element(_76213, powerset(_76211)))], (368 ^ _64803) ^ [_76393] : [top_str(_76393), 371 ^ _64803 : [(372 ^ _64803) ^ [_76557] : [element(_76557, powerset(the_carrier(_76393))), 375 ^ _64803 : [(376 ^ _64803) ^ [] : [closed_subset(_76557, _76393), -(topstr_closure(_76393, _76557) = _76557)], (382 ^ _64803) ^ [] : [-(closed_subset(_76557, _76393)), topological_space(_76393), topstr_closure(_76393, _76557) = _76557]]]]]], input).
% 0.51/1.39 ncf('1',plain,[410 : interior(396 ^ [], 402 ^ []) = 402 ^ [], 414 : open_subset(399 ^ [], 391 ^ [])],start(406 ^ 0)).
% 0.51/1.39 ncf('1.1',plain,[-(interior(396 ^ [], 402 ^ []) = 402 ^ []), interior(396 ^ [], 402 ^ []) = subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = 402 ^ []],extension(10 ^ 3,bind([[_65258, _65260, _65262], [402 ^ [], subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))), interior(396 ^ [], 402 ^ [])]]))).
% 0.51/1.39 ncf('1.1.1',plain,[-(interior(396 ^ [], 402 ^ []) = subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])))), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = interior(396 ^ [], 402 ^ [])],extension(4 ^ 4,bind([[_65054, _65056], [interior(396 ^ [], 402 ^ []), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])))]]))).
% 0.51/1.39 ncf('1.1.1.1',plain,[-(subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = interior(396 ^ [], 402 ^ [])), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = interior(396 ^ [], 402 ^ []), interior(396 ^ [], 402 ^ []) = interior(396 ^ [], 402 ^ [])],extension(10 ^ 5,bind([[_65258, _65260, _65262], [interior(396 ^ [], 402 ^ []), interior(396 ^ [], 402 ^ []), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])))]]))).
% 0.51/1.39 ncf('1.1.1.1.1',plain,[-(subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = interior(396 ^ [], 402 ^ [])), interior(396 ^ [], 402 ^ []) = subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])))],extension(4 ^ 6,bind([[_65054, _65056], [subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))), interior(396 ^ [], 402 ^ [])]]))).
% 0.51/1.39 ncf('1.1.1.1.1.1',plain,[-(interior(396 ^ [], 402 ^ []) = subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])))), 152 : element(402 ^ [], powerset(the_carrier(396 ^ []))), 152 : top_str(396 ^ [])],extension(148 ^ 7,bind([[_69727, _69878], [396 ^ [], 402 ^ []]]))).
% 0.51/1.39 ncf('1.1.1.1.1.1.1',plain,[-(element(402 ^ [], powerset(the_carrier(396 ^ []))))],extension(404 ^ 10)).
% 0.51/1.39 ncf('1.1.1.1.1.1.2',plain,[-(top_str(396 ^ []))],extension(398 ^ 8)).
% 0.51/1.39 ncf('1.1.1.1.2',plain,[-(interior(396 ^ [], 402 ^ []) = interior(396 ^ [], 402 ^ [])), 396 ^ [] = 396 ^ [], 402 ^ [] = 402 ^ []],extension(138 ^ 6,bind([[_69392, _69394, _69396, _69398], [402 ^ [], 402 ^ [], 396 ^ [], 396 ^ []]]))).
% 0.51/1.39 ncf('1.1.1.1.2.1',plain,[-(396 ^ [] = 396 ^ [])],extension(2 ^ 7,bind([[_64947], [396 ^ []]]))).
% 0.51/1.39 ncf('1.1.1.1.2.2',plain,[-(402 ^ [] = 402 ^ [])],extension(2 ^ 7,bind([[_64947], [402 ^ []]]))).
% 0.51/1.39 ncf('1.1.2',plain,[-(subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = 402 ^ []), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])), subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])) = 402 ^ []],extension(10 ^ 4,bind([[_65258, _65260, _65262], [402 ^ [], subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])), subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])))]]))).
% 0.51/1.39 ncf('1.1.2.1',plain,[-(subset_complement(the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ []))) = subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ []))), the_carrier(396 ^ []) = the_carrier(396 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])) = subset_complement(the_carrier(396 ^ []), 402 ^ [])],extension(106 ^ 5,bind([[_68258, _68260, _68262, _68264], [subset_complement(the_carrier(396 ^ []), 402 ^ []), topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])), the_carrier(396 ^ []), the_carrier(396 ^ [])]]))).
% 0.51/1.39 ncf('1.1.2.1.1',plain,[-(the_carrier(396 ^ []) = the_carrier(396 ^ [])), 396 ^ [] = 396 ^ []],extension(132 ^ 6,bind([[_69166, _69168], [396 ^ [], 396 ^ []]]))).
% 0.51/1.39 ncf('1.1.2.1.1.1',plain,[-(396 ^ [] = 396 ^ [])],extension(2 ^ 7,bind([[_64947], [396 ^ []]]))).
% 0.51/1.39 ncf('1.1.2.1.2',plain,[-(topstr_closure(396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])) = subset_complement(the_carrier(396 ^ []), 402 ^ [])), 376 : closed_subset(subset_complement(the_carrier(396 ^ []), 402 ^ []), 396 ^ []), 376 : element(subset_complement(the_carrier(396 ^ []), 402 ^ []), powerset(the_carrier(396 ^ []))), 372 : top_str(396 ^ [])],extension(368 ^ 6,bind([[_76393, _76557], [396 ^ [], subset_complement(the_carrier(396 ^ []), 402 ^ [])]]))).
% 0.51/1.39 ncf('1.1.2.1.2.1',plain,[-(closed_subset(subset_complement(the_carrier(396 ^ []), 402 ^ []), 396 ^ [])), 344 : open_subset(402 ^ [], 396 ^ []), 344 : element(402 ^ [], powerset(the_carrier(396 ^ []))), 340 : top_str(396 ^ [])],extension(336 ^ 11,bind([[_75380, _75526], [396 ^ [], 402 ^ []]]))).
% 0.51/1.39 ncf('1.1.2.1.2.1.1',plain,[-(open_subset(402 ^ [], 396 ^ []))],extension(408 ^ 16)).
% 0.51/1.39 ncf('1.1.2.1.2.1.2',plain,[-(element(402 ^ [], powerset(the_carrier(396 ^ []))))],extension(404 ^ 14)).
% 0.51/1.39 ncf('1.1.2.1.2.1.3',plain,[-(top_str(396 ^ []))],extension(398 ^ 12)).
% 0.51/1.39 ncf('1.1.2.1.2.2',plain,[-(element(subset_complement(the_carrier(396 ^ []), 402 ^ []), powerset(the_carrier(396 ^ [])))), element(402 ^ [], powerset(the_carrier(396 ^ [])))],extension(174 ^ 9,bind([[_70573, _70575], [402 ^ [], the_carrier(396 ^ [])]]))).
% 0.51/1.39 ncf('1.1.2.1.2.2.1',plain,[-(element(402 ^ [], powerset(the_carrier(396 ^ []))))],extension(404 ^ 10)).
% 0.51/1.39 ncf('1.1.2.1.2.3',plain,[-(top_str(396 ^ []))],extension(398 ^ 7)).
% 0.51/1.39 ncf('1.1.2.2',plain,[-(subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])) = 402 ^ []), subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])) = 402 ^ [], 402 ^ [] = 402 ^ []],extension(10 ^ 5,bind([[_65258, _65260, _65262], [402 ^ [], 402 ^ [], subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ []))]]))).
% 0.51/1.39 ncf('1.1.2.2.1',plain,[-(subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])) = 402 ^ []), subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])) = 402 ^ [], 402 ^ [] = 402 ^ []],extension(10 ^ 6,bind([[_65258, _65260, _65262], [402 ^ [], 402 ^ [], subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ []))]]))).
% 0.51/1.39 ncf('1.1.2.2.1.1',plain,[-(subset_complement(the_carrier(396 ^ []), subset_complement(the_carrier(396 ^ []), 402 ^ [])) = 402 ^ []), element(402 ^ [], powerset(the_carrier(396 ^ [])))],extension(287 ^ 7,bind([[_73737, _73739], [402 ^ [], the_carrier(396 ^ [])]]))).
% 0.51/1.39 ncf('1.1.2.2.1.1.1',plain,[-(element(402 ^ [], powerset(the_carrier(396 ^ []))))],extension(404 ^ 8)).
% 0.51/1.39 ncf('1.1.2.2.1.2',plain,[-(402 ^ [] = 402 ^ [])],extension(2 ^ 7,bind([[_64947], [402 ^ []]]))).
% 0.51/1.39 ncf('1.1.2.2.2',plain,[-(402 ^ [] = 402 ^ [])],extension(2 ^ 6,bind([[_64947], [402 ^ []]]))).
% 0.51/1.39 ncf('1.2',plain,[-(open_subset(399 ^ [], 391 ^ [])), open_subset(399 ^ [], 391 ^ []), 399 ^ [] = 399 ^ [], 391 ^ [] = 391 ^ []],extension(92 ^ 3,bind([[_67796, _67798, _67800, _67802], [391 ^ [], 391 ^ [], 399 ^ [], 399 ^ []]]))).
% 0.51/1.39 ncf('1.2.1',plain,[-(open_subset(399 ^ [], 391 ^ [])), open_subset(399 ^ [], 391 ^ []), 399 ^ [] = 399 ^ [], 391 ^ [] = 391 ^ []],extension(92 ^ 4,bind([[_67796, _67798, _67800, _67802], [391 ^ [], 391 ^ [], 399 ^ [], 399 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.1',plain,[-(open_subset(399 ^ [], 391 ^ [])), open_subset(399 ^ [], 391 ^ []), 399 ^ [] = 399 ^ [], 391 ^ [] = 391 ^ []],extension(92 ^ 5,bind([[_67796, _67798, _67800, _67802], [391 ^ [], 391 ^ [], 399 ^ [], 399 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.1.1',plain,[-(open_subset(399 ^ [], 391 ^ [])), open_subset(interior(391 ^ [], 399 ^ []), 391 ^ []), interior(391 ^ [], 399 ^ []) = 399 ^ [], 391 ^ [] = 391 ^ []],extension(92 ^ 6,bind([[_67796, _67798, _67800, _67802], [391 ^ [], 391 ^ [], 399 ^ [], interior(391 ^ [], 399 ^ [])]]))).
% 0.51/1.39 ncf('1.2.1.1.1.1',plain,[-(open_subset(interior(391 ^ [], 399 ^ []), 391 ^ [])), topological_space(391 ^ []), top_str(391 ^ []), element(399 ^ [], powerset(the_carrier(391 ^ [])))],extension(273 ^ 7,bind([[_73339, _73341], [399 ^ [], 391 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.1.1.1.1',plain,[-(topological_space(391 ^ []))],extension(393 ^ 8)).
% 0.51/1.39 ncf('1.2.1.1.1.1.2',plain,[-(top_str(391 ^ []))],extension(395 ^ 8)).
% 0.51/1.39 ncf('1.2.1.1.1.1.3',plain,[-(element(399 ^ [], powerset(the_carrier(391 ^ []))))],extension(401 ^ 8)).
% 0.51/1.39 ncf('1.2.1.1.1.2',plain,[-(interior(391 ^ [], 399 ^ []) = 399 ^ [])],extension(412 ^ 7)).
% 0.51/1.39 ncf('1.2.1.1.1.3',plain,[-(391 ^ [] = 391 ^ [])],extension(2 ^ 7,bind([[_64947], [391 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.1.2',plain,[-(399 ^ [] = 399 ^ [])],extension(2 ^ 6,bind([[_64947], [399 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.1.3',plain,[-(391 ^ [] = 391 ^ [])],extension(2 ^ 6,bind([[_64947], [391 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.2',plain,[-(399 ^ [] = 399 ^ [])],extension(2 ^ 5,bind([[_64947], [399 ^ []]]))).
% 0.51/1.39 ncf('1.2.1.3',plain,[-(391 ^ [] = 391 ^ [])],extension(2 ^ 5,bind([[_64947], [391 ^ []]]))).
% 0.51/1.39 ncf('1.2.2',plain,[-(399 ^ [] = 399 ^ [])],extension(2 ^ 4,bind([[_64947], [399 ^ []]]))).
% 0.51/1.39 ncf('1.2.3',plain,[-(391 ^ [] = 391 ^ [])],extension(2 ^ 4,bind([[_64947], [391 ^ []]]))).
% 0.51/1.39 %-----------------------------------------------------
% 0.51/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------