%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU401+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %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 : Fri May 19 12:03:24 EDT 2023
% Result : Theorem 35.02s 34.56s
% Output : Proof 35.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU401+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 13:52:28 EDT 2023
% 0.13/0.34 % CPUTime :
% 35.02/34.56
% 35.02/34.56 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 35.02/34.56 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 35.02/34.56 %-----------------------------------------------------
% 35.02/34.56 ncf(matrix, plain, [(1464 ^ _229231) ^ [] : [empty_carrier(1460 ^ [])], (1466 ^ _229231) ^ [] : [-(topological_space(1460 ^ []))], (1468 ^ _229231) ^ [] : [-(top_str(1460 ^ []))], (1470 ^ _229231) ^ [] : [empty_carrier(1461 ^ [])], (1472 ^ _229231) ^ [] : [-(transitive_relstr(1461 ^ []))], (1474 ^ _229231) ^ [] : [-(directed_relstr(1461 ^ []))], (1476 ^ _229231) ^ [] : [-(net_str(1461 ^ [], 1460 ^ []))], (1569 ^ _229231) ^ [] : [1478 ^ [] = 1479 ^ []], (1481 ^ _229231) ^ [_278141] : [in(_278141, 1478 ^ []), 1484 ^ _229231 : [(1485 ^ _229231) ^ [] : [-(in(_278141, the_carrier(1461 ^ [])))], (1488 ^ _229231) ^ [] : [-(netstr_induced_subset(1486 ^ [_278141], 1460 ^ [], 1461 ^ []))], (1491 ^ _229231) ^ [] : [-(element(1489 ^ [_278141], the_carrier(1461 ^ [])))], (1493 ^ _229231) ^ [] : [-(1477 ^ [] = topstr_closure(1460 ^ [], 1486 ^ [_278141]))], (1495 ^ _229231) ^ [] : [-(_278141 = 1489 ^ [_278141])], (1497 ^ _229231) ^ [] : [-(1486 ^ [_278141] = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], 1489 ^ [_278141])), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], 1489 ^ [_278141]))))]]], (1499 ^ _229231) ^ [_278925] : [-(in(_278925, 1478 ^ [])), in(_278925, the_carrier(1461 ^ [])), 1504 ^ _229231 : [(1505 ^ _229231) ^ [_279140] : [netstr_induced_subset(_279140, 1460 ^ [], 1461 ^ []), 1508 ^ _229231 : [(1509 ^ _229231) ^ [_279313] : [element(_279313, the_carrier(1461 ^ [])), 1477 ^ [] = topstr_closure(1460 ^ [], _279140), _278925 = _279313, _279140 = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], _279313)), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], _279313)))]]]]], (1525 ^ _229231) ^ [_279813] : [in(_279813, 1479 ^ []), 1528 ^ _229231 : [(1529 ^ _229231) ^ [] : [-(in(_279813, the_carrier(1461 ^ [])))], (1532 ^ _229231) ^ [] : [-(netstr_induced_subset(1530 ^ [_279813], 1460 ^ [], 1461 ^ []))], (1535 ^ _229231) ^ [] : [-(element(1533 ^ [_279813], the_carrier(1461 ^ [])))], (1537 ^ _229231) ^ [] : [-(1477 ^ [] = topstr_closure(1460 ^ [], 1530 ^ [_279813]))], (1539 ^ _229231) ^ [] : [-(_279813 = 1533 ^ [_279813])], (1541 ^ _229231) ^ [] : [-(1530 ^ [_279813] = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], 1533 ^ [_279813])), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], 1533 ^ [_279813]))))]]], (1543 ^ _229231) ^ [_280597] : [-(in(_280597, 1479 ^ [])), in(_280597, the_carrier(1461 ^ [])), 1548 ^ _229231 : [(1549 ^ _229231) ^ [_280812] : [netstr_induced_subset(_280812, 1460 ^ [], 1461 ^ []), 1552 ^ _229231 : [(1553 ^ _229231) ^ [_280985] : [element(_280985, the_carrier(1461 ^ [])), 1477 ^ [] = topstr_closure(1460 ^ [], _280812), _280597 = _280985, _280812 = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], _280985)), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], _280985)))]]]]], (382 ^ _229231) ^ [_241526, _241528, _241530, _241532, _241534, _241536, _241538, _241540] : [-(net_str_of(_241540, _241536, _241532, _241528) = net_str_of(_241538, _241534, _241530, _241526)), _241540 = _241538, _241536 = _241534, _241532 = _241530, _241528 = _241526], (400 ^ _229231) ^ [_242131, _242133] : [_242133 = _242131, -(the_InternalRel(_242133) = the_InternalRel(_242131))], (406 ^ _229231) ^ [_242377, _242379, _242381, _242383] : [-(cartesian_product2(_242383, _242379) = cartesian_product2(_242381, _242377)), _242383 = _242381, _242379 = _242377], (416 ^ _229231) ^ [_242708, _242710] : [_242710 = _242708, -(relation_rng(_242710) = relation_rng(_242708))], (422 ^ _229231) ^ [_242982, _242984, _242986, _242988, _242990, _242992] : [-(netstr_restr_to_element(_242992, _242988, _242984) = netstr_restr_to_element(_242990, _242986, _242982)), _242992 = _242990, _242988 = _242986, _242984 = _242982], (436 ^ _229231) ^ [_243442, _243444] : [_243444 = _243442, -(powerset(_243444) = powerset(_243442))], (442 ^ _229231) ^ [_243688, _243690, _243692, _243694] : [-(topstr_closure(_243694, _243690) = topstr_closure(_243692, _243688)), _243694 = _243692, _243690 = _243688], (452 ^ _229231) ^ [_244075, _244077, _244079, _244081, _244083, _244085] : [-(relation_rng_as_subset(_244085, _244081, _244077) = relation_rng_as_subset(_244083, _244079, _244075)), _244085 = _244083, _244081 = _244079, _244077 = _244075], (466 ^ _229231) ^ [_244535, _244537] : [_244537 = _244535, -(the_carrier(_244537) = the_carrier(_244535))], (472 ^ _229231) ^ [_244781, _244783, _244785, _244787] : [-(the_mapping(_244787, _244783) = the_mapping(_244785, _244781)), _244787 = _244785, _244783 = _244781], (482 ^ _229231) ^ [_245148, _245150, _245152, _245154, _245156, _245158] : [-(subnetstr_of_element(_245158, _245154, _245150) = subnetstr_of_element(_245156, _245152, _245148)), _245158 = _245156, _245154 = _245152, _245150 = _245148], (2 ^ _229231) ^ [_229375] : [-(_229375 = _229375)], (4 ^ _229231) ^ [_229482, _229484] : [_229484 = _229482, -(_229482 = _229484)], (10 ^ _229231) ^ [_229686, _229688, _229690] : [-(_229690 = _229686), _229690 = _229688, _229688 = _229686], (20 ^ _229231) ^ [_229999, _230001] : [-(v1_membered(_229999)), _230001 = _229999, v1_membered(_230001)], (30 ^ _229231) ^ [_230294, _230296] : [-(v2_membered(_230294)), _230296 = _230294, v2_membered(_230296)], (40 ^ _229231) ^ [_230589, _230591] : [-(v3_membered(_230589)), _230591 = _230589, v3_membered(_230591)], (50 ^ _229231) ^ [_230884, _230886] : [-(v4_membered(_230884)), _230886 = _230884, v4_membered(_230886)], (60 ^ _229231) ^ [_231179, _231181] : [-(v5_membered(_231179)), _231181 = _231179, v5_membered(_231181)], (70 ^ _229231) ^ [_231474, _231476] : [-(finite(_231474)), _231476 = _231474, finite(_231476)], (80 ^ _229231) ^ [_231797, _231799, _231801, _231803] : [-(open_subset(_231801, _231797)), open_subset(_231803, _231799), _231803 = _231801, _231799 = _231797], (94 ^ _229231) ^ [_232241, _232243, _232245, _232247] : [-(boundary_set(_232245, _232241)), boundary_set(_232247, _232243), _232247 = _232245, _232243 = _232241], (108 ^ _229231) ^ [_232685, _232687, _232689, _232691] : [-(nowhere_dense(_232689, _232685)), nowhere_dense(_232691, _232687), _232691 = _232689, _232687 = _232685], (122 ^ _229231) ^ [_233129, _233131, _233133, _233135] : [-(closed_subset(_233133, _233129)), closed_subset(_233135, _233131), _233135 = _233133, _233131 = _233129], (136 ^ _229231) ^ [_233545, _233547] : [-(empty(_233545)), _233547 = _233545, empty(_233547)], (146 ^ _229231) ^ [_233840, _233842] : [-(relation(_233840)), _233842 = _233840, relation(_233842)], (156 ^ _229231) ^ [_234191, _234193, _234195, _234197, _234199, _234201] : [-(relation_of2(_234199, _234195, _234191)), relation_of2(_234201, _234197, _234193), _234201 = _234199, _234197 = _234195, _234193 = _234191], (174 ^ _229231) ^ [_234772, _234774, _234776, _234778] : [-(strict_net_str(_234776, _234772)), strict_net_str(_234778, _234774), _234778 = _234776, _234774 = _234772], (188 ^ _229231) ^ [_235244, _235246, _235248, _235250, _235252, _235254] : [-(subnet(_235252, _235248, _235244)), subnet(_235254, _235250, _235246), _235254 = _235252, _235250 = _235248, _235246 = _235244], (206 ^ _229231) ^ [_235797, _235799] : [-(rel_str(_235797)), _235799 = _235797, rel_str(_235799)], (216 ^ _229231) ^ [_236092, _236094] : [-(one_sorted_str(_236092)), _236094 = _236092, one_sorted_str(_236094)], (226 ^ _229231) ^ [_236387, _236389] : [-(function(_236387)), _236389 = _236387, function(_236389)], (236 ^ _229231) ^ [_236738, _236740, _236742, _236744, _236746, _236748] : [-(quasi_total(_236746, _236742, _236738)), quasi_total(_236748, _236744, _236740), _236748 = _236746, _236744 = _236742, _236740 = _236738], (254 ^ _229231) ^ [_237347, _237349, _237351, _237353, _237355, _237357] : [-(relation_of2_as_subset(_237355, _237351, _237347)), relation_of2_as_subset(_237357, _237353, _237349), _237357 = _237355, _237353 = _237351, _237349 = _237347], (272 ^ _229231) ^ [_237900, _237902] : [-(topological_space(_237900)), _237902 = _237900, topological_space(_237902)], (282 ^ _229231) ^ [_238195, _238197] : [-(top_str(_238195)), _238197 = _238195, top_str(_238197)], (292 ^ _229231) ^ [_238490, _238492] : [-(empty_carrier(_238490)), _238492 = _238490, empty_carrier(_238492)], (302 ^ _229231) ^ [_238785, _238787] : [-(transitive_relstr(_238785)), _238787 = _238785, transitive_relstr(_238787)], (312 ^ _229231) ^ [_239080, _239082] : [-(directed_relstr(_239080)), _239082 = _239080, directed_relstr(_239082)], (322 ^ _229231) ^ [_239403, _239405, _239407, _239409] : [-(net_str(_239407, _239403)), net_str(_239409, _239405), _239409 = _239407, _239405 = _239403], (336 ^ _229231) ^ [_239847, _239849, _239851, _239853] : [-(in(_239851, _239847)), in(_239853, _239849), _239853 = _239851, _239849 = _239847], (368 ^ _229231) ^ [_240880, _240882, _240884, _240886] : [-(element(_240884, _240880)), element(_240886, _240882), _240886 = _240884, _240882 = _240880], (350 ^ _229231) ^ [_240319, _240321, _240323, _240325, _240327, _240329] : [-(netstr_induced_subset(_240327, _240323, _240319)), netstr_induced_subset(_240329, _240325, _240321), _240329 = _240327, _240325 = _240323, _240321 = _240319], (496 ^ _229231) ^ [_245641] : [top_str(_245641), 500 ^ _229231 : [(501 ^ _229231) ^ [] : [-(element(499 ^ [_245641], powerset(the_carrier(_245641))))], (503 ^ _229231) ^ [] : [-(empty(499 ^ [_245641]))], (505 ^ _229231) ^ [] : [-(v1_membered(499 ^ [_245641]))], (507 ^ _229231) ^ [] : [-(v2_membered(499 ^ [_245641]))], (509 ^ _229231) ^ [] : [-(v3_membered(499 ^ [_245641]))], (511 ^ _229231) ^ [] : [-(v4_membered(499 ^ [_245641]))], (513 ^ _229231) ^ [] : [-(v5_membered(499 ^ [_245641]))], (515 ^ _229231) ^ [] : [-(boundary_set(499 ^ [_245641], _245641))]]], (517 ^ _229231) ^ [_246456] : [525 ^ _229231 : [(526 ^ _229231) ^ [] : [-(element(524 ^ [_246456], powerset(the_carrier(_246456))))], (528 ^ _229231) ^ [] : [-(empty(524 ^ [_246456]))], (530 ^ _229231) ^ [] : [-(open_subset(524 ^ [_246456], _246456))], (532 ^ _229231) ^ [] : [-(closed_subset(524 ^ [_246456], _246456))], (534 ^ _229231) ^ [] : [-(v1_membered(524 ^ [_246456]))], (536 ^ _229231) ^ [] : [-(v2_membered(524 ^ [_246456]))], (538 ^ _229231) ^ [] : [-(v3_membered(524 ^ [_246456]))], (540 ^ _229231) ^ [] : [-(v4_membered(524 ^ [_246456]))], (542 ^ _229231) ^ [] : [-(v5_membered(524 ^ [_246456]))], (544 ^ _229231) ^ [] : [-(boundary_set(524 ^ [_246456], _246456))], (546 ^ _229231) ^ [] : [-(nowhere_dense(524 ^ [_246456], _246456))]], topological_space(_246456), top_str(_246456)], (549 ^ _229231) ^ [] : [empty(547 ^ [])], (551 ^ _229231) ^ [] : [-(finite(547 ^ []))], (553 ^ _229231) ^ [_247753] : [-(empty(_247753)), 557 ^ _229231 : [(558 ^ _229231) ^ [] : [-(element(556 ^ [_247753], powerset(_247753)))], (560 ^ _229231) ^ [] : [empty(556 ^ [_247753])], (562 ^ _229231) ^ [] : [-(finite(556 ^ [_247753]))]]], (564 ^ _229231) ^ [_248165] : [finite(_248165), 567 ^ _229231 : [(568 ^ _229231) ^ [_248297] : [element(_248297, powerset(_248165)), -(finite(_248297))]]], (574 ^ _229231) ^ [_248516, _248518] : [-(finite(cartesian_product2(_248518, _248516))), finite(_248518), finite(_248516)], (584 ^ _229231) ^ [_248801] : [-(empty(_248801)), 588 ^ _229231 : [(589 ^ _229231) ^ [] : [-(element(587 ^ [_248801], powerset(_248801)))], (591 ^ _229231) ^ [] : [empty(587 ^ [_248801])], (593 ^ _229231) ^ [] : [-(finite(587 ^ [_248801]))]]], (595 ^ _229231) ^ [_249213] : [603 ^ _229231 : [(604 ^ _229231) ^ [] : [-(element(602 ^ [_249213], powerset(the_carrier(_249213))))], (606 ^ _229231) ^ [] : [-(open_subset(602 ^ [_249213], _249213))]], topological_space(_249213), top_str(_249213)], (608 ^ _229231) ^ [_249631] : [616 ^ _229231 : [(617 ^ _229231) ^ [] : [-(element(615 ^ [_249631], powerset(the_carrier(_249631))))], (619 ^ _229231) ^ [] : [-(open_subset(615 ^ [_249631], _249631))], (621 ^ _229231) ^ [] : [-(closed_subset(615 ^ [_249631], _249631))]], topological_space(_249631), top_str(_249631)], (623 ^ _229231) ^ [_250132] : [635 ^ _229231 : [(636 ^ _229231) ^ [] : [-(element(634 ^ [_250132], powerset(the_carrier(_250132))))], (638 ^ _229231) ^ [] : [empty(634 ^ [_250132])], (640 ^ _229231) ^ [] : [-(open_subset(634 ^ [_250132], _250132))], (642 ^ _229231) ^ [] : [-(closed_subset(634 ^ [_250132], _250132))]], -(empty_carrier(_250132)), topological_space(_250132), top_str(_250132)], (644 ^ _229231) ^ [_250802] : [topological_space(_250802), top_str(_250802), 651 ^ _229231 : [(652 ^ _229231) ^ [_251026] : [element(_251026, powerset(the_carrier(_250802))), nowhere_dense(_251026, _250802), -(boundary_set(_251026, _250802))]]], (662 ^ _229231) ^ [_251328] : [topological_space(_251328), top_str(_251328), 669 ^ _229231 : [(670 ^ _229231) ^ [_251564] : [element(_251564, powerset(the_carrier(_251328))), 681 ^ _229231 : [(682 ^ _229231) ^ [] : [-(boundary_set(_251564, _251328))], (684 ^ _229231) ^ [] : [-(nowhere_dense(_251564, _251328))]], closed_subset(_251564, _251328), boundary_set(_251564, _251328)]]], (686 ^ _229231) ^ [_252030] : [topological_space(_252030), top_str(_252030), 693 ^ _229231 : [(694 ^ _229231) ^ [_252308] : [element(_252308, powerset(the_carrier(_252030))), 705 ^ _229231 : [(706 ^ _229231) ^ [] : [-(empty(_252308))], (708 ^ _229231) ^ [] : [-(open_subset(_252308, _252030))], (710 ^ _229231) ^ [] : [-(closed_subset(_252308, _252030))], (712 ^ _229231) ^ [] : [-(v1_membered(_252308))], (714 ^ _229231) ^ [] : [-(v2_membered(_252308))], (716 ^ _229231) ^ [] : [-(v3_membered(_252308))], (718 ^ _229231) ^ [] : [-(v4_membered(_252308))], (720 ^ _229231) ^ [] : [-(v5_membered(_252308))], (722 ^ _229231) ^ [] : [-(boundary_set(_252308, _252030))], (724 ^ _229231) ^ [] : [-(nowhere_dense(_252308, _252030))]], open_subset(_252308, _252030), nowhere_dense(_252308, _252030)]]], (727 ^ _229231) ^ [_253414] : [-(element(725 ^ [_253414], powerset(powerset(_253414))))], (729 ^ _229231) ^ [_253486] : [empty(725 ^ [_253486])], (731 ^ _229231) ^ [_253534] : [-(finite(725 ^ [_253534]))], (733 ^ _229231) ^ [_253635] : [one_sorted_str(_253635), 737 ^ _229231 : [(738 ^ _229231) ^ [] : [-(element(736 ^ [_253635], powerset(powerset(the_carrier(_253635)))))], (740 ^ _229231) ^ [] : [empty(736 ^ [_253635])], (742 ^ _229231) ^ [] : [-(finite(736 ^ [_253635]))]]], (744 ^ _229231) ^ [_254098, _254100, _254102, _254104] : [763 ^ _229231 : [(764 ^ _229231) ^ [_254726, _254728, _254730, _254732] : [net_str_of(_254104, _254102, _254100, _254098) = net_str_of(_254732, _254730, _254728, _254726), 767 ^ _229231 : [(768 ^ _229231) ^ [] : [-(_254104 = _254732)], (770 ^ _229231) ^ [] : [-(_254102 = _254730)], (772 ^ _229231) ^ [] : [-(_254100 = _254728)], (774 ^ _229231) ^ [] : [-(_254098 = _254726)]]]], one_sorted_str(_254104), relation_of2(_254100, _254102, _254102), function(_254098), quasi_total(_254098, _254102, the_carrier(_254104)), relation_of2(_254098, _254102, the_carrier(_254104))], (776 ^ _229231) ^ [_255292, _255294, _255296, _255298] : [795 ^ _229231 : [(796 ^ _229231) ^ [] : [-(strict_net_str(net_str_of(_255298, _255296, _255294, _255292), _255298))], (798 ^ _229231) ^ [] : [-(net_str(net_str_of(_255298, _255296, _255294, _255292), _255298))]], one_sorted_str(_255298), relation_of2(_255294, _255296, _255296), function(_255292), quasi_total(_255292, _255296, the_carrier(_255298)), relation_of2(_255292, _255296, the_carrier(_255298))], (800 ^ _229231) ^ [] : [true___, -(true___)], (806 ^ _229231) ^ [_256116] : [rel_str(_256116), -(relation_of2_as_subset(the_InternalRel(_256116), the_carrier(_256116), the_carrier(_256116)))], (812 ^ _229231) ^ [_256318] : [-(empty(_256318)), 816 ^ _229231 : [(817 ^ _229231) ^ [] : [-(element(815 ^ [_256318], powerset(_256318)))], (819 ^ _229231) ^ [] : [empty(815 ^ [_256318])]]], (821 ^ _229231) ^ [_256664, _256666] : [empty(cartesian_product2(_256666, _256664)), -(empty(_256666)), -(empty(_256664))], (832 ^ _229231) ^ [_257007] : [-(element(830 ^ [_257007], powerset(_257007)))], (834 ^ _229231) ^ [_257058] : [-(empty(830 ^ [_257058]))], (836 ^ _229231) ^ [_257157] : [empty(_257157), -(finite(_257157))], (842 ^ _229231) ^ [_257343] : [850 ^ _229231 : [(851 ^ _229231) ^ [] : [-(element(849 ^ [_257343], powerset(the_carrier(_257343))))], (853 ^ _229231) ^ [] : [empty(849 ^ [_257343])]], -(empty_carrier(_257343)), one_sorted_str(_257343)], (855 ^ _229231) ^ [_257764] : [863 ^ _229231 : [(864 ^ _229231) ^ [] : [-(element(862 ^ [_257764], powerset(the_carrier(_257764))))], (866 ^ _229231) ^ [] : [-(closed_subset(862 ^ [_257764], _257764))]], topological_space(_257764), top_str(_257764)], (868 ^ _229231) ^ [_258182] : [880 ^ _229231 : [(881 ^ _229231) ^ [] : [-(element(879 ^ [_258182], powerset(the_carrier(_258182))))], (883 ^ _229231) ^ [] : [empty(879 ^ [_258182])], (885 ^ _229231) ^ [] : [-(closed_subset(879 ^ [_258182], _258182))]], -(empty_carrier(_258182)), topological_space(_258182), top_str(_258182)], (887 ^ _229231) ^ [_258769] : [topological_space(_258769), top_str(_258769), 894 ^ _229231 : [(895 ^ _229231) ^ [_258998] : [element(_258998, powerset(the_carrier(_258769))), empty(_258998), 902 ^ _229231 : [(903 ^ _229231) ^ [] : [-(open_subset(_258998, _258769))], (905 ^ _229231) ^ [] : [-(closed_subset(_258998, _258769))]]]]], (907 ^ _229231) ^ [_259373] : [top_str(_259373), 910 ^ _229231 : [(911 ^ _229231) ^ [_259513] : [element(_259513, powerset(the_carrier(_259373))), empty(_259513), -(boundary_set(_259513, _259373))]]], (921 ^ _229231) ^ [_259811] : [topological_space(_259811), top_str(_259811), 928 ^ _229231 : [(929 ^ _229231) ^ [_260034] : [element(_260034, powerset(the_carrier(_259811))), empty(_260034), -(nowhere_dense(_260034, _259811))]]], (939 ^ _229231) ^ [_260362, _260364, _260366] : [element(_260362, powerset(cartesian_product2(_260366, _260364))), -(relation(_260362))], (945 ^ _229231) ^ [_260614, _260616, _260618, _260620] : [968 ^ _229231 : [(969 ^ _229231) ^ [] : [empty_carrier(net_str_of(_260620, _260618, _260616, _260614))], (971 ^ _229231) ^ [] : [-(strict_net_str(net_str_of(_260620, _260618, _260616, _260614), _260620))]], one_sorted_str(_260620), -(empty(_260618)), relation_of2(_260616, _260618, _260618), function(_260614), quasi_total(_260614, _260618, the_carrier(_260620)), relation_of2(_260614, _260618, the_carrier(_260620))], (974 ^ _229231) ^ [] : [-(empty(972 ^ []))], (976 ^ _229231) ^ [] : [-(relation(972 ^ []))], (978 ^ _229231) ^ [_261565] : [empty(_261565), -(relation(_261565))], (985 ^ _229231) ^ [] : [empty(983 ^ [])], (987 ^ _229231) ^ [] : [-(relation(983 ^ []))], (989 ^ _229231) ^ [_261901] : [empty(relation_rng(_261901)), -(empty(_261901)), relation(_261901)], (999 ^ _229231) ^ [_262178] : [empty(_262178), 1002 ^ _229231 : [(1003 ^ _229231) ^ [] : [-(empty(relation_rng(_262178)))], (1005 ^ _229231) ^ [] : [-(relation(relation_rng(_262178)))]]], (1007 ^ _229231) ^ [_262457, _262459] : [one_sorted_str(_262459), net_str(_262457, _262459), strict_net_str(_262457, _262459), -(_262457 = net_str_of(_262459, the_carrier(_262457), the_InternalRel(_262457), the_mapping(_262459, _262457)))], (1021 ^ _229231) ^ [_262912, _262914, _262916] : [relation_of2_as_subset(_262912, _262916, _262914), -(relation_of2(_262912, _262916, _262914))], (1027 ^ _229231) ^ [_263084, _263086, _263088] : [relation_of2(_263084, _263088, _263086), -(relation_of2_as_subset(_263084, _263088, _263086))], (1033 ^ _229231) ^ [] : [true___, -(true___)], (1039 ^ _229231) ^ [] : [true___, -(true___)], (1045 ^ _229231) ^ [_263558, _263560, _263562] : [1064 ^ _229231 : [(1065 ^ _229231) ^ [] : [-(strict_net_str(netstr_restr_to_element(_263562, _263560, _263558), _263562))], (1067 ^ _229231) ^ [] : [-(net_str(netstr_restr_to_element(_263562, _263560, _263558), _263562))]], -(empty_carrier(_263562)), one_sorted_str(_263562), -(empty_carrier(_263560)), net_str(_263560, _263562), element(_263558, the_carrier(_263560))], (1069 ^ _229231) ^ [_264229] : [rel_str(_264229), -(one_sorted_str(_264229))], (1075 ^ _229231) ^ [] : [true___, -(true___)], (1081 ^ _229231) ^ [] : [true___, -(true___)], (1087 ^ _229231) ^ [_264681, _264683, _264685] : [relation_of2_as_subset(_264681, _264685, _264683), -(element(_264681, powerset(cartesian_product2(_264685, _264683))))], (1093 ^ _229231) ^ [_264909, _264911] : [1116 ^ _229231 : [(1117 ^ _229231) ^ [_265505] : [subnet(_265505, _264911, _264909), 1120 ^ _229231 : [(1121 ^ _229231) ^ [] : [empty_carrier(_265505)], (1123 ^ _229231) ^ [] : [-(transitive_relstr(_265505))], (1125 ^ _229231) ^ [] : [-(directed_relstr(_265505))], (1127 ^ _229231) ^ [] : [-(net_str(_265505, _264911))]]]], -(empty_carrier(_264911)), one_sorted_str(_264911), -(empty_carrier(_264909)), transitive_relstr(_264909), directed_relstr(_264909), net_str(_264909, _264911)], (1129 ^ _229231) ^ [_265926] : [empty(powerset(_265926))], (1132 ^ _229231) ^ [] : [-(one_sorted_str(1130 ^ []))], (1134 ^ _229231) ^ [] : [empty_carrier(1130 ^ [])], (1136 ^ _229231) ^ [_266170] : [empty(the_carrier(_266170)), -(empty_carrier(_266170)), one_sorted_str(_266170)], (1146 ^ _229231) ^ [_266461, _266463] : [-(closed_subset(topstr_closure(_266463, _266461), _266463)), topological_space(_266463), top_str(_266463), element(_266461, powerset(the_carrier(_266463)))], (1160 ^ _229231) ^ [_266845] : [one_sorted_str(_266845), 1164 ^ _229231 : [(1165 ^ _229231) ^ [] : [-(net_str(1163 ^ [_266845], _266845))], (1167 ^ _229231) ^ [] : [-(strict_net_str(1163 ^ [_266845], _266845))]]], (1169 ^ _229231) ^ [_267196, _267198, _267200] : [1192 ^ _229231 : [(1193 ^ _229231) ^ [] : [empty_carrier(netstr_restr_to_element(_267200, _267198, _267196))], (1195 ^ _229231) ^ [] : [-(strict_net_str(netstr_restr_to_element(_267200, _267198, _267196), _267200))]], -(empty_carrier(_267200)), one_sorted_str(_267200), -(empty_carrier(_267198)), directed_relstr(_267198), net_str(_267198, _267200), element(_267196, the_carrier(_267198))], (1197 ^ _229231) ^ [_267985, _267987, _267989] : [1224 ^ _229231 : [(1225 ^ _229231) ^ [] : [empty_carrier(netstr_restr_to_element(_267989, _267987, _267985))], (1227 ^ _229231) ^ [] : [-(transitive_relstr(netstr_restr_to_element(_267989, _267987, _267985)))], (1229 ^ _229231) ^ [] : [-(strict_net_str(netstr_restr_to_element(_267989, _267987, _267985), _267989))], (1231 ^ _229231) ^ [] : [-(directed_relstr(netstr_restr_to_element(_267989, _267987, _267985)))]], -(empty_carrier(_267989)), one_sorted_str(_267989), -(empty_carrier(_267987)), transitive_relstr(_267987), directed_relstr(_267987), net_str(_267987, _267989), element(_267985, the_carrier(_267987))], (1233 ^ _229231) ^ [_269015, _269017] : [1257 ^ _229231 : [(1258 ^ _229231) ^ [] : [-(subnet(1256 ^ [_269015, _269017], _269017, _269015))], (1260 ^ _229231) ^ [] : [empty_carrier(1256 ^ [_269015, _269017])], (1262 ^ _229231) ^ [] : [-(transitive_relstr(1256 ^ [_269015, _269017]))], (1264 ^ _229231) ^ [] : [-(strict_net_str(1256 ^ [_269015, _269017], _269017))], (1266 ^ _229231) ^ [] : [-(directed_relstr(1256 ^ [_269015, _269017]))]], -(empty_carrier(_269017)), one_sorted_str(_269017), -(empty_carrier(_269015)), transitive_relstr(_269015), directed_relstr(_269015), net_str(_269015, _269017)], (1268 ^ _229231) ^ [_270069, _270071] : [1283 ^ _229231 : [(1284 ^ _229231) ^ [] : [empty(the_mapping(_270071, _270069))], (1286 ^ _229231) ^ [] : [-(relation(the_mapping(_270071, _270069)))], (1288 ^ _229231) ^ [] : [-(function(the_mapping(_270071, _270069)))], (1290 ^ _229231) ^ [] : [-(quasi_total(the_mapping(_270071, _270069), the_carrier(_270069), the_carrier(_270071)))]], -(empty_carrier(_270071)), one_sorted_str(_270071), -(empty_carrier(_270069)), net_str(_270069, _270071)], (1292 ^ _229231) ^ [_270798, _270800] : [in(_270800, _270798), in(_270798, _270800)], (1298 ^ _229231) ^ [_271023, _271025, _271027] : [relation_of2(_271023, _271027, _271025), -(relation_rng_as_subset(_271027, _271025, _271023) = relation_rng(_271023))], (1304 ^ _229231) ^ [_271267, _271269, _271271] : [-(subnetstr_of_element(_271271, _271269, _271267) = netstr_restr_to_element(_271271, _271269, _271267)), -(empty_carrier(_271271)), one_sorted_str(_271271), -(empty_carrier(_271269)), transitive_relstr(_271269), directed_relstr(_271269), net_str(_271269, _271271), element(_271267, the_carrier(_271269))], (1334 ^ _229231) ^ [_272071, _272073, _272075] : [relation_of2(_272071, _272075, _272073), -(element(relation_rng_as_subset(_272075, _272073, _272071), powerset(_272073)))], (1340 ^ _229231) ^ [_272301, _272303] : [-(element(topstr_closure(_272303, _272301), powerset(the_carrier(_272303)))), top_str(_272303), element(_272301, powerset(the_carrier(_272303)))], (1350 ^ _229231) ^ [_272634, _272636, _272638] : [1377 ^ _229231 : [(1378 ^ _229231) ^ [] : [-(strict_net_str(subnetstr_of_element(_272638, _272636, _272634), _272638))], (1380 ^ _229231) ^ [] : [-(subnet(subnetstr_of_element(_272638, _272636, _272634), _272638, _272636))]], -(empty_carrier(_272638)), one_sorted_str(_272638), -(empty_carrier(_272636)), transitive_relstr(_272636), directed_relstr(_272636), net_str(_272636, _272638), element(_272634, the_carrier(_272636))], (1382 ^ _229231) ^ [_273489] : [top_str(_273489), -(one_sorted_str(_273489))], (1388 ^ _229231) ^ [_273675] : [one_sorted_str(_273675), 1391 ^ _229231 : [(1392 ^ _229231) ^ [_273805] : [net_str(_273805, _273675), -(rel_str(_273805))]]], (1398 ^ _229231) ^ [] : [true___, -(true___)], (1404 ^ _229231) ^ [_274139, _274141] : [1419 ^ _229231 : [(1420 ^ _229231) ^ [_274548] : [netstr_induced_subset(_274548, _274141, _274139), -(element(_274548, powerset(the_carrier(_274141))))]], -(empty_carrier(_274141)), one_sorted_str(_274141), -(empty_carrier(_274139)), net_str(_274139, _274141)], (1426 ^ _229231) ^ [] : [true___, -(true___)], (1432 ^ _229231) ^ [_274902, _274904] : [1439 ^ _229231 : [(1440 ^ _229231) ^ [] : [-(function(the_mapping(_274904, _274902)))], (1442 ^ _229231) ^ [] : [-(quasi_total(the_mapping(_274904, _274902), the_carrier(_274902), the_carrier(_274904)))], (1444 ^ _229231) ^ [] : [-(relation_of2_as_subset(the_mapping(_274904, _274902), the_carrier(_274902), the_carrier(_274904)))]], one_sorted_str(_274904), net_str(_274902, _274904)], (1446 ^ _229231) ^ [_275364, _275366] : [-(_275366 = _275364), 1450 ^ _229231 : [(1451 ^ _229231) ^ [] : [-(in(1447 ^ [_275364, _275366], _275366))], (1453 ^ _229231) ^ [] : [in(1447 ^ [_275364, _275366], _275364)]], 1454 ^ _229231 : [(1455 ^ _229231) ^ [] : [-(in(1447 ^ [_275364, _275366], _275364))], (1457 ^ _229231) ^ [] : [in(1447 ^ [_275364, _275366], _275366)]]]], input).
% 35.02/34.56 ncf('1',plain,[1478 ^ [] = 1479 ^ []],start(1569 ^ 0)).
% 35.02/34.56 ncf('1.1',plain,[-(1478 ^ [] = 1479 ^ []), 1451 : -(in(1447 ^ [1479 ^ [], 1478 ^ []], 1478 ^ [])), 1455 : -(in(1447 ^ [1479 ^ [], 1478 ^ []], 1479 ^ []))],extension(1446 ^ 1,bind([[_275364, _275366], [1479 ^ [], 1478 ^ []]]))).
% 35.02/34.56 ncf('1.1.1',plain,[in(1447 ^ [1479 ^ [], 1478 ^ []], 1478 ^ []), 1485 : -(in(1447 ^ [1479 ^ [], 1478 ^ []], the_carrier(1461 ^ [])))],extension(1481 ^ 4,bind([[_278141], [1447 ^ [1479 ^ [], 1478 ^ []]]]))).
% 35.02/34.56 ncf('1.1.1.1',plain,[in(1447 ^ [1479 ^ [], 1478 ^ []], the_carrier(1461 ^ [])), -(in(1447 ^ [1479 ^ [], 1478 ^ []], 1479 ^ [])), 1549 : netstr_induced_subset(1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1460 ^ [], 1461 ^ []), 1553 : element(1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], the_carrier(1461 ^ [])), 1553 : 1477 ^ [] = topstr_closure(1460 ^ [], 1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]), 1553 : 1447 ^ [1479 ^ [], 1478 ^ []] = 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1553 : 1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]] = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])))],extension(1543 ^ 7,bind([[_280597, _280812, _280985], [1447 ^ [1479 ^ [], 1478 ^ []], 1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]]]))).
% 35.02/34.56 ncf('1.1.1.1.1',plain,[in(1447 ^ [1479 ^ [], 1478 ^ []], 1479 ^ [])],extension(1453 ^ 8)).
% 35.02/34.56 ncf('1.1.1.1.2',plain,[-(netstr_induced_subset(1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1460 ^ [], 1461 ^ []))],extension(1488 ^ 10)).
% 35.02/34.56 ncf('1.1.1.1.3',plain,[-(element(1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], the_carrier(1461 ^ [])))],extension(1491 ^ 12)).
% 35.02/34.56 ncf('1.1.1.1.4',plain,[-(1477 ^ [] = topstr_closure(1460 ^ [], 1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]))],extension(1493 ^ 12)).
% 35.02/34.56 ncf('1.1.1.1.5',plain,[-(1447 ^ [1479 ^ [], 1478 ^ []] = 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])],extension(1495 ^ 12)).
% 35.02/34.56 ncf('1.1.1.1.6',plain,[-(1486 ^ [1447 ^ [1479 ^ [], 1478 ^ []]] = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], 1489 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]))))],extension(1497 ^ 12)).
% 35.02/34.56 ncf('1.1.2',plain,[in(1447 ^ [1479 ^ [], 1478 ^ []], 1479 ^ []), 1529 : -(in(1447 ^ [1479 ^ [], 1478 ^ []], the_carrier(1461 ^ [])))],extension(1525 ^ 4,bind([[_279813], [1447 ^ [1479 ^ [], 1478 ^ []]]]))).
% 35.02/34.56 ncf('1.1.2.1',plain,[in(1447 ^ [1479 ^ [], 1478 ^ []], the_carrier(1461 ^ [])), -(in(1447 ^ [1479 ^ [], 1478 ^ []], 1478 ^ [])), 1505 : netstr_induced_subset(1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1460 ^ [], 1461 ^ []), 1509 : element(1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], the_carrier(1461 ^ [])), 1509 : 1477 ^ [] = topstr_closure(1460 ^ [], 1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]), 1509 : 1447 ^ [1479 ^ [], 1478 ^ []] = 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1509 : 1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]] = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])))],extension(1499 ^ 7,bind([[_278925, _279140, _279313], [1447 ^ [1479 ^ [], 1478 ^ []], 1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]]]))).
% 35.02/34.56 ncf('1.1.2.1.1',plain,[in(1447 ^ [1479 ^ [], 1478 ^ []], 1478 ^ [])],extension(1457 ^ 8)).
% 35.02/34.56 ncf('1.1.2.1.2',plain,[-(netstr_induced_subset(1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], 1460 ^ [], 1461 ^ []))],extension(1532 ^ 10)).
% 35.02/34.56 ncf('1.1.2.1.3',plain,[-(element(1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]], the_carrier(1461 ^ [])))],extension(1535 ^ 12)).
% 35.02/34.56 ncf('1.1.2.1.4',plain,[-(1477 ^ [] = topstr_closure(1460 ^ [], 1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]))],extension(1537 ^ 12)).
% 35.02/34.56 ncf('1.1.2.1.5',plain,[-(1447 ^ [1479 ^ [], 1478 ^ []] = 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])],extension(1539 ^ 12)).
% 35.02/34.56 ncf('1.1.2.1.6',plain,[-(1530 ^ [1447 ^ [1479 ^ [], 1478 ^ []]] = relation_rng_as_subset(the_carrier(subnetstr_of_element(1460 ^ [], 1461 ^ [], 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]])), the_carrier(1460 ^ []), the_mapping(1460 ^ [], subnetstr_of_element(1460 ^ [], 1461 ^ [], 1533 ^ [1447 ^ [1479 ^ [], 1478 ^ []]]))))],extension(1541 ^ 12)).
% 35.02/34.56 %-----------------------------------------------------
% 35.02/34.56 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------