%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU386+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:21 EDT 2023
% Result : Theorem 0.37s 1.37s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU386+1 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n017.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 : 300
% 0.12/0.33 % DateTime : Thu May 18 12:21:45 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.37/1.37
% 0.37/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 ncf(matrix, plain, [(788 ^ _106829) ^ [] : [empty_carrier(786 ^ [])], (790 ^ _106829) ^ [] : [-(topological_space(786 ^ []))], (792 ^ _106829) ^ [] : [-(top_str(786 ^ []))], (795 ^ _106829) ^ [] : [empty_carrier(793 ^ [])], (797 ^ _106829) ^ [] : [-(transitive_relstr(793 ^ []))], (799 ^ _106829) ^ [] : [-(directed_relstr(793 ^ []))], (801 ^ _106829) ^ [] : [-(net_str(793 ^ [], 786 ^ []))], (804 ^ _106829) ^ [] : [-(element(802 ^ [], the_carrier(786 ^ [])))], (806 ^ _106829) ^ [] : [-(in(802 ^ [], lim_points_of_net(786 ^ [], 793 ^ [])))], (808 ^ _106829) ^ [] : [is_a_cluster_point_of_netstr(786 ^ [], 793 ^ [], 802 ^ [])], (278 ^ _106829) ^ [_115718, _115720] : [_115720 = _115718, -(powerset(_115720) = powerset(_115718))], (284 ^ _106829) ^ [_115936, _115938] : [_115938 = _115936, -(the_carrier(_115938) = the_carrier(_115936))], (290 ^ _106829) ^ [_116162, _116164, _116166, _116168] : [-(lim_points_of_net(_116168, _116164) = lim_points_of_net(_116166, _116162)), _116168 = _116166, _116164 = _116162], (2 ^ _106829) ^ [_106973] : [-(_106973 = _106973)], (4 ^ _106829) ^ [_107080, _107082] : [_107082 = _107080, -(_107080 = _107082)], (10 ^ _106829) ^ [_107284, _107286, _107288] : [-(_107288 = _107284), _107288 = _107286, _107286 = _107284], (20 ^ _106829) ^ [_107597, _107599] : [-(function(_107597)), _107599 = _107597, function(_107599)], (30 ^ _106829) ^ [_107892, _107894] : [-(rel_str(_107892)), _107894 = _107892, rel_str(_107894)], (40 ^ _106829) ^ [_108243, _108245, _108247, _108249, _108251, _108253] : [-(point_neighbourhood(_108251, _108247, _108243)), point_neighbourhood(_108253, _108249, _108245), _108253 = _108251, _108249 = _108247, _108245 = _108243], (58 ^ _106829) ^ [_108796, _108798] : [-(cup_closed(_108796)), _108798 = _108796, cup_closed(_108798)], (68 ^ _106829) ^ [_109091, _109093] : [-(diff_closed(_109091)), _109093 = _109091, diff_closed(_109093)], (78 ^ _106829) ^ [_109386, _109388] : [-(preboolean(_109386)), _109388 = _109386, preboolean(_109388)], (88 ^ _106829) ^ [_109681, _109683] : [-(finite(_109681)), _109683 = _109681, finite(_109683)], (98 ^ _106829) ^ [_109976, _109978] : [-(one_sorted_str(_109976)), _109978 = _109976, one_sorted_str(_109978)], (108 ^ _106829) ^ [_110327, _110329, _110331, _110333, _110335, _110337] : [-(is_eventually_in(_110335, _110331, _110327)), is_eventually_in(_110337, _110333, _110329), _110337 = _110335, _110333 = _110331, _110329 = _110327], (126 ^ _106829) ^ [_110936, _110938, _110940, _110942, _110944, _110946] : [-(is_often_in(_110944, _110940, _110936)), is_often_in(_110946, _110942, _110938), _110946 = _110944, _110942 = _110940, _110938 = _110936], (144 ^ _106829) ^ [_111517, _111519, _111521, _111523] : [-(subset(_111521, _111517)), subset(_111523, _111519), _111523 = _111521, _111519 = _111517], (158 ^ _106829) ^ [_111933, _111935] : [-(empty(_111933)), _111935 = _111933, empty(_111935)], (168 ^ _106829) ^ [_112228, _112230] : [-(topological_space(_112228)), _112230 = _112228, topological_space(_112230)], (178 ^ _106829) ^ [_112523, _112525] : [-(top_str(_112523)), _112525 = _112523, top_str(_112525)], (188 ^ _106829) ^ [_112818, _112820] : [-(empty_carrier(_112818)), _112820 = _112818, empty_carrier(_112820)], (198 ^ _106829) ^ [_113113, _113115] : [-(transitive_relstr(_113113)), _113115 = _113113, transitive_relstr(_113115)], (208 ^ _106829) ^ [_113408, _113410] : [-(directed_relstr(_113408)), _113410 = _113408, directed_relstr(_113410)], (218 ^ _106829) ^ [_113731, _113733, _113735, _113737] : [-(net_str(_113735, _113731)), net_str(_113737, _113733), _113737 = _113735, _113733 = _113731], (232 ^ _106829) ^ [_114175, _114177, _114179, _114181] : [-(element(_114179, _114175)), element(_114181, _114177), _114181 = _114179, _114177 = _114175], (246 ^ _106829) ^ [_114619, _114621, _114623, _114625] : [-(in(_114623, _114619)), in(_114625, _114621), _114625 = _114623, _114621 = _114619], (260 ^ _106829) ^ [_115071, _115073, _115075, _115077, _115079, _115081] : [-(is_a_cluster_point_of_netstr(_115079, _115075, _115071)), is_a_cluster_point_of_netstr(_115081, _115077, _115073), _115081 = _115079, _115077 = _115075, _115073 = _115071], (300 ^ _106829) ^ [_116507, _116509] : [in(_116509, _116507), in(_116507, _116509)], (306 ^ _106829) ^ [_116704] : [empty(_116704), -(finite(_116704))], (312 ^ _106829) ^ [_116890] : [preboolean(_116890), 315 ^ _106829 : [(316 ^ _106829) ^ [] : [-(cup_closed(_116890))], (318 ^ _106829) ^ [] : [-(diff_closed(_116890))]]], (320 ^ _106829) ^ [_117147] : [empty(_117147), -(function(_117147))], (326 ^ _106829) ^ [_117333] : [finite(_117333), 329 ^ _106829 : [(330 ^ _106829) ^ [_117465] : [element(_117465, powerset(_117333)), -(finite(_117465))]]], (336 ^ _106829) ^ [_117670] : [-(preboolean(_117670)), cup_closed(_117670), diff_closed(_117670)], (346 ^ _106829) ^ [_117939] : [-(empty_carrier(_117939)), topological_space(_117939), top_str(_117939), 357 ^ _106829 : [(358 ^ _106829) ^ [_118312] : [-(empty_carrier(_118312)), transitive_relstr(_118312), directed_relstr(_118312), net_str(_118312, _117939), 373 ^ _106829 : [(374 ^ _106829) ^ [_118760] : [element(_118760, powerset(the_carrier(_117939))), 377 ^ _106829 : [(405 ^ _106829) ^ [] : [-(_118760 = lim_points_of_net(_117939, _118312)), 407 ^ _106829 : [(408 ^ _106829) ^ [] : [-(element(406 ^ [_117939, _118312, _118760], the_carrier(_117939)))], (410 ^ _106829) ^ [] : [411 ^ _106829 : [(412 ^ _106829) ^ [] : [-(in(406 ^ [_117939, _118312, _118760], _118760))], (415 ^ _106829) ^ [] : [-(point_neighbourhood(413 ^ [_117939, _118312, _118760], _117939, 406 ^ [_117939, _118312, _118760]))], (417 ^ _106829) ^ [] : [is_eventually_in(_117939, _118312, 413 ^ [_117939, _118312, _118760])]], 418 ^ _106829 : [(425 ^ _106829) ^ [] : [in(406 ^ [_117939, _118312, _118760], _118760)], (419 ^ _106829) ^ [_120406] : [point_neighbourhood(_120406, _117939, 406 ^ [_117939, _118312, _118760]), -(is_eventually_in(_117939, _118312, _120406))]]]]], (378 ^ _106829) ^ [] : [_118760 = lim_points_of_net(_117939, _118312), 381 ^ _106829 : [(382 ^ _106829) ^ [_119058] : [element(_119058, the_carrier(_117939)), 385 ^ _106829 : [(396 ^ _106829) ^ [] : [398 ^ _106829 : [(399 ^ _106829) ^ [] : [-(point_neighbourhood(397 ^ [_117939, _118312, _118760, _119058], _117939, _119058))], (401 ^ _106829) ^ [] : [is_eventually_in(_117939, _118312, 397 ^ [_117939, _118312, _118760, _119058])]], -(in(_119058, _118760))], (386 ^ _106829) ^ [] : [in(_119058, _118760), 389 ^ _106829 : [(390 ^ _106829) ^ [_119337] : [point_neighbourhood(_119337, _117939, _119058), -(is_eventually_in(_117939, _118312, _119337))]]]]]]]]]]]]], (429 ^ _106829) ^ [_120791] : [-(empty_carrier(_120791)), topological_space(_120791), top_str(_120791), 440 ^ _106829 : [(441 ^ _106829) ^ [_121131] : [-(empty_carrier(_121131)), net_str(_121131, _120791), 448 ^ _106829 : [(449 ^ _106829) ^ [_121382] : [element(_121382, the_carrier(_120791)), 452 ^ _106829 : [(463 ^ _106829) ^ [] : [465 ^ _106829 : [(466 ^ _106829) ^ [] : [-(point_neighbourhood(464 ^ [_120791, _121131, _121382], _120791, _121382))], (468 ^ _106829) ^ [] : [is_often_in(_120791, _121131, 464 ^ [_120791, _121131, _121382])]], -(is_a_cluster_point_of_netstr(_120791, _121131, _121382))], (453 ^ _106829) ^ [] : [is_a_cluster_point_of_netstr(_120791, _121131, _121382), 456 ^ _106829 : [(457 ^ _106829) ^ [_121653] : [point_neighbourhood(_121653, _120791, _121382), -(is_often_in(_120791, _121131, _121653))]]]]]]]]], (472 ^ _106829) ^ [_122197, _122199] : [-(element(lim_points_of_net(_122199, _122197), powerset(the_carrier(_122199)))), -(empty_carrier(_122199)), topological_space(_122199), top_str(_122199), -(empty_carrier(_122197)), transitive_relstr(_122197), directed_relstr(_122197), net_str(_122197, _122199)], (502 ^ _106829) ^ [] : [true___, -(true___)], (508 ^ _106829) ^ [] : [true___, -(true___)], (514 ^ _106829) ^ [_123173] : [rel_str(_123173), -(one_sorted_str(_123173))], (520 ^ _106829) ^ [_123359] : [top_str(_123359), -(one_sorted_str(_123359))], (526 ^ _106829) ^ [] : [true___, -(true___)], (532 ^ _106829) ^ [_123664] : [one_sorted_str(_123664), 535 ^ _106829 : [(536 ^ _106829) ^ [_123794] : [net_str(_123794, _123664), -(rel_str(_123794))]]], (542 ^ _106829) ^ [_124009, _124011] : [557 ^ _106829 : [(558 ^ _106829) ^ [_124419] : [point_neighbourhood(_124419, _124011, _124009), -(element(_124419, powerset(the_carrier(_124011))))]], -(empty_carrier(_124011)), topological_space(_124011), top_str(_124011), element(_124009, the_carrier(_124011))], (564 ^ _106829) ^ [] : [true___, -(true___)], (570 ^ _106829) ^ [] : [true___, -(true___)], (577 ^ _106829) ^ [] : [-(rel_str(575 ^ []))], (580 ^ _106829) ^ [] : [-(top_str(578 ^ []))], (583 ^ _106829) ^ [] : [-(one_sorted_str(581 ^ []))], (585 ^ _106829) ^ [_125145] : [one_sorted_str(_125145), -(net_str(588 ^ [_125145], _125145))], (592 ^ _106829) ^ [_125398, _125400] : [-(point_neighbourhood(607 ^ [_125398, _125400], _125400, _125398)), -(empty_carrier(_125400)), topological_space(_125400), top_str(_125400), element(_125398, the_carrier(_125400))], (612 ^ _106829) ^ [_125946] : [-(element(610 ^ [_125946], _125946))], (614 ^ _106829) ^ [_126048] : [empty(powerset(_126048))], (616 ^ _106829) ^ [_126113] : [-(cup_closed(powerset(_126113)))], (618 ^ _106829) ^ [_126178] : [-(diff_closed(powerset(_126178)))], (620 ^ _106829) ^ [_126223] : [-(preboolean(powerset(_126223)))], (622 ^ _106829) ^ [_126323] : [empty(the_carrier(_126323)), -(empty_carrier(_126323)), one_sorted_str(_126323)], (632 ^ _106829) ^ [] : [-(empty(empty_set))], (635 ^ _106829) ^ [] : [empty(633 ^ [])], (637 ^ _106829) ^ [] : [-(finite(633 ^ []))], (640 ^ _106829) ^ [] : [-(empty(638 ^ []))], (643 ^ _106829) ^ [] : [empty(641 ^ [])], (645 ^ _106829) ^ [_126982] : [-(empty(_126982)), 649 ^ _106829 : [(650 ^ _106829) ^ [] : [-(element(648 ^ [_126982], powerset(_126982)))], (652 ^ _106829) ^ [] : [empty(648 ^ [_126982])], (654 ^ _106829) ^ [] : [-(finite(648 ^ [_126982]))]]], (657 ^ _106829) ^ [] : [-(one_sorted_str(655 ^ []))], (659 ^ _106829) ^ [] : [empty_carrier(655 ^ [])], (661 ^ _106829) ^ [_127544] : [-(empty(_127544)), 665 ^ _106829 : [(666 ^ _106829) ^ [] : [-(element(664 ^ [_127544], powerset(_127544)))], (668 ^ _106829) ^ [] : [empty(664 ^ [_127544])], (670 ^ _106829) ^ [] : [-(finite(664 ^ [_127544]))]]], (672 ^ _106829) ^ [_127956] : [680 ^ _106829 : [(681 ^ _106829) ^ [] : [-(element(679 ^ [_127956], powerset(the_carrier(_127956))))], (683 ^ _106829) ^ [] : [empty(679 ^ [_127956])]], -(empty_carrier(_127956)), one_sorted_str(_127956)], (685 ^ _106829) ^ [_128376, _128378] : [-(subset(_128378, _128378))], (687 ^ _106829) ^ [_128485, _128487] : [in(_128487, _128485), -(element(_128487, _128485))], (693 ^ _106829) ^ [_128681] : [-(empty_carrier(_128681)), one_sorted_str(_128681), 700 ^ _106829 : [(701 ^ _106829) ^ [_128928] : [716 ^ _106829 : [(717 ^ _106829) ^ [_129333] : [is_eventually_in(_128681, _128928, _129333), -(is_often_in(_128681, _128928, _129333))]], -(empty_carrier(_128928)), transitive_relstr(_128928), directed_relstr(_128928), net_str(_128928, _128681)]]], (723 ^ _106829) ^ [_129569, _129571] : [element(_129571, _129569), -(empty(_129569)), -(in(_129571, _129569))], (733 ^ _106829) ^ [_129896, _129898] : [element(_129898, powerset(_129896)), -(subset(_129898, _129896))], (739 ^ _106829) ^ [_130062, _130064] : [subset(_130064, _130062), -(element(_130064, powerset(_130062)))], (745 ^ _106829) ^ [_130292, _130294, _130296] : [-(element(_130296, _130292)), in(_130296, _130294), element(_130294, powerset(_130292))], (755 ^ _106829) ^ [_130619, _130621, _130623] : [in(_130623, _130621), element(_130621, powerset(_130619)), empty(_130619)], (765 ^ _106829) ^ [_130915] : [empty(_130915), -(_130915 = empty_set)], (771 ^ _106829) ^ [_131117, _131119] : [in(_131119, _131117), empty(_131117)], (777 ^ _106829) ^ [_131304, _131306] : [empty(_131306), -(_131306 = _131304), empty(_131304)]], input).
% 0.37/1.37 ncf('1',plain,[empty_carrier(786 ^ [])],start(788 ^ 0)).
% 0.37/1.37 ncf('1.1',plain,[-(empty_carrier(786 ^ [])), one_sorted_str(786 ^ []), 717 : is_eventually_in(786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []]), 717 : -(is_often_in(786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []])), 717 : -(empty_carrier(793 ^ [])), 717 : transitive_relstr(793 ^ []), 717 : directed_relstr(793 ^ []), 717 : net_str(793 ^ [], 786 ^ [])],extension(693 ^ 1,bind([[_128681, _128928, _129333], [786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []]]]))).
% 0.37/1.37 ncf('1.1.1',plain,[-(one_sorted_str(786 ^ [])), top_str(786 ^ [])],extension(520 ^ 2,bind([[_123359], [786 ^ []]]))).
% 0.37/1.37 ncf('1.1.1.1',plain,[-(top_str(786 ^ []))],extension(792 ^ 3)).
% 0.37/1.37 ncf('1.1.2',plain,[-(is_eventually_in(786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []])), 390 : point_neighbourhood(464 ^ [786 ^ [], 793 ^ [], 802 ^ []], 786 ^ [], 802 ^ []), 390 : in(802 ^ [], lim_points_of_net(786 ^ [], 793 ^ [])), 386 : element(802 ^ [], the_carrier(786 ^ [])), 382 : lim_points_of_net(786 ^ [], 793 ^ []) = lim_points_of_net(786 ^ [], 793 ^ []), 378 : element(lim_points_of_net(786 ^ [], 793 ^ []), powerset(the_carrier(786 ^ []))), 374 : -(empty_carrier(793 ^ [])), 374 : transitive_relstr(793 ^ []), 374 : directed_relstr(793 ^ []), 374 : net_str(793 ^ [], 786 ^ []), 358 : -(empty_carrier(786 ^ [])), 358 : topological_space(786 ^ []), 358 : top_str(786 ^ [])],extension(346 ^ 6,bind([[_117939, _118312, _118760, _119058, _119337], [786 ^ [], 793 ^ [], lim_points_of_net(786 ^ [], 793 ^ []), 802 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []]]]))).
% 0.37/1.37 ncf('1.1.2.1',plain,[-(point_neighbourhood(464 ^ [786 ^ [], 793 ^ [], 802 ^ []], 786 ^ [], 802 ^ [])), 463 : -(is_a_cluster_point_of_netstr(786 ^ [], 793 ^ [], 802 ^ [])), 463 : element(802 ^ [], the_carrier(786 ^ [])), 449 : -(empty_carrier(793 ^ [])), 449 : net_str(793 ^ [], 786 ^ []), 441 : -(empty_carrier(786 ^ [])), 441 : topological_space(786 ^ []), 441 : top_str(786 ^ [])],extension(429 ^ 19,bind([[_120791, _121131, _121382], [786 ^ [], 793 ^ [], 802 ^ []]]))).
% 0.37/1.37 ncf('1.1.2.1.1',plain,[is_a_cluster_point_of_netstr(786 ^ [], 793 ^ [], 802 ^ [])],extension(808 ^ 26)).
% 0.37/1.37 ncf('1.1.2.1.2',plain,[-(element(802 ^ [], the_carrier(786 ^ [])))],extension(804 ^ 24)).
% 0.37/1.37 ncf('1.1.2.1.3',plain,[empty_carrier(793 ^ [])],extension(795 ^ 22)).
% 0.37/1.37 ncf('1.1.2.1.4',plain,[-(net_str(793 ^ [], 786 ^ []))],extension(801 ^ 22)).
% 0.37/1.37 ncf('1.1.2.1.5',plain,[empty_carrier(786 ^ [])],reduction('1')).
% 0.37/1.37 ncf('1.1.2.1.6',plain,[-(topological_space(786 ^ []))],extension(790 ^ 20)).
% 0.37/1.37 ncf('1.1.2.1.7',plain,[-(top_str(786 ^ []))],extension(792 ^ 20)).
% 0.37/1.37 ncf('1.1.2.2',plain,[-(in(802 ^ [], lim_points_of_net(786 ^ [], 793 ^ [])))],extension(806 ^ 17)).
% 0.37/1.37 ncf('1.1.2.3',plain,[-(element(802 ^ [], the_carrier(786 ^ [])))],extension(804 ^ 15)).
% 0.37/1.37 ncf('1.1.2.4',plain,[-(lim_points_of_net(786 ^ [], 793 ^ []) = lim_points_of_net(786 ^ [], 793 ^ []))],extension(2 ^ 13,bind([[_106973], [lim_points_of_net(786 ^ [], 793 ^ [])]]))).
% 0.37/1.37 ncf('1.1.2.5',plain,[-(element(lim_points_of_net(786 ^ [], 793 ^ []), powerset(the_carrier(786 ^ [])))), -(empty_carrier(786 ^ [])), topological_space(786 ^ []), top_str(786 ^ []), -(empty_carrier(793 ^ [])), transitive_relstr(793 ^ []), directed_relstr(793 ^ []), net_str(793 ^ [], 786 ^ [])],extension(472 ^ 11,bind([[_122197, _122199], [793 ^ [], 786 ^ []]]))).
% 0.37/1.37 ncf('1.1.2.5.1',plain,[empty_carrier(786 ^ [])],reduction('1')).
% 0.37/1.37 ncf('1.1.2.5.2',plain,[-(topological_space(786 ^ []))],extension(790 ^ 12)).
% 0.37/1.37 ncf('1.1.2.5.3',plain,[-(top_str(786 ^ []))],extension(792 ^ 12)).
% 0.37/1.37 ncf('1.1.2.5.4',plain,[empty_carrier(793 ^ [])],extension(795 ^ 12)).
% 0.37/1.37 ncf('1.1.2.5.5',plain,[-(transitive_relstr(793 ^ []))],extension(797 ^ 12)).
% 0.37/1.37 ncf('1.1.2.5.6',plain,[-(directed_relstr(793 ^ []))],extension(799 ^ 12)).
% 0.37/1.37 ncf('1.1.2.5.7',plain,[-(net_str(793 ^ [], 786 ^ []))],extension(801 ^ 12)).
% 0.37/1.37 ncf('1.1.2.6',plain,[empty_carrier(793 ^ [])],extension(795 ^ 9)).
% 0.37/1.37 ncf('1.1.2.7',plain,[-(transitive_relstr(793 ^ []))],extension(797 ^ 9)).
% 0.37/1.37 ncf('1.1.2.8',plain,[-(directed_relstr(793 ^ []))],extension(799 ^ 9)).
% 0.37/1.37 ncf('1.1.2.9',plain,[-(net_str(793 ^ [], 786 ^ []))],extension(801 ^ 9)).
% 0.37/1.37 ncf('1.1.2.10',plain,[empty_carrier(786 ^ [])],reduction('1')).
% 0.37/1.37 ncf('1.1.2.11',plain,[-(topological_space(786 ^ []))],extension(790 ^ 7)).
% 0.37/1.37 ncf('1.1.2.12',plain,[-(top_str(786 ^ []))],extension(792 ^ 7)).
% 0.37/1.37 ncf('1.1.3',plain,[is_often_in(786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []]), -(is_often_in(786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []])), 786 ^ [] = 786 ^ [], 793 ^ [] = 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []] = 464 ^ [786 ^ [], 793 ^ [], 802 ^ []]],extension(126 ^ 6,bind([[_110936, _110938, _110940, _110942, _110944, _110946], [464 ^ [786 ^ [], 793 ^ [], 802 ^ []], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []], 793 ^ [], 793 ^ [], 786 ^ [], 786 ^ []]]))).
% 0.37/1.37 ncf('1.1.3.1',plain,[is_often_in(786 ^ [], 793 ^ [], 464 ^ [786 ^ [], 793 ^ [], 802 ^ []]), 463 : -(is_a_cluster_point_of_netstr(786 ^ [], 793 ^ [], 802 ^ [])), 463 : element(802 ^ [], the_carrier(786 ^ [])), 449 : -(empty_carrier(793 ^ [])), 449 : net_str(793 ^ [], 786 ^ []), 441 : -(empty_carrier(786 ^ [])), 441 : topological_space(786 ^ []), 441 : top_str(786 ^ [])],extension(429 ^ 7,bind([[_120791, _121131, _121382], [786 ^ [], 793 ^ [], 802 ^ []]]))).
% 0.37/1.37 ncf('1.1.3.1.1',plain,[is_a_cluster_point_of_netstr(786 ^ [], 793 ^ [], 802 ^ [])],extension(808 ^ 14)).
% 0.37/1.37 ncf('1.1.3.1.2',plain,[-(element(802 ^ [], the_carrier(786 ^ [])))],extension(804 ^ 12)).
% 0.37/1.37 ncf('1.1.3.1.3',plain,[empty_carrier(793 ^ [])],extension(795 ^ 10)).
% 0.37/1.37 ncf('1.1.3.1.4',plain,[-(net_str(793 ^ [], 786 ^ []))],extension(801 ^ 10)).
% 0.37/1.37 ncf('1.1.3.1.5',plain,[empty_carrier(786 ^ [])],reduction('1')).
% 0.37/1.37 ncf('1.1.3.1.6',plain,[-(topological_space(786 ^ []))],extension(790 ^ 8)).
% 0.37/1.37 ncf('1.1.3.1.7',plain,[-(top_str(786 ^ []))],extension(792 ^ 8)).
% 0.37/1.37 ncf('1.1.3.2',plain,[-(786 ^ [] = 786 ^ [])],extension(2 ^ 7,bind([[_106973], [786 ^ []]]))).
% 0.37/1.37 ncf('1.1.3.3',plain,[-(793 ^ [] = 793 ^ [])],extension(2 ^ 7,bind([[_106973], [793 ^ []]]))).
% 0.37/1.37 ncf('1.1.3.4',plain,[-(464 ^ [786 ^ [], 793 ^ [], 802 ^ []] = 464 ^ [786 ^ [], 793 ^ [], 802 ^ []])],extension(2 ^ 7,bind([[_106973], [464 ^ [786 ^ [], 793 ^ [], 802 ^ []]]]))).
% 0.37/1.37 ncf('1.1.4',plain,[empty_carrier(793 ^ [])],extension(795 ^ 4)).
% 0.37/1.37 ncf('1.1.5',plain,[-(transitive_relstr(793 ^ []))],extension(797 ^ 4)).
% 0.37/1.37 ncf('1.1.6',plain,[-(directed_relstr(793 ^ []))],extension(799 ^ 4)).
% 0.37/1.37 ncf('1.1.7',plain,[-(net_str(793 ^ [], 786 ^ []))],extension(801 ^ 4)).
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------