%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU294+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:01 EDT 2023
% Result : Theorem 2.73s 3.39s
% Output : Proof 2.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SEU294+2 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.09 % Command : nanocop.sh %s %d
% 0.10/0.28 % Computer : n032.cluster.edu
% 0.10/0.28 % Model : x86_64 x86_64
% 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.28 % Memory : 8042.1875MB
% 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.28 % CPULimit : 300
% 0.10/0.28 % WCLimit : 300
% 0.10/0.28 % DateTime : Thu May 18 13:43:04 EDT 2023
% 0.10/0.29 % CPUTime :
% 2.73/3.39
% 2.73/3.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.73/3.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.73/3.39 %-----------------------------------------------------
% 2.73/3.39 ncf(matrix, plain, [(7252 ^ _39627) ^ [] : [-(subset(7249 ^ [], 7250 ^ []))], (7254 ^ _39627) ^ [] : [-(finite(7250 ^ []))], (7256 ^ _39627) ^ [] : [finite(7249 ^ [])], (458 ^ _39627) ^ [_45905, _45907, _45909, _45911, _45913, _45915] : [-(unordered_triple(_45915, _45911, _45907) = unordered_triple(_45913, _45909, _45905)), _45915 = _45913, _45911 = _45909, _45907 = _45905], (472 ^ _39627) ^ [_46126, _46128] : [_46128 = _46126, -(set_meet(_46128) = set_meet(_46126))], (478 ^ _39627) ^ [_46211, _46213, _46215, _46217] : [-(relation_image(_46217, _46213) = relation_image(_46215, _46211)), _46217 = _46215, _46213 = _46211], (488 ^ _39627) ^ [_46360, _46362, _46364, _46366] : [-(relation_rng_restriction(_46366, _46362) = relation_rng_restriction(_46364, _46360)), _46366 = _46364, _46362 = _46360], (498 ^ _39627) ^ [_46509, _46511, _46513, _46515] : [-(cartesian_product2(_46515, _46511) = cartesian_product2(_46513, _46509)), _46515 = _46513, _46511 = _46509], (508 ^ _39627) ^ [_46658, _46660, _46662, _46664] : [-(fiber(_46664, _46660) = fiber(_46662, _46658)), _46664 = _46662, _46660 = _46658], (518 ^ _39627) ^ [_46807, _46809, _46811, _46813, _46815, _46817] : [-(relation_dom_as_subset(_46817, _46813, _46809) = relation_dom_as_subset(_46815, _46811, _46807)), _46817 = _46815, _46813 = _46811, _46809 = _46807], (532 ^ _39627) ^ [_47028, _47030, _47032, _47034, _47036, _47038] : [-(relation_rng_as_subset(_47038, _47034, _47030) = relation_rng_as_subset(_47036, _47032, _47028)), _47038 = _47036, _47034 = _47032, _47030 = _47028], (546 ^ _39627) ^ [_47249, _47251] : [_47251 = _47249, -(relation_inverse(_47251) = relation_inverse(_47249))], (552 ^ _39627) ^ [_47334, _47336, _47338, _47340] : [-(relation_restriction(_47340, _47336) = relation_restriction(_47338, _47334)), _47340 = _47338, _47336 = _47334], (562 ^ _39627) ^ [_47483, _47485] : [_47485 = _47483, -(succ(_47485) = succ(_47483))], (568 ^ _39627) ^ [_47568, _47570, _47572, _47574] : [-(relation_inverse_image(_47574, _47570) = relation_inverse_image(_47572, _47568)), _47574 = _47572, _47570 = _47568], (578 ^ _39627) ^ [_47717, _47719, _47721, _47723] : [-(union_of_subsets(_47723, _47719) = union_of_subsets(_47721, _47717)), _47723 = _47721, _47719 = _47717], (588 ^ _39627) ^ [_47866, _47868, _47870, _47872] : [-(complements_of_subsets(_47872, _47868) = complements_of_subsets(_47870, _47866)), _47872 = _47870, _47868 = _47866], (598 ^ _39627) ^ [_48015, _48017, _48019, _48021, _48023, _48025] : [-(subset_difference(_48025, _48021, _48017) = subset_difference(_48023, _48019, _48015)), _48025 = _48023, _48021 = _48019, _48017 = _48015], (612 ^ _39627) ^ [_48236, _48238] : [_48238 = _48236, -(cast_to_subset(_48238) = cast_to_subset(_48236))], (618 ^ _39627) ^ [_48321, _48323, _48325, _48327] : [-(meet_of_subsets(_48327, _48323) = meet_of_subsets(_48325, _48321)), _48327 = _48325, _48323 = _48321], (628 ^ _39627) ^ [_48470, _48472, _48474, _48476] : [-(subset_complement(_48476, _48472) = subset_complement(_48474, _48470)), _48476 = _48474, _48472 = _48470], (638 ^ _39627) ^ [_48619, _48621] : [_48621 = _48619, -(function_inverse(_48621) = function_inverse(_48619))], (644 ^ _39627) ^ [_48704, _48706] : [_48706 = _48704, -(pair_first(_48706) = pair_first(_48704))], (650 ^ _39627) ^ [_48789, _48791] : [_48791 = _48789, -(pair_second(_48791) = pair_second(_48789))], (656 ^ _39627) ^ [_48874, _48876] : [_48876 = _48874, -(inclusion_relation(_48876) = inclusion_relation(_48874))], (662 ^ _39627) ^ [_48959, _48961, _48963, _48965] : [-(set_difference(_48965, _48961) = set_difference(_48963, _48959)), _48965 = _48963, _48961 = _48959], (672 ^ _39627) ^ [_49108, _49110, _49112, _49114] : [-(ordered_pair(_49114, _49110) = ordered_pair(_49112, _49108)), _49114 = _49112, _49110 = _49108], (682 ^ _39627) ^ [_49257, _49259, _49261, _49263] : [-(apply(_49263, _49259) = apply(_49261, _49257)), _49263 = _49261, _49259 = _49257], (692 ^ _39627) ^ [_49406, _49408] : [_49408 = _49406, -(relation_field(_49408) = relation_field(_49406))], (698 ^ _39627) ^ [_49491, _49493, _49495, _49497] : [-(set_union2(_49497, _49493) = set_union2(_49495, _49491)), _49497 = _49495, _49493 = _49491], (708 ^ _39627) ^ [_49640, _49642, _49644, _49646] : [-(set_intersection2(_49646, _49642) = set_intersection2(_49644, _49640)), _49646 = _49644, _49642 = _49640], (718 ^ _39627) ^ [_49789, _49791] : [_49791 = _49789, -(relation_dom(_49791) = relation_dom(_49789))], (724 ^ _39627) ^ [_49874, _49876, _49878, _49880] : [-(relation_composition(_49880, _49876) = relation_composition(_49878, _49874)), _49880 = _49878, _49876 = _49874], (734 ^ _39627) ^ [_50023, _50025] : [_50025 = _50023, -(identity_relation(_50025) = identity_relation(_50023))], (740 ^ _39627) ^ [_50108, _50110, _50112, _50114] : [-(relation_dom_restriction(_50114, _50110) = relation_dom_restriction(_50112, _50108)), _50114 = _50112, _50110 = _50108], (750 ^ _39627) ^ [_50257, _50259] : [_50259 = _50257, -(relation_rng(_50259) = relation_rng(_50257))], (756 ^ _39627) ^ [_50342, _50344] : [_50344 = _50342, -(union(_50344) = union(_50342))], (762 ^ _39627) ^ [_50427, _50429] : [_50429 = _50427, -(powerset(_50429) = powerset(_50427))], (768 ^ _39627) ^ [_50512, _50514] : [_50514 = _50512, -(singleton(_50514) = singleton(_50512))], (774 ^ _39627) ^ [_50593, _50595, _50597, _50599] : [-(unordered_pair(_50599, _50595) = unordered_pair(_50597, _50593)), _50599 = _50597, _50595 = _50593], (2 ^ _39627) ^ [_39657] : [-(_39657 = _39657)], (4 ^ _39627) ^ [_39680, _39682] : [_39682 = _39680, -(_39680 = _39682)], (10 ^ _39627) ^ [_39753, _39755, _39757] : [-(_39757 = _39753), _39757 = _39755, _39755 = _39753], (20 ^ _39627) ^ [_39890, _39892, _39894, _39896] : [-(is_antisymmetric_in(_39894, _39890)), is_antisymmetric_in(_39896, _39892), _39896 = _39894, _39892 = _39890], (34 ^ _39627) ^ [_40083, _40085, _40087, _40089] : [-(is_connected_in(_40087, _40083)), is_connected_in(_40089, _40085), _40089 = _40087, _40085 = _40083], (48 ^ _39627) ^ [_40276, _40278, _40280, _40282] : [-(is_transitive_in(_40280, _40276)), is_transitive_in(_40282, _40278), _40282 = _40280, _40278 = _40276], (62 ^ _39627) ^ [_40469, _40471, _40473, _40475] : [-(is_reflexive_in(_40473, _40469)), is_reflexive_in(_40475, _40471), _40475 = _40473, _40471 = _40469], (76 ^ _39627) ^ [_40662, _40664] : [-(natural(_40662)), _40664 = _40662, natural(_40664)], (86 ^ _39627) ^ [_40787, _40789] : [-(epsilon_connected(_40787)), _40789 = _40787, epsilon_connected(_40789)], (96 ^ _39627) ^ [_40912, _40914] : [-(relation_empty_yielding(_40912)), _40914 = _40912, relation_empty_yielding(_40914)], (106 ^ _39627) ^ [_41037, _41039, _41041, _41043, _41045, _41047] : [-(relation_of2(_41045, _41041, _41037)), relation_of2(_41047, _41043, _41039), _41047 = _41045, _41043 = _41041, _41039 = _41037], (124 ^ _39627) ^ [_41306, _41308, _41310, _41312] : [-(equipotent(_41310, _41306)), equipotent(_41312, _41308), _41312 = _41310, _41308 = _41306], (138 ^ _39627) ^ [_41499, _41501] : [-(epsilon_transitive(_41499)), _41501 = _41499, epsilon_transitive(_41501)], (148 ^ _39627) ^ [_41624, _41626, _41628, _41630] : [-(ordinal_subset(_41628, _41624)), ordinal_subset(_41630, _41626), _41630 = _41628, _41626 = _41624], (162 ^ _39627) ^ [_41817, _41819] : [-(being_limit_ordinal(_41817)), _41819 = _41817, being_limit_ordinal(_41819)], (172 ^ _39627) ^ [_41942, _41944] : [-(reflexive(_41942)), _41944 = _41942, reflexive(_41944)], (182 ^ _39627) ^ [_42067, _42069] : [-(transitive(_42067)), _42069 = _42067, transitive(_42069)], (192 ^ _39627) ^ [_42192, _42194] : [-(connected(_42192)), _42194 = _42192, connected(_42194)], (202 ^ _39627) ^ [_42317, _42319, _42321, _42323, _42325, _42327] : [-(relation_isomorphism(_42325, _42321, _42317)), relation_isomorphism(_42327, _42323, _42319), _42327 = _42325, _42323 = _42321, _42319 = _42317], (220 ^ _39627) ^ [_42586, _42588, _42590, _42592] : [-(element(_42590, _42586)), element(_42592, _42588), _42592 = _42590, _42588 = _42586], (234 ^ _39627) ^ [_42779, _42781, _42783, _42785] : [-(is_well_founded_in(_42783, _42779)), is_well_founded_in(_42785, _42781), _42785 = _42783, _42781 = _42779], (248 ^ _39627) ^ [_42972, _42974] : [-(antisymmetric(_42972)), _42974 = _42972, antisymmetric(_42974)], (258 ^ _39627) ^ [_43097, _43099, _43101, _43103] : [-(proper_subset(_43101, _43097)), proper_subset(_43103, _43099), _43103 = _43101, _43099 = _43097], (272 ^ _39627) ^ [_43290, _43292] : [-(one_to_one(_43290)), _43292 = _43290, one_to_one(_43292)], (282 ^ _39627) ^ [_43415, _43417] : [-(well_founded_relation(_43415)), _43417 = _43415, well_founded_relation(_43417)], (292 ^ _39627) ^ [_43540, _43542] : [-(ordinal(_43540)), _43542 = _43540, ordinal(_43542)], (302 ^ _39627) ^ [_43665, _43667, _43669, _43671] : [-(disjoint(_43669, _43665)), disjoint(_43671, _43667), _43671 = _43669, _43667 = _43665], (316 ^ _39627) ^ [_43858, _43860] : [-(empty(_43858)), _43860 = _43858, empty(_43860)], (326 ^ _39627) ^ [_43983, _43985, _43987, _43989] : [-(well_orders(_43987, _43983)), well_orders(_43989, _43985), _43989 = _43987, _43985 = _43983], (340 ^ _39627) ^ [_44176, _44178] : [-(well_ordering(_44176)), _44178 = _44176, well_ordering(_44178)], (350 ^ _39627) ^ [_44301, _44303] : [-(relation(_44301)), _44303 = _44301, relation(_44303)], (360 ^ _39627) ^ [_44426, _44428] : [-(function(_44426)), _44428 = _44426, function(_44428)], (370 ^ _39627) ^ [_44551, _44553, _44555, _44557, _44559, _44561] : [-(quasi_total(_44559, _44555, _44551)), quasi_total(_44561, _44557, _44553), _44561 = _44559, _44557 = _44555, _44553 = _44551], (388 ^ _39627) ^ [_44820, _44822, _44824, _44826, _44828, _44830] : [-(relation_of2_as_subset(_44828, _44824, _44820)), relation_of2_as_subset(_44830, _44826, _44822), _44830 = _44828, _44826 = _44824, _44822 = _44820], (406 ^ _39627) ^ [_45089, _45091, _45093, _45095] : [-(are_equipotent(_45093, _45089)), are_equipotent(_45095, _45091), _45095 = _45093, _45091 = _45089], (420 ^ _39627) ^ [_45282, _45284, _45286, _45288] : [-(in(_45286, _45282)), in(_45288, _45284), _45288 = _45286, _45284 = _45282], (448 ^ _39627) ^ [_45664, _45666] : [-(finite(_45664)), _45666 = _45664, finite(_45666)], (434 ^ _39627) ^ [_45475, _45477, _45479, _45481] : [-(subset(_45479, _45475)), subset(_45481, _45477), _45481 = _45479, _45477 = _45475], (784 ^ _39627) ^ [_50849, _50851] : [in(_50851, _50849), in(_50849, _50851)], (790 ^ _39627) ^ [_50927, _50929] : [proper_subset(_50929, _50927), proper_subset(_50927, _50929)], (796 ^ _39627) ^ [_51005] : [ordinal(_51005), 799 ^ _39627 : [(800 ^ _39627) ^ [_51073] : [element(_51073, _51005), 803 ^ _39627 : [(804 ^ _39627) ^ [] : [-(epsilon_transitive(_51073))], (806 ^ _39627) ^ [] : [-(epsilon_connected(_51073))], (808 ^ _39627) ^ [] : [-(ordinal(_51073))]]]]], (810 ^ _39627) ^ [_51198] : [empty(_51198), -(finite(_51198))], (816 ^ _39627) ^ [_51269] : [empty(_51269), -(function(_51269))], (822 ^ _39627) ^ [_51340] : [ordinal(_51340), 825 ^ _39627 : [(826 ^ _39627) ^ [] : [-(epsilon_transitive(_51340))], (828 ^ _39627) ^ [] : [-(epsilon_connected(_51340))]]], (830 ^ _39627) ^ [_51435] : [empty(_51435), -(relation(_51435))], (836 ^ _39627) ^ [_51506, _51508, _51510] : [element(_51506, powerset(cartesian_product2(_51510, _51508))), -(relation(_51506))], (842 ^ _39627) ^ [_51593] : [849 ^ _39627 : [(850 ^ _39627) ^ [] : [-(epsilon_transitive(_51593))], (852 ^ _39627) ^ [] : [-(epsilon_connected(_51593))], (854 ^ _39627) ^ [] : [-(ordinal(_51593))], (856 ^ _39627) ^ [] : [-(natural(_51593))]], empty(_51593), ordinal(_51593)], (858 ^ _39627) ^ [_51780] : [finite(_51780), 861 ^ _39627 : [(862 ^ _39627) ^ [_51840] : [element(_51840, powerset(_51780)), -(finite(_51840))]]], (868 ^ _39627) ^ [_51923] : [879 ^ _39627 : [(880 ^ _39627) ^ [] : [-(relation(_51923))], (882 ^ _39627) ^ [] : [-(function(_51923))], (884 ^ _39627) ^ [] : [-(one_to_one(_51923))]], relation(_51923), empty(_51923), function(_51923)], (886 ^ _39627) ^ [_52136] : [-(ordinal(_52136)), epsilon_transitive(_52136), epsilon_connected(_52136)], (896 ^ _39627) ^ [_52255] : [empty(_52255), 899 ^ _39627 : [(900 ^ _39627) ^ [] : [-(epsilon_transitive(_52255))], (902 ^ _39627) ^ [] : [-(epsilon_connected(_52255))], (904 ^ _39627) ^ [] : [-(ordinal(_52255))]]], (906 ^ _39627) ^ [_52372, _52374] : [-(unordered_pair(_52374, _52372) = unordered_pair(_52372, _52374))], (908 ^ _39627) ^ [_52403, _52405] : [-(set_union2(_52405, _52403) = set_union2(_52403, _52405))], (910 ^ _39627) ^ [_52434, _52436] : [-(set_intersection2(_52436, _52434) = set_intersection2(_52434, _52436))], (912 ^ _39627) ^ [_52465, _52467] : [ordinal(_52467), ordinal(_52465), -(ordinal_subset(_52467, _52465)), -(ordinal_subset(_52465, _52467))], (926 ^ _39627) ^ [_52605, _52607] : [relation(_52605), 929 ^ _39627 : [(952 ^ _39627) ^ [] : [-(_52605 = identity_relation(_52607)), 965 ^ _39627 : [(966 ^ _39627) ^ [] : [-(in(953 ^ [_52605, _52607], _52607))], (968 ^ _39627) ^ [] : [-(953 ^ [_52605, _52607] = 954 ^ [_52605, _52607])], (970 ^ _39627) ^ [] : [in(ordered_pair(953 ^ [_52605, _52607], 954 ^ [_52605, _52607]), _52605)]], 957 ^ _39627 : [(958 ^ _39627) ^ [] : [-(in(ordered_pair(953 ^ [_52605, _52607], 954 ^ [_52605, _52607]), _52605))], (960 ^ _39627) ^ [] : [in(953 ^ [_52605, _52607], _52607), 953 ^ [_52605, _52607] = 954 ^ [_52605, _52607]]]], (930 ^ _39627) ^ [] : [_52605 = identity_relation(_52607), 933 ^ _39627 : [(934 ^ _39627) ^ [_52758, _52760] : [in(ordered_pair(_52760, _52758), _52605), 937 ^ _39627 : [(938 ^ _39627) ^ [] : [-(in(_52760, _52607))], (940 ^ _39627) ^ [] : [-(_52760 = _52758)]]], (942 ^ _39627) ^ [_52867, _52869] : [-(in(ordered_pair(_52869, _52867), _52605)), in(_52869, _52607), _52869 = _52867]]]]], (974 ^ _39627) ^ [_53394, _53396] : [_53396 = _53394, 977 ^ _39627 : [(978 ^ _39627) ^ [] : [-(subset(_53396, _53394))], (980 ^ _39627) ^ [] : [-(subset(_53394, _53396))]]], (982 ^ _39627) ^ [_53493, _53495] : [-(_53495 = _53493), subset(_53495, _53493), subset(_53493, _53495)], (992 ^ _39627) ^ [_53624] : [relation(_53624), 995 ^ _39627 : [(996 ^ _39627) ^ [_53724, _53726] : [relation(_53724), 999 ^ _39627 : [(1022 ^ _39627) ^ [] : [-(_53724 = relation_dom_restriction(_53624, _53726)), 1035 ^ _39627 : [(1036 ^ _39627) ^ [] : [-(in(1023 ^ [_53624, _53724, _53726], _53726))], (1038 ^ _39627) ^ [] : [-(in(ordered_pair(1023 ^ [_53624, _53724, _53726], 1024 ^ [_53624, _53724, _53726]), _53624))], (1040 ^ _39627) ^ [] : [in(ordered_pair(1023 ^ [_53624, _53724, _53726], 1024 ^ [_53624, _53724, _53726]), _53724)]], 1027 ^ _39627 : [(1028 ^ _39627) ^ [] : [-(in(ordered_pair(1023 ^ [_53624, _53724, _53726], 1024 ^ [_53624, _53724, _53726]), _53724))], (1030 ^ _39627) ^ [] : [in(1023 ^ [_53624, _53724, _53726], _53726), in(ordered_pair(1023 ^ [_53624, _53724, _53726], 1024 ^ [_53624, _53724, _53726]), _53624)]]], (1000 ^ _39627) ^ [] : [_53724 = relation_dom_restriction(_53624, _53726), 1003 ^ _39627 : [(1004 ^ _39627) ^ [_53886, _53888] : [in(ordered_pair(_53888, _53886), _53724), 1007 ^ _39627 : [(1008 ^ _39627) ^ [] : [-(in(_53888, _53726))], (1010 ^ _39627) ^ [] : [-(in(ordered_pair(_53888, _53886), _53624))]]], (1012 ^ _39627) ^ [_54003, _54005] : [-(in(ordered_pair(_54005, _54003), _53724)), in(_54005, _53726), in(ordered_pair(_54005, _54003), _53624)]]]]]]], (1044 ^ _39627) ^ [_54573] : [relation(_54573), function(_54573), 1051 ^ _39627 : [(1081 ^ _39627) ^ [_55251, _55253] : [-(_55251 = relation_image(_54573, _55253)), 1098 ^ _39627 : [(1099 ^ _39627) ^ [] : [-(in(1097 ^ [_54573, _55251, _55253], relation_dom(_54573)))], (1101 ^ _39627) ^ [] : [-(in(1097 ^ [_54573, _55251, _55253], _55253))], (1103 ^ _39627) ^ [] : [-(1082 ^ [_54573, _55251, _55253] = apply(_54573, 1097 ^ [_54573, _55251, _55253]))], (1105 ^ _39627) ^ [] : [in(1082 ^ [_54573, _55251, _55253], _55251)]], 1085 ^ _39627 : [(1086 ^ _39627) ^ [] : [-(in(1082 ^ [_54573, _55251, _55253], _55251))], (1088 ^ _39627) ^ [_55415] : [in(_55415, relation_dom(_54573)), in(_55415, _55253), 1082 ^ [_54573, _55251, _55253] = apply(_54573, _55415)]]], (1052 ^ _39627) ^ [_54736, _54738] : [_54736 = relation_image(_54573, _54738), 1055 ^ _39627 : [(1056 ^ _39627) ^ [_54841] : [in(_54841, _54736), 1060 ^ _39627 : [(1061 ^ _39627) ^ [] : [-(in(1059 ^ [_54573, _54736, _54738, _54841], relation_dom(_54573)))], (1063 ^ _39627) ^ [] : [-(in(1059 ^ [_54573, _54736, _54738, _54841], _54738))], (1065 ^ _39627) ^ [] : [-(_54841 = apply(_54573, 1059 ^ [_54573, _54736, _54738, _54841]))]]], (1067 ^ _39627) ^ [_55016] : [-(in(_55016, _54736)), 1068 ^ _39627 : [(1069 ^ _39627) ^ [_55071] : [in(_55071, relation_dom(_54573)), in(_55071, _54738), _55016 = apply(_54573, _55071)]]]]]]], (1109 ^ _39627) ^ [_55762, _55764] : [relation(_55762), 1112 ^ _39627 : [(1113 ^ _39627) ^ [_55859] : [relation(_55859), 1116 ^ _39627 : [(1139 ^ _39627) ^ [] : [-(_55859 = relation_rng_restriction(_55764, _55762)), 1152 ^ _39627 : [(1153 ^ _39627) ^ [] : [-(in(1141 ^ [_55762, _55764, _55859], _55764))], (1155 ^ _39627) ^ [] : [-(in(ordered_pair(1140 ^ [_55762, _55764, _55859], 1141 ^ [_55762, _55764, _55859]), _55762))], (1157 ^ _39627) ^ [] : [in(ordered_pair(1140 ^ [_55762, _55764, _55859], 1141 ^ [_55762, _55764, _55859]), _55859)]], 1144 ^ _39627 : [(1145 ^ _39627) ^ [] : [-(in(ordered_pair(1140 ^ [_55762, _55764, _55859], 1141 ^ [_55762, _55764, _55859]), _55859))], (1147 ^ _39627) ^ [] : [in(1141 ^ [_55762, _55764, _55859], _55764), in(ordered_pair(1140 ^ [_55762, _55764, _55859], 1141 ^ [_55762, _55764, _55859]), _55762)]]], (1117 ^ _39627) ^ [] : [_55859 = relation_rng_restriction(_55764, _55762), 1120 ^ _39627 : [(1121 ^ _39627) ^ [_56021, _56023] : [in(ordered_pair(_56023, _56021), _55859), 1124 ^ _39627 : [(1125 ^ _39627) ^ [] : [-(in(_56021, _55764))], (1127 ^ _39627) ^ [] : [-(in(ordered_pair(_56023, _56021), _55762))]]], (1129 ^ _39627) ^ [_56138, _56140] : [-(in(ordered_pair(_56140, _56138), _55859)), in(_56138, _55764), in(ordered_pair(_56140, _56138), _55762)]]]]]]], (1161 ^ _39627) ^ [_56699] : [relation(_56699), 1164 ^ _39627 : [(1165 ^ _39627) ^ [] : [antisymmetric(_56699), -(is_antisymmetric_in(_56699, relation_field(_56699)))], (1171 ^ _39627) ^ [] : [is_antisymmetric_in(_56699, relation_field(_56699)), -(antisymmetric(_56699))]]], (1177 ^ _39627) ^ [_56901] : [relation(_56901), function(_56901), 1184 ^ _39627 : [(1207 ^ _39627) ^ [_57409, _57411] : [-(_57409 = relation_inverse_image(_56901, _57411)), 1219 ^ _39627 : [(1220 ^ _39627) ^ [] : [-(in(1208 ^ [_56901, _57409, _57411], relation_dom(_56901)))], (1222 ^ _39627) ^ [] : [-(in(apply(_56901, 1208 ^ [_56901, _57409, _57411]), _57411))], (1224 ^ _39627) ^ [] : [in(1208 ^ [_56901, _57409, _57411], _57409)]], 1211 ^ _39627 : [(1212 ^ _39627) ^ [] : [-(in(1208 ^ [_56901, _57409, _57411], _57409))], (1214 ^ _39627) ^ [] : [in(1208 ^ [_56901, _57409, _57411], relation_dom(_56901)), in(apply(_56901, 1208 ^ [_56901, _57409, _57411]), _57411)]]], (1185 ^ _39627) ^ [_57053, _57055] : [_57053 = relation_inverse_image(_56901, _57055), 1188 ^ _39627 : [(1189 ^ _39627) ^ [_57147] : [in(_57147, _57053), 1192 ^ _39627 : [(1193 ^ _39627) ^ [] : [-(in(_57147, relation_dom(_56901)))], (1195 ^ _39627) ^ [] : [-(in(apply(_56901, _57147), _57055))]]], (1197 ^ _39627) ^ [_57260] : [-(in(_57260, _57053)), in(_57260, relation_dom(_56901)), in(apply(_56901, _57260), _57055)]]]]], (1228 ^ _39627) ^ [_57789] : [relation(_57789), 1231 ^ _39627 : [(1255 ^ _39627) ^ [_58294, _58296] : [-(_58294 = relation_image(_57789, _58296)), 1268 ^ _39627 : [(1269 ^ _39627) ^ [] : [-(in(ordered_pair(1267 ^ [_57789, _58294, _58296], 1256 ^ [_57789, _58294, _58296]), _57789))], (1271 ^ _39627) ^ [] : [-(in(1267 ^ [_57789, _58294, _58296], _58296))], (1273 ^ _39627) ^ [] : [in(1256 ^ [_57789, _58294, _58296], _58294)]], 1259 ^ _39627 : [(1260 ^ _39627) ^ [] : [-(in(1256 ^ [_57789, _58294, _58296], _58294))], (1262 ^ _39627) ^ [_58442] : [in(ordered_pair(_58442, 1256 ^ [_57789, _58294, _58296]), _57789), in(_58442, _58296)]]], (1232 ^ _39627) ^ [_57896, _57898] : [_57896 = relation_image(_57789, _57898), 1235 ^ _39627 : [(1236 ^ _39627) ^ [_57993] : [in(_57993, _57896), 1240 ^ _39627 : [(1241 ^ _39627) ^ [] : [-(in(ordered_pair(1239 ^ [_57789, _57896, _57898, _57993], _57993), _57789))], (1243 ^ _39627) ^ [] : [-(in(1239 ^ [_57789, _57896, _57898, _57993], _57898))]]], (1245 ^ _39627) ^ [_58129] : [-(in(_58129, _57896)), 1246 ^ _39627 : [(1247 ^ _39627) ^ [_58176] : [in(ordered_pair(_58176, _58129), _57789), in(_58176, _57898)]]]]]]], (1277 ^ _39627) ^ [_58696] : [relation(_58696), 1280 ^ _39627 : [(1304 ^ _39627) ^ [_59201, _59203] : [-(_59201 = relation_inverse_image(_58696, _59203)), 1317 ^ _39627 : [(1318 ^ _39627) ^ [] : [-(in(ordered_pair(1305 ^ [_58696, _59201, _59203], 1316 ^ [_58696, _59201, _59203]), _58696))], (1320 ^ _39627) ^ [] : [-(in(1316 ^ [_58696, _59201, _59203], _59203))], (1322 ^ _39627) ^ [] : [in(1305 ^ [_58696, _59201, _59203], _59201)]], 1308 ^ _39627 : [(1309 ^ _39627) ^ [] : [-(in(1305 ^ [_58696, _59201, _59203], _59201))], (1311 ^ _39627) ^ [_59349] : [in(ordered_pair(1305 ^ [_58696, _59201, _59203], _59349), _58696), in(_59349, _59203)]]], (1281 ^ _39627) ^ [_58803, _58805] : [_58803 = relation_inverse_image(_58696, _58805), 1284 ^ _39627 : [(1285 ^ _39627) ^ [_58900] : [in(_58900, _58803), 1289 ^ _39627 : [(1290 ^ _39627) ^ [] : [-(in(ordered_pair(_58900, 1288 ^ [_58696, _58803, _58805, _58900]), _58696))], (1292 ^ _39627) ^ [] : [-(in(1288 ^ [_58696, _58803, _58805, _58900], _58805))]]], (1294 ^ _39627) ^ [_59036] : [-(in(_59036, _58803)), 1295 ^ _39627 : [(1296 ^ _39627) ^ [_59083] : [in(ordered_pair(_59036, _59083), _58696), in(_59083, _58805)]]]]]]], (1326 ^ _39627) ^ [_59603] : [relation(_59603), 1329 ^ _39627 : [(1330 ^ _39627) ^ [] : [connected(_59603), -(is_connected_in(_59603, relation_field(_59603)))], (1336 ^ _39627) ^ [] : [is_connected_in(_59603, relation_field(_59603)), -(connected(_59603))]]], (1342 ^ _39627) ^ [_59805] : [relation(_59805), 1345 ^ _39627 : [(1346 ^ _39627) ^ [] : [transitive(_59805), -(is_transitive_in(_59805, relation_field(_59805)))], (1352 ^ _39627) ^ [] : [is_transitive_in(_59805, relation_field(_59805)), -(transitive(_59805))]]], (1386 ^ _39627) ^ [_60414, _60416, _60418, _60420] : [-(_60414 = unordered_triple(_60420, _60418, _60416)), 1390 ^ _39627 : [(1391 ^ _39627) ^ [] : [-(in(1387 ^ [_60414, _60416, _60418, _60420], _60414))], (1393 ^ _39627) ^ [] : [1387 ^ [_60414, _60416, _60418, _60420] = _60420], (1395 ^ _39627) ^ [] : [1387 ^ [_60414, _60416, _60418, _60420] = _60418], (1397 ^ _39627) ^ [] : [1387 ^ [_60414, _60416, _60418, _60420] = _60416]], 1398 ^ _39627 : [(1409 ^ _39627) ^ [] : [in(1387 ^ [_60414, _60416, _60418, _60420], _60414)], (1399 ^ _39627) ^ [] : [-(1387 ^ [_60414, _60416, _60418, _60420] = _60420), -(1387 ^ [_60414, _60416, _60418, _60420] = _60418), -(1387 ^ [_60414, _60416, _60418, _60420] = _60416)]]], (1358 ^ _39627) ^ [_60028, _60030, _60032, _60034] : [_60028 = unordered_triple(_60034, _60032, _60030), 1361 ^ _39627 : [(1376 ^ _39627) ^ [_60248] : [1377 ^ _39627 : [(1378 ^ _39627) ^ [] : [_60248 = _60034], (1380 ^ _39627) ^ [] : [_60248 = _60032], (1382 ^ _39627) ^ [] : [_60248 = _60030]], -(in(_60248, _60028))], (1362 ^ _39627) ^ [_60135] : [in(_60135, _60028), -(_60135 = _60034), -(_60135 = _60032), -(_60135 = _60030)]]], (1427 ^ _39627) ^ [_61084] : [1431 ^ _39627 : [(1432 ^ _39627) ^ [] : [-(in(ordered_pair(1428 ^ [_61084], 1429 ^ [_61084]), _61084))], (1434 ^ _39627) ^ [] : [-(in(ordered_pair(1428 ^ [_61084], 1430 ^ [_61084]), _61084))], (1436 ^ _39627) ^ [] : [1429 ^ [_61084] = 1430 ^ [_61084]]], -(function(_61084))], (1413 ^ _39627) ^ [_60854] : [function(_60854), 1416 ^ _39627 : [(1417 ^ _39627) ^ [_60935, _60937, _60939] : [-(_60937 = _60935), in(ordered_pair(_60939, _60937), _60854), in(ordered_pair(_60939, _60935), _60854)]]], (1440 ^ _39627) ^ [_61290, _61292, _61294] : [relation_of2_as_subset(_61290, _61294, _61292), 1443 ^ _39627 : [(1444 ^ _39627) ^ [] : [1445 ^ _39627 : [(1446 ^ _39627) ^ [] : [-(_61292 = empty_set)], (1448 ^ _39627) ^ [] : [_61294 = empty_set]], 1449 ^ _39627 : [(1450 ^ _39627) ^ [] : [quasi_total(_61290, _61294, _61292), -(_61294 = relation_dom_as_subset(_61294, _61292, _61290))], (1456 ^ _39627) ^ [] : [_61294 = relation_dom_as_subset(_61294, _61292, _61290), -(quasi_total(_61290, _61294, _61292))]]], (1462 ^ _39627) ^ [] : [_61292 = empty_set, -(_61294 = empty_set), 1469 ^ _39627 : [(1470 ^ _39627) ^ [] : [quasi_total(_61290, _61294, _61292), -(_61290 = empty_set)], (1476 ^ _39627) ^ [] : [_61290 = empty_set, -(quasi_total(_61290, _61294, _61292))]]]]], (1482 ^ _39627) ^ [_61885] : [1483 ^ _39627 : [(1484 ^ _39627) ^ [_61965, _61967] : [_61885 = ordered_pair(_61967, _61965)]], 1485 ^ _39627 : [(1496 ^ _39627) ^ [_62168] : [1499 ^ _39627 : [(1500 ^ _39627) ^ [] : [-(_61885 = ordered_pair(1497 ^ [_61885, _62168], 1498 ^ [_61885, _62168]))], (1502 ^ _39627) ^ [] : [_62168 = 1497 ^ [_61885, _62168]]], -(_62168 = pair_first(_61885))], (1486 ^ _39627) ^ [_62006] : [_62006 = pair_first(_61885), 1489 ^ _39627 : [(1490 ^ _39627) ^ [_62081, _62083] : [_61885 = ordered_pair(_62083, _62081), -(_62006 = _62083)]]]]], (1506 ^ _39627) ^ [_62339] : [-(succ(_62339) = set_union2(_62339, singleton(_62339)))], (1520 ^ _39627) ^ [_62566] : [1522 ^ _39627 : [(1523 ^ _39627) ^ [] : [-(in(1521 ^ [_62566], _62566))], (1525 ^ _39627) ^ [_62679, _62681] : [1521 ^ [_62566] = ordered_pair(_62681, _62679)]], -(relation(_62566))], (1508 ^ _39627) ^ [_62381] : [relation(_62381), 1511 ^ _39627 : [(1512 ^ _39627) ^ [_62457] : [in(_62457, _62381), -(_62457 = ordered_pair(1515 ^ [_62381, _62457], 1516 ^ [_62381, _62457]))]]], (1529 ^ _39627) ^ [_62743] : [relation(_62743), 1532 ^ _39627 : [(1543 ^ _39627) ^ [_62979] : [1545 ^ _39627 : [(1546 ^ _39627) ^ [] : [-(in(1544 ^ [_62743, _62979], _62979))], (1548 ^ _39627) ^ [] : [in(ordered_pair(1544 ^ [_62743, _62979], 1544 ^ [_62743, _62979]), _62743)]], -(is_reflexive_in(_62743, _62979))], (1533 ^ _39627) ^ [_62828] : [is_reflexive_in(_62743, _62828), 1536 ^ _39627 : [(1537 ^ _39627) ^ [_62894] : [in(_62894, _62828), -(in(ordered_pair(_62894, _62894), _62743))]]]]], (1552 ^ _39627) ^ [_63159, _63161, _63163] : [relation_of2(_63159, _63163, _63161), -(subset(_63159, cartesian_product2(_63163, _63161)))], (1558 ^ _39627) ^ [_63242, _63244, _63246] : [subset(_63242, cartesian_product2(_63246, _63244)), -(relation_of2(_63242, _63246, _63244))], (1613 ^ _39627) ^ [_64132, _64134] : [_64134 = empty_set, 1616 ^ _39627 : [(1617 ^ _39627) ^ [] : [_64132 = set_meet(_64134), -(_64132 = empty_set)], (1623 ^ _39627) ^ [] : [_64132 = empty_set, -(_64132 = set_meet(_64134))]]], (1564 ^ _39627) ^ [_63339, _63341] : [-(_63341 = empty_set), 1567 ^ _39627 : [(1591 ^ _39627) ^ [] : [-(_63339 = set_meet(_63341)), 1595 ^ _39627 : [(1596 ^ _39627) ^ [] : [-(in(1592 ^ [_63339, _63341], _63339))], (1599 ^ _39627) ^ [] : [-(in(1597 ^ [_63339, _63341], _63341))], (1601 ^ _39627) ^ [] : [in(1592 ^ [_63339, _63341], 1597 ^ [_63339, _63341])]], 1602 ^ _39627 : [(1609 ^ _39627) ^ [] : [in(1592 ^ [_63339, _63341], _63339)], (1603 ^ _39627) ^ [_63976] : [in(_63976, _63341), -(in(1592 ^ [_63339, _63341], _63976))]]], (1568 ^ _39627) ^ [] : [_63339 = set_meet(_63341), 1571 ^ _39627 : [(1582 ^ _39627) ^ [_63632] : [1584 ^ _39627 : [(1585 ^ _39627) ^ [] : [-(in(1583 ^ [_63339, _63341, _63632], _63341))], (1587 ^ _39627) ^ [] : [in(_63632, 1583 ^ [_63339, _63341, _63632])]], -(in(_63632, _63339))], (1572 ^ _39627) ^ [_63486] : [in(_63486, _63339), 1575 ^ _39627 : [(1576 ^ _39627) ^ [_63551] : [in(_63551, _63341), -(in(_63486, _63551))]]]]]]], (1645 ^ _39627) ^ [_64597, _64599] : [-(_64597 = singleton(_64599)), 1649 ^ _39627 : [(1650 ^ _39627) ^ [] : [-(in(1646 ^ [_64597, _64599], _64597))], (1652 ^ _39627) ^ [] : [1646 ^ [_64597, _64599] = _64599]], 1653 ^ _39627 : [(1654 ^ _39627) ^ [] : [-(1646 ^ [_64597, _64599] = _64599)], (1656 ^ _39627) ^ [] : [in(1646 ^ [_64597, _64599], _64597)]]], (1629 ^ _39627) ^ [_64362, _64364] : [_64362 = singleton(_64364), 1632 ^ _39627 : [(1633 ^ _39627) ^ [_64441] : [in(_64441, _64362), -(_64441 = _64364)], (1639 ^ _39627) ^ [_64516] : [_64516 = _64364, -(in(_64516, _64362))]]], (1660 ^ _39627) ^ [_64839] : [relation(_64839), 1663 ^ _39627 : [(1686 ^ _39627) ^ [_65304, _65306] : [-(_65304 = fiber(_64839, _65306)), 1698 ^ _39627 : [(1699 ^ _39627) ^ [] : [1687 ^ [_64839, _65304, _65306] = _65306], (1701 ^ _39627) ^ [] : [-(in(ordered_pair(1687 ^ [_64839, _65304, _65306], _65306), _64839))], (1703 ^ _39627) ^ [] : [in(1687 ^ [_64839, _65304, _65306], _65304)]], 1690 ^ _39627 : [(1691 ^ _39627) ^ [] : [-(in(1687 ^ [_64839, _65304, _65306], _65304))], (1693 ^ _39627) ^ [] : [-(1687 ^ [_64839, _65304, _65306] = _65306), in(ordered_pair(1687 ^ [_64839, _65304, _65306], _65306), _64839)]]], (1664 ^ _39627) ^ [_64943, _64945] : [_64943 = fiber(_64839, _64945), 1667 ^ _39627 : [(1668 ^ _39627) ^ [_65037] : [in(_65037, _64943), 1671 ^ _39627 : [(1672 ^ _39627) ^ [] : [_65037 = _64945], (1674 ^ _39627) ^ [] : [-(in(ordered_pair(_65037, _64945), _64839))]]], (1676 ^ _39627) ^ [_65156] : [-(in(_65156, _64943)), -(_65156 = _64945), in(ordered_pair(_65156, _64945), _64839)]]]]], (1707 ^ _39627) ^ [_65688, _65690] : [relation(_65688), 1710 ^ _39627 : [(1737 ^ _39627) ^ [] : [-(_65688 = inclusion_relation(_65690)), relation_field(_65688) = _65690, 1744 ^ _39627 : [(1745 ^ _39627) ^ [] : [-(in(1742 ^ [_65688, _65690], _65690))], (1747 ^ _39627) ^ [] : [-(in(1743 ^ [_65688, _65690], _65690))], (1749 ^ _39627) ^ [] : [1750 ^ _39627 : [(1751 ^ _39627) ^ [] : [-(in(ordered_pair(1742 ^ [_65688, _65690], 1743 ^ [_65688, _65690]), _65688))], (1753 ^ _39627) ^ [] : [subset(1742 ^ [_65688, _65690], 1743 ^ [_65688, _65690])]], 1754 ^ _39627 : [(1755 ^ _39627) ^ [] : [-(subset(1742 ^ [_65688, _65690], 1743 ^ [_65688, _65690]))], (1757 ^ _39627) ^ [] : [in(ordered_pair(1742 ^ [_65688, _65690], 1743 ^ [_65688, _65690]), _65688)]]]]], (1711 ^ _39627) ^ [] : [_65688 = inclusion_relation(_65690), 1714 ^ _39627 : [(1715 ^ _39627) ^ [] : [-(relation_field(_65688) = _65690)], (1717 ^ _39627) ^ [_65863, _65865] : [in(_65865, _65690), in(_65863, _65690), 1724 ^ _39627 : [(1725 ^ _39627) ^ [] : [in(ordered_pair(_65865, _65863), _65688), -(subset(_65865, _65863))], (1731 ^ _39627) ^ [] : [subset(_65865, _65863), -(in(ordered_pair(_65865, _65863), _65688))]]]]]]], (1761 ^ _39627) ^ [_66551] : [_66551 = empty_set, 1764 ^ _39627 : [(1765 ^ _39627) ^ [_66612] : [in(_66612, _66551)]]], (1767 ^ _39627) ^ [_66633] : [-(in(1768 ^ [_66633], _66633)), -(_66633 = empty_set)], (1790 ^ _39627) ^ [_66924, _66926] : [-(_66924 = powerset(_66926)), 1794 ^ _39627 : [(1795 ^ _39627) ^ [] : [-(in(1791 ^ [_66924, _66926], _66924))], (1797 ^ _39627) ^ [] : [subset(1791 ^ [_66924, _66926], _66926)]], 1798 ^ _39627 : [(1799 ^ _39627) ^ [] : [-(subset(1791 ^ [_66924, _66926], _66926))], (1801 ^ _39627) ^ [] : [in(1791 ^ [_66924, _66926], _66924)]]], (1774 ^ _39627) ^ [_66689, _66691] : [_66689 = powerset(_66691), 1777 ^ _39627 : [(1778 ^ _39627) ^ [_66768] : [in(_66768, _66689), -(subset(_66768, _66691))], (1784 ^ _39627) ^ [_66843] : [subset(_66843, _66691), -(in(_66843, _66689))]]], (1805 ^ _39627) ^ [_67166] : [1806 ^ _39627 : [(1807 ^ _39627) ^ [_67246, _67248] : [_67166 = ordered_pair(_67248, _67246)]], 1808 ^ _39627 : [(1819 ^ _39627) ^ [_67449] : [1822 ^ _39627 : [(1823 ^ _39627) ^ [] : [-(_67166 = ordered_pair(1820 ^ [_67166, _67449], 1821 ^ [_67166, _67449]))], (1825 ^ _39627) ^ [] : [_67449 = 1821 ^ [_67166, _67449]]], -(_67449 = pair_second(_67166))], (1809 ^ _39627) ^ [_67287] : [_67287 = pair_second(_67166), 1812 ^ _39627 : [(1813 ^ _39627) ^ [_67362, _67364] : [_67166 = ordered_pair(_67364, _67362), -(_67287 = _67362)]]]]], (1839 ^ _39627) ^ [_67768] : [1841 ^ _39627 : [(1842 ^ _39627) ^ [] : [-(in(1840 ^ [_67768], _67768))], (1844 ^ _39627) ^ [] : [subset(1840 ^ [_67768], _67768)]], -(epsilon_transitive(_67768))], (1829 ^ _39627) ^ [_67632] : [epsilon_transitive(_67632), 1832 ^ _39627 : [(1833 ^ _39627) ^ [_67691] : [in(_67691, _67632), -(subset(_67691, _67632))]]], (1848 ^ _39627) ^ [_67901] : [relation(_67901), 1851 ^ _39627 : [(1852 ^ _39627) ^ [_67987] : [relation(_67987), 1855 ^ _39627 : [(1872 ^ _39627) ^ [] : [-(_67901 = _67987), 1877 ^ _39627 : [(1878 ^ _39627) ^ [] : [-(in(ordered_pair(1873 ^ [_67901, _67987], 1874 ^ [_67901, _67987]), _67901))], (1880 ^ _39627) ^ [] : [in(ordered_pair(1873 ^ [_67901, _67987], 1874 ^ [_67901, _67987]), _67987)]], 1881 ^ _39627 : [(1882 ^ _39627) ^ [] : [-(in(ordered_pair(1873 ^ [_67901, _67987], 1874 ^ [_67901, _67987]), _67987))], (1884 ^ _39627) ^ [] : [in(ordered_pair(1873 ^ [_67901, _67987], 1874 ^ [_67901, _67987]), _67901)]]], (1856 ^ _39627) ^ [] : [_67901 = _67987, 1859 ^ _39627 : [(1860 ^ _39627) ^ [_68133, _68135] : [in(ordered_pair(_68135, _68133), _67901), -(in(ordered_pair(_68135, _68133), _67987))], (1866 ^ _39627) ^ [_68222, _68224] : [in(ordered_pair(_68224, _68222), _67987), -(in(ordered_pair(_68224, _68222), _67901))]]]]]]], (1888 ^ _39627) ^ [_68612, _68614] : [-(empty(_68614)), 1891 ^ _39627 : [(1892 ^ _39627) ^ [] : [element(_68612, _68614), -(in(_68612, _68614))], (1898 ^ _39627) ^ [] : [in(_68612, _68614), -(element(_68612, _68614))]]], (1904 ^ _39627) ^ [_68812, _68814] : [empty(_68814), 1907 ^ _39627 : [(1908 ^ _39627) ^ [] : [element(_68812, _68814), -(empty(_68812))], (1914 ^ _39627) ^ [] : [empty(_68812), -(element(_68812, _68814))]]], (1942 ^ _39627) ^ [_69334, _69336, _69338] : [-(_69334 = unordered_pair(_69338, _69336)), 1946 ^ _39627 : [(1947 ^ _39627) ^ [] : [-(in(1943 ^ [_69334, _69336, _69338], _69334))], (1949 ^ _39627) ^ [] : [1943 ^ [_69334, _69336, _69338] = _69338], (1951 ^ _39627) ^ [] : [1943 ^ [_69334, _69336, _69338] = _69336]], 1952 ^ _39627 : [(1959 ^ _39627) ^ [] : [in(1943 ^ [_69334, _69336, _69338], _69334)], (1953 ^ _39627) ^ [] : [-(1943 ^ [_69334, _69336, _69338] = _69338), -(1943 ^ [_69334, _69336, _69338] = _69336)]]], (1920 ^ _39627) ^ [_69034, _69036, _69038] : [_69034 = unordered_pair(_69038, _69036), 1923 ^ _39627 : [(1934 ^ _39627) ^ [_69213] : [1935 ^ _39627 : [(1936 ^ _39627) ^ [] : [_69213 = _69038], (1938 ^ _39627) ^ [] : [_69213 = _69036]], -(in(_69213, _69034))], (1924 ^ _39627) ^ [_69123] : [in(_69123, _69034), -(_69123 = _69038), -(_69123 = _69036)]]], (1963 ^ _39627) ^ [_69656] : [relation(_69656), 1966 ^ _39627 : [(1984 ^ _39627) ^ [] : [-(well_founded_relation(_69656)), 1986 ^ _39627 : [(1987 ^ _39627) ^ [] : [-(subset(1985 ^ [_69656], relation_field(_69656)))], (1989 ^ _39627) ^ [] : [1985 ^ [_69656] = empty_set], (1991 ^ _39627) ^ [_70077] : [in(_70077, 1985 ^ [_69656]), disjoint(fiber(_69656, _70077), 1985 ^ [_69656])]]], (1967 ^ _39627) ^ [] : [well_founded_relation(_69656), 1970 ^ _39627 : [(1971 ^ _39627) ^ [_69798] : [subset(_69798, relation_field(_69656)), -(_69798 = empty_set), 1979 ^ _39627 : [(1980 ^ _39627) ^ [] : [-(in(1978 ^ [_69656, _69798], _69798))], (1982 ^ _39627) ^ [] : [-(disjoint(fiber(_69656, 1978 ^ [_69656, _69798]), _69798))]]]]]]], (2021 ^ _39627) ^ [_70534, _70536, _70538] : [-(_70534 = set_union2(_70538, _70536)), 2025 ^ _39627 : [(2026 ^ _39627) ^ [] : [-(in(2022 ^ [_70534, _70536, _70538], _70534))], (2028 ^ _39627) ^ [] : [in(2022 ^ [_70534, _70536, _70538], _70538)], (2030 ^ _39627) ^ [] : [in(2022 ^ [_70534, _70536, _70538], _70536)]], 2031 ^ _39627 : [(2038 ^ _39627) ^ [] : [in(2022 ^ [_70534, _70536, _70538], _70534)], (2032 ^ _39627) ^ [] : [-(in(2022 ^ [_70534, _70536, _70538], _70538)), -(in(2022 ^ [_70534, _70536, _70538], _70536))]]], (1999 ^ _39627) ^ [_70234, _70236, _70238] : [_70234 = set_union2(_70238, _70236), 2002 ^ _39627 : [(2013 ^ _39627) ^ [_70413] : [2014 ^ _39627 : [(2015 ^ _39627) ^ [] : [in(_70413, _70238)], (2017 ^ _39627) ^ [] : [in(_70413, _70236)]], -(in(_70413, _70234))], (2003 ^ _39627) ^ [_70323] : [in(_70323, _70234), -(in(_70323, _70238)), -(in(_70323, _70236))]]], (2072 ^ _39627) ^ [_71407, _71409, _71411] : [-(_71407 = cartesian_product2(_71411, _71409)), 2090 ^ _39627 : [(2091 ^ _39627) ^ [] : [-(in(2088 ^ [_71407, _71409, _71411], _71411))], (2093 ^ _39627) ^ [] : [-(in(2089 ^ [_71407, _71409, _71411], _71409))], (2095 ^ _39627) ^ [] : [-(2073 ^ [_71407, _71409, _71411] = ordered_pair(2088 ^ [_71407, _71409, _71411], 2089 ^ [_71407, _71409, _71411]))], (2097 ^ _39627) ^ [] : [in(2073 ^ [_71407, _71409, _71411], _71407)]], 2076 ^ _39627 : [(2077 ^ _39627) ^ [] : [-(in(2073 ^ [_71407, _71409, _71411], _71407))], (2079 ^ _39627) ^ [_71577, _71579] : [in(_71579, _71411), in(_71577, _71409), 2073 ^ [_71407, _71409, _71411] = ordered_pair(_71579, _71577)]]], (2042 ^ _39627) ^ [_70874, _70876, _70878] : [_70874 = cartesian_product2(_70878, _70876), 2045 ^ _39627 : [(2046 ^ _39627) ^ [_70982] : [in(_70982, _70874), 2051 ^ _39627 : [(2052 ^ _39627) ^ [] : [-(in(2049 ^ [_70874, _70876, _70878, _70982], _70878))], (2054 ^ _39627) ^ [] : [-(in(2050 ^ [_70874, _70876, _70878, _70982], _70876))], (2056 ^ _39627) ^ [] : [-(_70982 = ordered_pair(2049 ^ [_70874, _70876, _70878, _70982], 2050 ^ [_70874, _70876, _70878, _70982]))]]], (2058 ^ _39627) ^ [_71169] : [-(in(_71169, _70874)), 2059 ^ _39627 : [(2060 ^ _39627) ^ [_71227, _71229] : [in(_71229, _70878), in(_71227, _70876), _71169 = ordered_pair(_71229, _71227)]]]]], (2123 ^ _39627) ^ [_72192] : [2126 ^ _39627 : [(2127 ^ _39627) ^ [] : [-(in(2124 ^ [_72192], _72192))], (2129 ^ _39627) ^ [] : [-(in(2125 ^ [_72192], _72192))], (2131 ^ _39627) ^ [] : [in(2124 ^ [_72192], 2125 ^ [_72192])], (2133 ^ _39627) ^ [] : [2124 ^ [_72192] = 2125 ^ [_72192]], (2135 ^ _39627) ^ [] : [in(2125 ^ [_72192], 2124 ^ [_72192])]], -(epsilon_connected(_72192))], (2101 ^ _39627) ^ [_71937] : [epsilon_connected(_71937), 2104 ^ _39627 : [(2105 ^ _39627) ^ [_72027, _72029] : [in(_72029, _71937), in(_72027, _71937), -(in(_72029, _72027)), -(_72029 = _72027), -(in(_72027, _72029))]]], (2139 ^ _39627) ^ [_72506] : [relation(_72506), 2142 ^ _39627 : [(2143 ^ _39627) ^ [_72592] : [relation(_72592), 2146 ^ _39627 : [(2157 ^ _39627) ^ [] : [2160 ^ _39627 : [(2161 ^ _39627) ^ [] : [-(in(ordered_pair(2158 ^ [_72506, _72592], 2159 ^ [_72506, _72592]), _72506))], (2163 ^ _39627) ^ [] : [in(ordered_pair(2158 ^ [_72506, _72592], 2159 ^ [_72506, _72592]), _72592)]], -(subset(_72506, _72592))], (2147 ^ _39627) ^ [] : [subset(_72506, _72592), 2150 ^ _39627 : [(2151 ^ _39627) ^ [_72723, _72725] : [in(ordered_pair(_72725, _72723), _72506), -(in(ordered_pair(_72725, _72723), _72592))]]]]]]], (2177 ^ _39627) ^ [_73136, _73138] : [2179 ^ _39627 : [(2180 ^ _39627) ^ [] : [-(in(2178 ^ [_73136, _73138], _73138))], (2182 ^ _39627) ^ [] : [in(2178 ^ [_73136, _73138], _73136)]], -(subset(_73138, _73136))], (2167 ^ _39627) ^ [_72994, _72996] : [subset(_72996, _72994), 2170 ^ _39627 : [(2171 ^ _39627) ^ [_73057] : [in(_73057, _72996), -(in(_73057, _72994))]]], (2186 ^ _39627) ^ [_73278] : [relation(_73278), 2189 ^ _39627 : [(2207 ^ _39627) ^ [_73643] : [-(is_well_founded_in(_73278, _73643)), 2209 ^ _39627 : [(2210 ^ _39627) ^ [] : [-(subset(2208 ^ [_73278, _73643], _73643))], (2212 ^ _39627) ^ [] : [2208 ^ [_73278, _73643] = empty_set], (2214 ^ _39627) ^ [_73806] : [in(_73806, 2208 ^ [_73278, _73643]), disjoint(fiber(_73278, _73806), 2208 ^ [_73278, _73643])]]], (2190 ^ _39627) ^ [_73386] : [is_well_founded_in(_73278, _73386), 2193 ^ _39627 : [(2194 ^ _39627) ^ [_73475] : [subset(_73475, _73386), -(_73475 = empty_set), 2202 ^ _39627 : [(2203 ^ _39627) ^ [] : [-(in(2201 ^ [_73278, _73386, _73475], _73475))], (2205 ^ _39627) ^ [] : [-(disjoint(fiber(_73278, 2201 ^ [_73278, _73386, _73475]), _73475))]]]]]]], (2244 ^ _39627) ^ [_74305, _74307, _74309] : [-(_74305 = set_intersection2(_74309, _74307)), 2256 ^ _39627 : [(2257 ^ _39627) ^ [] : [-(in(2245 ^ [_74305, _74307, _74309], _74309))], (2259 ^ _39627) ^ [] : [-(in(2245 ^ [_74305, _74307, _74309], _74307))], (2261 ^ _39627) ^ [] : [in(2245 ^ [_74305, _74307, _74309], _74305)]], 2248 ^ _39627 : [(2249 ^ _39627) ^ [] : [-(in(2245 ^ [_74305, _74307, _74309], _74305))], (2251 ^ _39627) ^ [] : [in(2245 ^ [_74305, _74307, _74309], _74309), in(2245 ^ [_74305, _74307, _74309], _74307)]]], (2222 ^ _39627) ^ [_73974, _73976, _73978] : [_73974 = set_intersection2(_73978, _73976), 2225 ^ _39627 : [(2226 ^ _39627) ^ [_74063] : [in(_74063, _73974), 2229 ^ _39627 : [(2230 ^ _39627) ^ [] : [-(in(_74063, _73978))], (2232 ^ _39627) ^ [] : [-(in(_74063, _73976))]]], (2234 ^ _39627) ^ [_74166] : [-(in(_74166, _73974)), in(_74166, _73978), in(_74166, _73976)]]], (2265 ^ _39627) ^ [_74659] : [relation(_74659), function(_74659), 2272 ^ _39627 : [(2273 ^ _39627) ^ [_74819, _74821] : [in(_74821, relation_dom(_74659)), 2276 ^ _39627 : [(2277 ^ _39627) ^ [] : [_74819 = apply(_74659, _74821), -(in(ordered_pair(_74821, _74819), _74659))], (2283 ^ _39627) ^ [] : [in(ordered_pair(_74821, _74819), _74659), -(_74819 = apply(_74659, _74821))]]], (2289 ^ _39627) ^ [_75049, _75051] : [-(in(_75051, relation_dom(_74659))), 2292 ^ _39627 : [(2293 ^ _39627) ^ [] : [_75049 = apply(_74659, _75051), -(_75049 = empty_set)], (2299 ^ _39627) ^ [] : [_75049 = empty_set, -(_75049 = apply(_74659, _75051))]]]]], (2305 ^ _39627) ^ [_75292] : [ordinal(_75292), 2308 ^ _39627 : [(2309 ^ _39627) ^ [] : [-(epsilon_transitive(_75292))], (2311 ^ _39627) ^ [] : [-(epsilon_connected(_75292))]]], (2313 ^ _39627) ^ [_75383] : [-(ordinal(_75383)), epsilon_transitive(_75383), epsilon_connected(_75383)], (2323 ^ _39627) ^ [_75504] : [relation(_75504), 2326 ^ _39627 : [(2344 ^ _39627) ^ [_75878] : [-(_75878 = relation_dom(_75504)), 2348 ^ _39627 : [(2349 ^ _39627) ^ [] : [-(in(2345 ^ [_75504, _75878], _75878))], (2351 ^ _39627) ^ [_76012] : [in(ordered_pair(2345 ^ [_75504, _75878], _76012), _75504)]], 2353 ^ _39627 : [(2354 ^ _39627) ^ [] : [-(in(ordered_pair(2345 ^ [_75504, _75878], 2352 ^ [_75504, _75878]), _75504))], (2356 ^ _39627) ^ [] : [in(2345 ^ [_75504, _75878], _75878)]]], (2327 ^ _39627) ^ [_75596] : [_75596 = relation_dom(_75504), 2330 ^ _39627 : [(2331 ^ _39627) ^ [_75683] : [in(_75683, _75596), -(in(ordered_pair(_75683, 2334 ^ [_75504, _75596, _75683]), _75504))], (2338 ^ _39627) ^ [_75778] : [2339 ^ _39627 : [(2340 ^ _39627) ^ [_75822] : [in(ordered_pair(_75778, _75822), _75504)]], -(in(_75778, _75596))]]]]], (2360 ^ _39627) ^ [_76159] : [relation(_76159), 2363 ^ _39627 : [(2386 ^ _39627) ^ [_76623] : [2389 ^ _39627 : [(2390 ^ _39627) ^ [] : [-(in(2387 ^ [_76159, _76623], _76623))], (2392 ^ _39627) ^ [] : [-(in(2388 ^ [_76159, _76623], _76623))], (2394 ^ _39627) ^ [] : [-(in(ordered_pair(2387 ^ [_76159, _76623], 2388 ^ [_76159, _76623]), _76159))], (2396 ^ _39627) ^ [] : [-(in(ordered_pair(2388 ^ [_76159, _76623], 2387 ^ [_76159, _76623]), _76159))], (2398 ^ _39627) ^ [] : [2387 ^ [_76159, _76623] = 2388 ^ [_76159, _76623]]], -(is_antisymmetric_in(_76159, _76623))], (2364 ^ _39627) ^ [_76270] : [is_antisymmetric_in(_76159, _76270), 2367 ^ _39627 : [(2368 ^ _39627) ^ [_76362, _76364] : [-(_76364 = _76362), in(_76364, _76270), in(_76362, _76270), in(ordered_pair(_76364, _76362), _76159), in(ordered_pair(_76362, _76364), _76159)]]]]], (2402 ^ _39627) ^ [_76915] : [-(cast_to_subset(_76915) = _76915)], (2427 ^ _39627) ^ [_77321, _77323] : [-(_77321 = union(_77323)), 2440 ^ _39627 : [(2441 ^ _39627) ^ [] : [-(in(2428 ^ [_77321, _77323], 2439 ^ [_77321, _77323]))], (2443 ^ _39627) ^ [] : [-(in(2439 ^ [_77321, _77323], _77323))], (2445 ^ _39627) ^ [] : [in(2428 ^ [_77321, _77323], _77321)]], 2431 ^ _39627 : [(2432 ^ _39627) ^ [] : [-(in(2428 ^ [_77321, _77323], _77321))], (2434 ^ _39627) ^ [_77454] : [in(2428 ^ [_77321, _77323], _77454), in(_77454, _77323)]]], (2404 ^ _39627) ^ [_76955, _76957] : [_76955 = union(_76957), 2407 ^ _39627 : [(2408 ^ _39627) ^ [_77045] : [in(_77045, _76955), 2412 ^ _39627 : [(2413 ^ _39627) ^ [] : [-(in(_77045, 2411 ^ [_76955, _76957, _77045]))], (2415 ^ _39627) ^ [] : [-(in(2411 ^ [_76955, _76957, _77045], _76957))]]], (2417 ^ _39627) ^ [_77169] : [-(in(_77169, _76955)), 2418 ^ _39627 : [(2419 ^ _39627) ^ [_77211] : [in(_77169, _77211), in(_77211, _76957)]]]]], (2449 ^ _39627) ^ [_77680] : [relation(_77680), 2452 ^ _39627 : [(2453 ^ _39627) ^ [] : [well_ordering(_77680), 2456 ^ _39627 : [(2457 ^ _39627) ^ [] : [-(reflexive(_77680))], (2459 ^ _39627) ^ [] : [-(transitive(_77680))], (2461 ^ _39627) ^ [] : [-(antisymmetric(_77680))], (2463 ^ _39627) ^ [] : [-(connected(_77680))], (2465 ^ _39627) ^ [] : [-(well_founded_relation(_77680))]]], (2467 ^ _39627) ^ [] : [-(well_ordering(_77680)), reflexive(_77680), transitive(_77680), antisymmetric(_77680), connected(_77680), well_founded_relation(_77680)]]], (2489 ^ _39627) ^ [_78150, _78152] : [equipotent(_78152, _78150), 2493 ^ _39627 : [(2494 ^ _39627) ^ [] : [-(relation(2492 ^ [_78150, _78152]))], (2496 ^ _39627) ^ [] : [-(function(2492 ^ [_78150, _78152]))], (2498 ^ _39627) ^ [] : [-(one_to_one(2492 ^ [_78150, _78152]))], (2500 ^ _39627) ^ [] : [-(relation_dom(2492 ^ [_78150, _78152]) = _78152)], (2502 ^ _39627) ^ [] : [-(relation_rng(2492 ^ [_78150, _78152]) = _78150)]]], (2504 ^ _39627) ^ [_78526, _78528] : [-(equipotent(_78528, _78526)), 2505 ^ _39627 : [(2506 ^ _39627) ^ [_78637] : [relation(_78637), function(_78637), one_to_one(_78637), relation_dom(_78637) = _78528, relation_rng(_78637) = _78526]]], (2548 ^ _39627) ^ [_79964, _79966, _79968] : [-(_79964 = set_difference(_79968, _79966)), 2560 ^ _39627 : [(2561 ^ _39627) ^ [] : [-(in(2549 ^ [_79964, _79966, _79968], _79968))], (2563 ^ _39627) ^ [] : [in(2549 ^ [_79964, _79966, _79968], _79966)], (2565 ^ _39627) ^ [] : [in(2549 ^ [_79964, _79966, _79968], _79964)]], 2552 ^ _39627 : [(2553 ^ _39627) ^ [] : [-(in(2549 ^ [_79964, _79966, _79968], _79964))], (2555 ^ _39627) ^ [] : [in(2549 ^ [_79964, _79966, _79968], _79968), -(in(2549 ^ [_79964, _79966, _79968], _79966))]]], (2526 ^ _39627) ^ [_79233, _79235, _79237] : [_79233 = set_difference(_79237, _79235), 2529 ^ _39627 : [(2530 ^ _39627) ^ [_79417] : [in(_79417, _79233), 2533 ^ _39627 : [(2534 ^ _39627) ^ [] : [-(in(_79417, _79237))], (2536 ^ _39627) ^ [] : [in(_79417, _79235)]]], (2538 ^ _39627) ^ [_79677] : [-(in(_79677, _79233)), in(_79677, _79237), -(in(_79677, _79235))]]], (2569 ^ _39627) ^ [_80707] : [relation(_80707), function(_80707), 2576 ^ _39627 : [(2600 ^ _39627) ^ [_81861] : [-(_81861 = relation_rng(_80707)), 2613 ^ _39627 : [(2614 ^ _39627) ^ [] : [-(in(2612 ^ [_80707, _81861], relation_dom(_80707)))], (2616 ^ _39627) ^ [] : [-(2601 ^ [_80707, _81861] = apply(_80707, 2612 ^ [_80707, _81861]))], (2618 ^ _39627) ^ [] : [in(2601 ^ [_80707, _81861], _81861)]], 2604 ^ _39627 : [(2605 ^ _39627) ^ [] : [-(in(2601 ^ [_80707, _81861], _81861))], (2607 ^ _39627) ^ [_82156] : [in(_82156, relation_dom(_80707)), 2601 ^ [_80707, _81861] = apply(_80707, _82156)]]], (2577 ^ _39627) ^ [_80979] : [_80979 = relation_rng(_80707), 2580 ^ _39627 : [(2581 ^ _39627) ^ [_81167] : [in(_81167, _80979), 2585 ^ _39627 : [(2586 ^ _39627) ^ [] : [-(in(2584 ^ [_80707, _80979, _81167], relation_dom(_80707)))], (2588 ^ _39627) ^ [] : [-(_81167 = apply(_80707, 2584 ^ [_80707, _80979, _81167]))]]], (2590 ^ _39627) ^ [_81509] : [-(in(_81509, _80979)), 2591 ^ _39627 : [(2592 ^ _39627) ^ [_81612] : [in(_81612, relation_dom(_80707)), _81509 = apply(_80707, _81612)]]]]]]], (2622 ^ _39627) ^ [_82733] : [relation(_82733), 2625 ^ _39627 : [(2643 ^ _39627) ^ [_83545] : [-(_83545 = relation_rng(_82733)), 2647 ^ _39627 : [(2648 ^ _39627) ^ [] : [-(in(2644 ^ [_82733, _83545], _83545))], (2650 ^ _39627) ^ [_83808] : [in(ordered_pair(_83808, 2644 ^ [_82733, _83545]), _82733)]], 2652 ^ _39627 : [(2653 ^ _39627) ^ [] : [-(in(ordered_pair(2651 ^ [_82733, _83545], 2644 ^ [_82733, _83545]), _82733))], (2655 ^ _39627) ^ [] : [in(2644 ^ [_82733, _83545], _83545)]]], (2626 ^ _39627) ^ [_82914] : [_82914 = relation_rng(_82733), 2629 ^ _39627 : [(2630 ^ _39627) ^ [_83094] : [in(_83094, _82914), -(in(ordered_pair(2633 ^ [_82733, _82914, _83094], _83094), _82733))], (2637 ^ _39627) ^ [_83338] : [2638 ^ _39627 : [(2639 ^ _39627) ^ [_83417] : [in(ordered_pair(_83417, _83338), _82733)]], -(in(_83338, _82914))]]]]], (2659 ^ _39627) ^ [_84188, _84190] : [element(_84188, powerset(_84190)), -(subset_complement(_84190, _84188) = set_difference(_84190, _84188))], (2665 ^ _39627) ^ [_84399, _84401] : [-(ordered_pair(_84401, _84399) = unordered_pair(unordered_pair(_84401, _84399), singleton(_84401)))], (2667 ^ _39627) ^ [_84505] : [relation(_84505), 2670 ^ _39627 : [(2671 ^ _39627) ^ [_84689] : [well_orders(_84505, _84689), 2674 ^ _39627 : [(2675 ^ _39627) ^ [] : [-(is_reflexive_in(_84505, _84689))], (2677 ^ _39627) ^ [] : [-(is_transitive_in(_84505, _84689))], (2679 ^ _39627) ^ [] : [-(is_antisymmetric_in(_84505, _84689))], (2681 ^ _39627) ^ [] : [-(is_connected_in(_84505, _84689))], (2683 ^ _39627) ^ [] : [-(is_well_founded_in(_84505, _84689))]]], (2685 ^ _39627) ^ [_85150] : [-(well_orders(_84505, _85150)), is_reflexive_in(_84505, _85150), is_transitive_in(_84505, _85150), is_antisymmetric_in(_84505, _85150), is_connected_in(_84505, _85150), is_well_founded_in(_84505, _85150)]]], (2707 ^ _39627) ^ [_85740] : [being_limit_ordinal(_85740), -(_85740 = union(_85740))], (2713 ^ _39627) ^ [_85898] : [_85898 = union(_85898), -(being_limit_ordinal(_85898))], (2719 ^ _39627) ^ [_86092] : [relation(_86092), -(relation_field(_86092) = set_union2(relation_dom(_86092), relation_rng(_86092)))], (2725 ^ _39627) ^ [_86298] : [relation(_86298), 2728 ^ _39627 : [(2751 ^ _39627) ^ [_87190] : [2754 ^ _39627 : [(2755 ^ _39627) ^ [] : [-(in(2752 ^ [_86298, _87190], _87190))], (2757 ^ _39627) ^ [] : [-(in(2753 ^ [_86298, _87190], _87190))], (2759 ^ _39627) ^ [] : [2752 ^ [_86298, _87190] = 2753 ^ [_86298, _87190]], (2761 ^ _39627) ^ [] : [in(ordered_pair(2752 ^ [_86298, _87190], 2753 ^ [_86298, _87190]), _86298)], (2763 ^ _39627) ^ [] : [in(ordered_pair(2753 ^ [_86298, _87190], 2752 ^ [_86298, _87190]), _86298)]], -(is_connected_in(_86298, _87190))], (2729 ^ _39627) ^ [_86506] : [is_connected_in(_86298, _86506), 2732 ^ _39627 : [(2733 ^ _39627) ^ [_86696, _86698] : [in(_86698, _86506), in(_86696, _86506), -(_86698 = _86696), -(in(ordered_pair(_86698, _86696), _86298)), -(in(ordered_pair(_86696, _86698), _86298))]]]]], (2767 ^ _39627) ^ [_87975] : [relation(_87975), 2770 ^ _39627 : [(2771 ^ _39627) ^ [_88094] : [-(relation_restriction(_87975, _88094) = set_intersection2(_87975, cartesian_product2(_88094, _88094)))]]], (2773 ^ _39627) ^ [_88203] : [relation(_88203), 2776 ^ _39627 : [(2777 ^ _39627) ^ [_88363] : [relation(_88363), 2780 ^ _39627 : [(2797 ^ _39627) ^ [] : [-(_88363 = relation_inverse(_88203)), 2802 ^ _39627 : [(2803 ^ _39627) ^ [] : [-(in(ordered_pair(2798 ^ [_88203, _88363], 2799 ^ [_88203, _88363]), _88363))], (2805 ^ _39627) ^ [] : [in(ordered_pair(2799 ^ [_88203, _88363], 2798 ^ [_88203, _88363]), _88203)]], 2806 ^ _39627 : [(2807 ^ _39627) ^ [] : [-(in(ordered_pair(2799 ^ [_88203, _88363], 2798 ^ [_88203, _88363]), _88203))], (2809 ^ _39627) ^ [] : [in(ordered_pair(2798 ^ [_88203, _88363], 2799 ^ [_88203, _88363]), _88363)]]], (2781 ^ _39627) ^ [] : [_88363 = relation_inverse(_88203), 2784 ^ _39627 : [(2785 ^ _39627) ^ [_88672, _88674] : [in(ordered_pair(_88674, _88672), _88363), -(in(ordered_pair(_88672, _88674), _88203))], (2791 ^ _39627) ^ [_88862, _88864] : [in(ordered_pair(_88862, _88864), _88203), -(in(ordered_pair(_88864, _88862), _88363))]]]]]]], (2813 ^ _39627) ^ [_89667] : [relation(_89667), 2816 ^ _39627 : [(2817 ^ _39627) ^ [_89888] : [relation(_89888), 2820 ^ _39627 : [(2821 ^ _39627) ^ [_90105] : [relation(_90105), function(_90105), 2828 ^ _39627 : [(2863 ^ _39627) ^ [] : [-(relation_isomorphism(_89667, _89888, _90105)), relation_dom(_90105) = relation_field(_89667), relation_rng(_90105) = relation_field(_89888), one_to_one(_90105), 2892 ^ _39627 : [(2893 ^ _39627) ^ [] : [-(in(2876 ^ [_89667, _89888, _90105], relation_field(_89667)))], (2895 ^ _39627) ^ [] : [-(in(2877 ^ [_89667, _89888, _90105], relation_field(_89667)))], (2897 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_90105, 2876 ^ [_89667, _89888, _90105]), apply(_90105, 2877 ^ [_89667, _89888, _90105])), _89888))], (2899 ^ _39627) ^ [] : [in(ordered_pair(2876 ^ [_89667, _89888, _90105], 2877 ^ [_89667, _89888, _90105]), _89667)]], 2880 ^ _39627 : [(2881 ^ _39627) ^ [] : [-(in(ordered_pair(2876 ^ [_89667, _89888, _90105], 2877 ^ [_89667, _89888, _90105]), _89667))], (2883 ^ _39627) ^ [] : [in(2876 ^ [_89667, _89888, _90105], relation_field(_89667)), in(2877 ^ [_89667, _89888, _90105], relation_field(_89667)), in(ordered_pair(apply(_90105, 2876 ^ [_89667, _89888, _90105]), apply(_90105, 2877 ^ [_89667, _89888, _90105])), _89888)]]], (2829 ^ _39627) ^ [] : [relation_isomorphism(_89667, _89888, _90105), 2832 ^ _39627 : [(2833 ^ _39627) ^ [] : [-(relation_dom(_90105) = relation_field(_89667))], (2835 ^ _39627) ^ [] : [-(relation_rng(_90105) = relation_field(_89888))], (2837 ^ _39627) ^ [] : [-(one_to_one(_90105))], (2839 ^ _39627) ^ [_90771, _90773] : [in(ordered_pair(_90773, _90771), _89667), 2842 ^ _39627 : [(2843 ^ _39627) ^ [] : [-(in(_90773, relation_field(_89667)))], (2845 ^ _39627) ^ [] : [-(in(_90771, relation_field(_89667)))], (2847 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_90105, _90773), apply(_90105, _90771)), _89888))]]], (2849 ^ _39627) ^ [_91150, _91152] : [-(in(ordered_pair(_91152, _91150), _89667)), in(_91152, relation_field(_89667)), in(_91150, relation_field(_89667)), in(ordered_pair(apply(_90105, _91152), apply(_90105, _91150)), _89888)]]]]]]]]], (2903 ^ _39627) ^ [_92977, _92979] : [disjoint(_92979, _92977), -(set_intersection2(_92979, _92977) = empty_set)], (2909 ^ _39627) ^ [_93145, _93147] : [set_intersection2(_93147, _93145) = empty_set, -(disjoint(_93147, _93145))], (2915 ^ _39627) ^ [_93349] : [relation(_93349), function(_93349), 2922 ^ _39627 : [(2941 ^ _39627) ^ [] : [2944 ^ _39627 : [(2945 ^ _39627) ^ [] : [-(in(2942 ^ [_93349], relation_dom(_93349)))], (2947 ^ _39627) ^ [] : [-(in(2943 ^ [_93349], relation_dom(_93349)))], (2949 ^ _39627) ^ [] : [-(apply(_93349, 2942 ^ [_93349]) = apply(_93349, 2943 ^ [_93349]))], (2951 ^ _39627) ^ [] : [2942 ^ [_93349] = 2943 ^ [_93349]]], -(one_to_one(_93349))], (2923 ^ _39627) ^ [] : [one_to_one(_93349), 2926 ^ _39627 : [(2927 ^ _39627) ^ [_93712, _93714] : [-(_93714 = _93712), in(_93714, relation_dom(_93349)), in(_93712, relation_dom(_93349)), apply(_93349, _93714) = apply(_93349, _93712)]]]]], (2955 ^ _39627) ^ [_94659] : [relation(_94659), 2958 ^ _39627 : [(2959 ^ _39627) ^ [_94844] : [relation(_94844), 2962 ^ _39627 : [(2963 ^ _39627) ^ [_95025] : [relation(_95025), 2966 ^ _39627 : [(2990 ^ _39627) ^ [] : [-(_95025 = relation_composition(_94659, _94844)), 3004 ^ _39627 : [(3005 ^ _39627) ^ [] : [-(in(ordered_pair(2991 ^ [_94659, _94844, _95025], 3003 ^ [_94659, _94844, _95025]), _94659))], (3007 ^ _39627) ^ [] : [-(in(ordered_pair(3003 ^ [_94659, _94844, _95025], 2992 ^ [_94659, _94844, _95025]), _94844))], (3009 ^ _39627) ^ [] : [in(ordered_pair(2991 ^ [_94659, _94844, _95025], 2992 ^ [_94659, _94844, _95025]), _95025)]], 2995 ^ _39627 : [(2996 ^ _39627) ^ [] : [-(in(ordered_pair(2991 ^ [_94659, _94844, _95025], 2992 ^ [_94659, _94844, _95025]), _95025))], (2998 ^ _39627) ^ [_96489] : [in(ordered_pair(2991 ^ [_94659, _94844, _95025], _96489), _94659), in(ordered_pair(_96489, 2992 ^ [_94659, _94844, _95025]), _94844)]]], (2967 ^ _39627) ^ [] : [_95025 = relation_composition(_94659, _94844), 2970 ^ _39627 : [(2971 ^ _39627) ^ [_95360, _95362] : [in(ordered_pair(_95362, _95360), _95025), 2975 ^ _39627 : [(2976 ^ _39627) ^ [] : [-(in(ordered_pair(_95362, 2974 ^ [_94659, _94844, _95025, _95360, _95362]), _94659))], (2978 ^ _39627) ^ [] : [-(in(ordered_pair(2974 ^ [_94659, _94844, _95025, _95360, _95362], _95360), _94844))]]], (2980 ^ _39627) ^ [_95745, _95747] : [-(in(ordered_pair(_95747, _95745), _95025)), 2981 ^ _39627 : [(2982 ^ _39627) ^ [_95858] : [in(ordered_pair(_95747, _95858), _94659), in(ordered_pair(_95858, _95745), _94844)]]]]]]]]]]], (3013 ^ _39627) ^ [_97161] : [relation(_97161), 3016 ^ _39627 : [(3043 ^ _39627) ^ [_98196] : [3047 ^ _39627 : [(3048 ^ _39627) ^ [] : [-(in(3044 ^ [_97161, _98196], _98196))], (3050 ^ _39627) ^ [] : [-(in(3045 ^ [_97161, _98196], _98196))], (3052 ^ _39627) ^ [] : [-(in(3046 ^ [_97161, _98196], _98196))], (3054 ^ _39627) ^ [] : [-(in(ordered_pair(3044 ^ [_97161, _98196], 3045 ^ [_97161, _98196]), _97161))], (3056 ^ _39627) ^ [] : [-(in(ordered_pair(3045 ^ [_97161, _98196], 3046 ^ [_97161, _98196]), _97161))], (3058 ^ _39627) ^ [] : [in(ordered_pair(3044 ^ [_97161, _98196], 3046 ^ [_97161, _98196]), _97161)]], -(is_transitive_in(_97161, _98196))], (3017 ^ _39627) ^ [_97375] : [is_transitive_in(_97161, _97375), 3020 ^ _39627 : [(3021 ^ _39627) ^ [_97585, _97587, _97589] : [-(in(ordered_pair(_97589, _97585), _97161)), in(_97589, _97375), in(_97587, _97375), in(_97585, _97375), in(ordered_pair(_97589, _97587), _97161), in(ordered_pair(_97587, _97585), _97161)]]]]], (3062 ^ _39627) ^ [_99220, _99222] : [element(_99220, powerset(powerset(_99222))), 3065 ^ _39627 : [(3066 ^ _39627) ^ [_99400] : [element(_99400, powerset(powerset(_99222))), 3069 ^ _39627 : [(3090 ^ _39627) ^ [] : [-(_99400 = complements_of_subsets(_99222, _99220)), 3092 ^ _39627 : [(3093 ^ _39627) ^ [] : [-(element(3091 ^ [_99220, _99222, _99400], powerset(_99222)))], (3095 ^ _39627) ^ [] : [3096 ^ _39627 : [(3097 ^ _39627) ^ [] : [-(in(3091 ^ [_99220, _99222, _99400], _99400))], (3099 ^ _39627) ^ [] : [in(subset_complement(_99222, 3091 ^ [_99220, _99222, _99400]), _99220)]], 3100 ^ _39627 : [(3101 ^ _39627) ^ [] : [-(in(subset_complement(_99222, 3091 ^ [_99220, _99222, _99400]), _99220))], (3103 ^ _39627) ^ [] : [in(3091 ^ [_99220, _99222, _99400], _99400)]]]]], (3070 ^ _39627) ^ [] : [_99400 = complements_of_subsets(_99222, _99220), 3073 ^ _39627 : [(3074 ^ _39627) ^ [_99688] : [element(_99688, powerset(_99222)), 3077 ^ _39627 : [(3078 ^ _39627) ^ [] : [in(_99688, _99400), -(in(subset_complement(_99222, _99688), _99220))], (3084 ^ _39627) ^ [] : [in(subset_complement(_99222, _99688), _99220), -(in(_99688, _99400))]]]]]]]]], (3107 ^ _39627) ^ [_100811, _100813] : [proper_subset(_100813, _100811), 3110 ^ _39627 : [(3111 ^ _39627) ^ [] : [-(subset(_100813, _100811))], (3113 ^ _39627) ^ [] : [_100813 = _100811]]], (3115 ^ _39627) ^ [_101049, _101051] : [-(proper_subset(_101051, _101049)), subset(_101051, _101049), -(_101051 = _101049)], (3125 ^ _39627) ^ [_101339] : [relation(_101339), function(_101339), one_to_one(_101339), -(function_inverse(_101339) = relation_inverse(_101339))], (3139 ^ _39627) ^ [_101703] : [relation(_101703), 3142 ^ _39627 : [(3143 ^ _39627) ^ [] : [reflexive(_101703), -(is_reflexive_in(_101703, relation_field(_101703)))], (3149 ^ _39627) ^ [] : [is_reflexive_in(_101703, relation_field(_101703)), -(reflexive(_101703))]]], (3155 ^ _39627) ^ [] : [true___, -(true___)], (3161 ^ _39627) ^ [] : [true___, -(true___)], (3167 ^ _39627) ^ [] : [true___, -(true___)], (3173 ^ _39627) ^ [] : [true___, -(true___)], (3179 ^ _39627) ^ [] : [true___, -(true___)], (3185 ^ _39627) ^ [] : [true___, -(true___)], (3191 ^ _39627) ^ [] : [true___, -(true___)], (3197 ^ _39627) ^ [] : [true___, -(true___)], (3203 ^ _39627) ^ [] : [true___, -(true___)], (3209 ^ _39627) ^ [_103190] : [-(relation(inclusion_relation(_103190)))], (3211 ^ _39627) ^ [] : [true___, -(true___)], (3217 ^ _39627) ^ [] : [true___, -(true___)], (3223 ^ _39627) ^ [_103522] : [3230 ^ _39627 : [(3231 ^ _39627) ^ [] : [-(relation(function_inverse(_103522)))], (3233 ^ _39627) ^ [] : [-(function(function_inverse(_103522)))]], relation(_103522), function(_103522)], (3235 ^ _39627) ^ [] : [true___, -(true___)], (3241 ^ _39627) ^ [] : [true___, -(true___)], (3247 ^ _39627) ^ [_104093] : [-(element(cast_to_subset(_104093), powerset(_104093)))], (3249 ^ _39627) ^ [] : [true___, -(true___)], (3255 ^ _39627) ^ [_104323, _104325] : [relation(_104325), -(relation(relation_restriction(_104325, _104323)))], (3261 ^ _39627) ^ [] : [true___, -(true___)], (3267 ^ _39627) ^ [] : [true___, -(true___)], (3273 ^ _39627) ^ [] : [true___, -(true___)], (3279 ^ _39627) ^ [_104892, _104894] : [element(_104892, powerset(_104894)), -(element(subset_complement(_104894, _104892), powerset(_104894)))], (3285 ^ _39627) ^ [] : [true___, -(true___)], (3291 ^ _39627) ^ [] : [true___, -(true___)], (3297 ^ _39627) ^ [_105340] : [relation(_105340), -(relation(relation_inverse(_105340)))], (3303 ^ _39627) ^ [_105558, _105560, _105562] : [relation_of2(_105558, _105562, _105560), -(element(relation_dom_as_subset(_105562, _105560, _105558), powerset(_105562)))], (3309 ^ _39627) ^ [] : [true___, -(true___)], (3315 ^ _39627) ^ [] : [true___, -(true___)], (3321 ^ _39627) ^ [_106026, _106028] : [-(relation(relation_composition(_106028, _106026))), relation(_106028), relation(_106026)], (3331 ^ _39627) ^ [_106339, _106341, _106343] : [relation_of2(_106339, _106343, _106341), -(element(relation_rng_as_subset(_106343, _106341, _106339), powerset(_106341)))], (3337 ^ _39627) ^ [_106569, _106571] : [element(_106569, powerset(powerset(_106571))), -(element(union_of_subsets(_106571, _106569), powerset(_106571)))], (3343 ^ _39627) ^ [_106768] : [-(relation(identity_relation(_106768)))], (3345 ^ _39627) ^ [_106876, _106878] : [element(_106876, powerset(powerset(_106878))), -(element(meet_of_subsets(_106878, _106876), powerset(_106878)))], (3351 ^ _39627) ^ [_107118, _107120, _107122] : [-(element(subset_difference(_107122, _107120, _107118), powerset(_107122))), element(_107120, powerset(_107122)), element(_107118, powerset(_107122))], (3361 ^ _39627) ^ [_107447, _107449] : [relation(_107449), -(relation(relation_dom_restriction(_107449, _107447)))], (3367 ^ _39627) ^ [_107659, _107661] : [element(_107659, powerset(powerset(_107661))), -(element(complements_of_subsets(_107661, _107659), powerset(powerset(_107661))))], (3373 ^ _39627) ^ [_107891, _107893] : [relation(_107891), -(relation(relation_rng_restriction(_107893, _107891)))], (3379 ^ _39627) ^ [] : [true___, -(true___)], (3385 ^ _39627) ^ [] : [true___, -(true___)], (3391 ^ _39627) ^ [] : [true___, -(true___)], (3397 ^ _39627) ^ [_108474, _108476, _108478] : [relation_of2_as_subset(_108474, _108478, _108476), -(element(_108474, powerset(cartesian_product2(_108478, _108476))))], (3404 ^ _39627) ^ [_108729, _108731] : [-(relation_of2(3402 ^ [_108729, _108731], _108731, _108729))], (3407 ^ _39627) ^ [_108856] : [-(element(3405 ^ [_108856], _108856))], (3410 ^ _39627) ^ [_108995, _108997] : [-(relation_of2_as_subset(3408 ^ [_108995, _108997], _108997, _108995))], (3412 ^ _39627) ^ [_109112, _109114] : [3419 ^ _39627 : [(3420 ^ _39627) ^ [] : [-(empty(relation_composition(_109112, _109114)))], (3422 ^ _39627) ^ [] : [-(relation(relation_composition(_109112, _109114)))]], empty(_109114), relation(_109112)], (3424 ^ _39627) ^ [_109476] : [empty(_109476), 3427 ^ _39627 : [(3428 ^ _39627) ^ [] : [-(empty(relation_inverse(_109476)))], (3430 ^ _39627) ^ [] : [-(relation(relation_inverse(_109476)))]]], (3432 ^ _39627) ^ [] : [-(empty(empty_set))], (3434 ^ _39627) ^ [] : [-(relation(empty_set))], (3436 ^ _39627) ^ [] : [-(relation_empty_yielding(empty_set))], (3438 ^ _39627) ^ [_109918, _109920] : [3445 ^ _39627 : [(3446 ^ _39627) ^ [] : [-(relation(relation_dom_restriction(_109920, _109918)))], (3448 ^ _39627) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_109920, _109918)))]], relation(_109920), relation_empty_yielding(_109920)], (3450 ^ _39627) ^ [_110296, _110298] : [3465 ^ _39627 : [(3466 ^ _39627) ^ [] : [-(relation(relation_composition(_110298, _110296)))], (3468 ^ _39627) ^ [] : [-(function(relation_composition(_110298, _110296)))]], relation(_110298), function(_110298), relation(_110296), function(_110296)], (3470 ^ _39627) ^ [_110818] : [empty(succ(_110818))], (3472 ^ _39627) ^ [_110926, _110928] : [-(relation(set_intersection2(_110928, _110926))), relation(_110928), relation(_110926)], (3482 ^ _39627) ^ [_111195] : [empty(powerset(_111195))], (3484 ^ _39627) ^ [] : [-(empty(empty_set))], (3486 ^ _39627) ^ [_111340, _111342] : [empty(ordered_pair(_111342, _111340))], (3488 ^ _39627) ^ [_111442] : [-(relation(identity_relation(_111442)))], (3490 ^ _39627) ^ [_111487] : [-(function(identity_relation(_111487)))], (3492 ^ _39627) ^ [] : [-(relation(empty_set))], (3494 ^ _39627) ^ [] : [-(relation_empty_yielding(empty_set))], (3496 ^ _39627) ^ [] : [-(function(empty_set))], (3498 ^ _39627) ^ [] : [-(one_to_one(empty_set))], (3500 ^ _39627) ^ [] : [-(empty(empty_set))], (3502 ^ _39627) ^ [] : [-(epsilon_transitive(empty_set))], (3504 ^ _39627) ^ [] : [-(epsilon_connected(empty_set))], (3506 ^ _39627) ^ [] : [-(ordinal(empty_set))], (3508 ^ _39627) ^ [_112035, _112037] : [-(relation(set_union2(_112037, _112035))), relation(_112037), relation(_112035)], (3518 ^ _39627) ^ [_112304] : [empty(singleton(_112304))], (3520 ^ _39627) ^ [_112412, _112414] : [-(empty(_112414)), empty(set_union2(_112414, _112412))], (3526 ^ _39627) ^ [_112614] : [3537 ^ _39627 : [(3538 ^ _39627) ^ [] : [-(relation(relation_inverse(_112614)))], (3540 ^ _39627) ^ [] : [-(function(relation_inverse(_112614)))]], relation(_112614), function(_112614), one_to_one(_112614)], (3542 ^ _39627) ^ [_113045] : [ordinal(_113045), 3545 ^ _39627 : [(3546 ^ _39627) ^ [] : [empty(succ(_113045))], (3548 ^ _39627) ^ [] : [-(epsilon_transitive(succ(_113045)))], (3550 ^ _39627) ^ [] : [-(epsilon_connected(succ(_113045)))], (3552 ^ _39627) ^ [] : [-(ordinal(succ(_113045)))]]], (3554 ^ _39627) ^ [_113473, _113475] : [-(relation(set_difference(_113475, _113473))), relation(_113475), relation(_113473)], (3564 ^ _39627) ^ [_113756, _113758] : [empty(unordered_pair(_113758, _113756))], (3566 ^ _39627) ^ [_113867, _113869] : [-(empty(_113869)), empty(set_union2(_113867, _113869))], (3572 ^ _39627) ^ [_114083, _114085] : [3579 ^ _39627 : [(3580 ^ _39627) ^ [] : [-(relation(relation_dom_restriction(_114085, _114083)))], (3582 ^ _39627) ^ [] : [-(function(relation_dom_restriction(_114085, _114083)))]], relation(_114085), function(_114085)], (3584 ^ _39627) ^ [_114447] : [ordinal(_114447), 3587 ^ _39627 : [(3588 ^ _39627) ^ [] : [-(epsilon_transitive(union(_114447)))], (3590 ^ _39627) ^ [] : [-(epsilon_connected(union(_114447)))], (3592 ^ _39627) ^ [] : [-(ordinal(union(_114447)))]]], (3594 ^ _39627) ^ [] : [-(empty(empty_set))], (3596 ^ _39627) ^ [] : [-(relation(empty_set))], (3598 ^ _39627) ^ [_114908, _114910] : [empty(cartesian_product2(_114910, _114908)), -(empty(_114910)), -(empty(_114908))], (3608 ^ _39627) ^ [_115214, _115216] : [3615 ^ _39627 : [(3616 ^ _39627) ^ [] : [-(relation(relation_rng_restriction(_115216, _115214)))], (3618 ^ _39627) ^ [] : [-(function(relation_rng_restriction(_115216, _115214)))]], relation(_115214), function(_115214)], (3620 ^ _39627) ^ [_115578] : [empty(relation_dom(_115578)), -(empty(_115578)), relation(_115578)], (3630 ^ _39627) ^ [_115855] : [empty(relation_rng(_115855)), -(empty(_115855)), relation(_115855)], (3640 ^ _39627) ^ [_116132] : [empty(_116132), 3643 ^ _39627 : [(3644 ^ _39627) ^ [] : [-(empty(relation_dom(_116132)))], (3646 ^ _39627) ^ [] : [-(relation(relation_dom(_116132)))]]], (3648 ^ _39627) ^ [_116397] : [empty(_116397), 3651 ^ _39627 : [(3652 ^ _39627) ^ [] : [-(empty(relation_rng(_116397)))], (3654 ^ _39627) ^ [] : [-(relation(relation_rng(_116397)))]]], (3656 ^ _39627) ^ [_116676, _116678] : [3663 ^ _39627 : [(3664 ^ _39627) ^ [] : [-(empty(relation_composition(_116678, _116676)))], (3666 ^ _39627) ^ [] : [-(relation(relation_composition(_116678, _116676)))]], empty(_116678), relation(_116676)], (3668 ^ _39627) ^ [_117039, _117041] : [-(set_union2(_117041, _117041) = _117041)], (3670 ^ _39627) ^ [_117136, _117138] : [-(set_intersection2(_117138, _117138) = _117138)], (3672 ^ _39627) ^ [_117248, _117250] : [element(_117248, powerset(_117250)), -(subset_complement(_117250, subset_complement(_117250, _117248)) = _117248)], (3678 ^ _39627) ^ [_117460] : [relation(_117460), -(relation_inverse(relation_inverse(_117460)) = _117460)], (3684 ^ _39627) ^ [_117670, _117672] : [element(_117670, powerset(powerset(_117672))), -(complements_of_subsets(_117672, complements_of_subsets(_117672, _117670)) = _117670)], (3690 ^ _39627) ^ [_117884, _117886] : [proper_subset(_117886, _117886)], (3692 ^ _39627) ^ [_117979] : [relation(_117979), 3695 ^ _39627 : [(3706 ^ _39627) ^ [] : [3708 ^ _39627 : [(3709 ^ _39627) ^ [] : [-(in(3707 ^ [_117979], relation_field(_117979)))], (3711 ^ _39627) ^ [] : [in(ordered_pair(3707 ^ [_117979], 3707 ^ [_117979]), _117979)]], -(reflexive(_117979))], (3696 ^ _39627) ^ [] : [reflexive(_117979), 3699 ^ _39627 : [(3700 ^ _39627) ^ [_118223] : [in(_118223, relation_field(_117979)), -(in(ordered_pair(_118223, _118223), _117979))]]]]], (3715 ^ _39627) ^ [_118688] : [singleton(_118688) = empty_set], (3717 ^ _39627) ^ [_118797, _118799] : [in(_118799, _118797), -(set_union2(singleton(_118799), _118797) = _118797)], (3723 ^ _39627) ^ [_119017, _119019] : [disjoint(singleton(_119019), _119017), in(_119019, _119017)], (3729 ^ _39627) ^ [_119230, _119232] : [-(in(_119232, _119230)), -(disjoint(singleton(_119232), _119230))], (3735 ^ _39627) ^ [_119447, _119449] : [relation(_119447), -(subset(relation_dom(relation_rng_restriction(_119449, _119447)), relation_dom(_119447)))], (3741 ^ _39627) ^ [_119655] : [relation(_119655), 3744 ^ _39627 : [(3759 ^ _39627) ^ [] : [3763 ^ _39627 : [(3764 ^ _39627) ^ [] : [-(in(ordered_pair(3760 ^ [_119655], 3761 ^ [_119655]), _119655))], (3766 ^ _39627) ^ [] : [-(in(ordered_pair(3761 ^ [_119655], 3762 ^ [_119655]), _119655))], (3768 ^ _39627) ^ [] : [in(ordered_pair(3760 ^ [_119655], 3762 ^ [_119655]), _119655)]], -(transitive(_119655))], (3745 ^ _39627) ^ [] : [transitive(_119655), 3748 ^ _39627 : [(3749 ^ _39627) ^ [_119947, _119949, _119951] : [-(in(ordered_pair(_119951, _119947), _119655)), in(ordered_pair(_119951, _119949), _119655), in(ordered_pair(_119949, _119947), _119655)]]]]], (3772 ^ _39627) ^ [_120854, _120856] : [subset(singleton(_120856), _120854), -(in(_120856, _120854))], (3778 ^ _39627) ^ [_121020, _121022] : [in(_121022, _121020), -(subset(singleton(_121022), _121020))], (3784 ^ _39627) ^ [_121236, _121238] : [relation(_121236), well_ordering(_121236), equipotent(_121238, relation_field(_121236)), 3796 ^ _39627 : [(3797 ^ _39627) ^ [] : [-(relation(3795 ^ [_121236, _121238]))], (3799 ^ _39627) ^ [] : [-(well_orders(3795 ^ [_121236, _121238], _121238))]]], (3801 ^ _39627) ^ [_121801, _121803] : [set_difference(_121803, _121801) = empty_set, -(subset(_121803, _121801))], (3807 ^ _39627) ^ [_121969, _121971] : [subset(_121971, _121969), -(set_difference(_121971, _121969) = empty_set)], (3813 ^ _39627) ^ [_122187, _122189] : [element(_122187, powerset(_122189)), 3816 ^ _39627 : [(3817 ^ _39627) ^ [_122328] : [in(_122328, _122187), -(in(_122328, _122189))]]], (3823 ^ _39627) ^ [_122539] : [relation(_122539), 3826 ^ _39627 : [(3841 ^ _39627) ^ [] : [3844 ^ _39627 : [(3845 ^ _39627) ^ [] : [-(in(ordered_pair(3842 ^ [_122539], 3843 ^ [_122539]), _122539))], (3847 ^ _39627) ^ [] : [-(in(ordered_pair(3843 ^ [_122539], 3842 ^ [_122539]), _122539))], (3849 ^ _39627) ^ [] : [3842 ^ [_122539] = 3843 ^ [_122539]]], -(antisymmetric(_122539))], (3827 ^ _39627) ^ [] : [antisymmetric(_122539), 3830 ^ _39627 : [(3831 ^ _39627) ^ [_122809, _122811] : [-(_122811 = _122809), in(ordered_pair(_122811, _122809), _122539), in(ordered_pair(_122809, _122811), _122539)]]]]], (3853 ^ _39627) ^ [_123589, _123591, _123593] : [subset(_123593, _123591), -(in(_123589, _123593)), -(subset(_123593, set_difference(_123591, singleton(_123589))))], (3863 ^ _39627) ^ [_123895] : [relation(_123895), 3866 ^ _39627 : [(3889 ^ _39627) ^ [] : [3892 ^ _39627 : [(3893 ^ _39627) ^ [] : [-(in(3890 ^ [_123895], relation_field(_123895)))], (3895 ^ _39627) ^ [] : [-(in(3891 ^ [_123895], relation_field(_123895)))], (3897 ^ _39627) ^ [] : [3890 ^ [_123895] = 3891 ^ [_123895]], (3899 ^ _39627) ^ [] : [in(ordered_pair(3890 ^ [_123895], 3891 ^ [_123895]), _123895)], (3901 ^ _39627) ^ [] : [in(ordered_pair(3891 ^ [_123895], 3890 ^ [_123895]), _123895)]], -(connected(_123895))], (3867 ^ _39627) ^ [] : [connected(_123895), 3870 ^ _39627 : [(3871 ^ _39627) ^ [_124189, _124191] : [in(_124191, relation_field(_123895)), in(_124189, relation_field(_123895)), -(_124191 = _124189), -(in(ordered_pair(_124191, _124189), _123895)), -(in(ordered_pair(_124189, _124191), _123895))]]]]], (3915 ^ _39627) ^ [_125641, _125643] : [3916 ^ _39627 : [(3917 ^ _39627) ^ [] : [_125643 = empty_set], (3919 ^ _39627) ^ [] : [_125643 = singleton(_125641)]], -(subset(_125643, singleton(_125641)))], (3905 ^ _39627) ^ [_125381, _125383] : [subset(_125383, singleton(_125381)), -(_125383 = empty_set), -(_125383 = singleton(_125381))], (3923 ^ _39627) ^ [_125935, _125937] : [in(_125937, _125935), -(subset(_125937, union(_125935)))], (3929 ^ _39627) ^ [_126206, _126208, _126210, _126212] : [in(ordered_pair(_126212, _126210), cartesian_product2(_126208, _126206)), 3932 ^ _39627 : [(3933 ^ _39627) ^ [] : [-(in(_126212, _126208))], (3935 ^ _39627) ^ [] : [-(in(_126210, _126206))]]], (3937 ^ _39627) ^ [_126471, _126473, _126475, _126477] : [-(in(ordered_pair(_126477, _126475), cartesian_product2(_126473, _126471))), in(_126477, _126473), in(_126475, _126471)], (3947 ^ _39627) ^ [_126804, _126806] : [3949 ^ _39627 : [(3950 ^ _39627) ^ [] : [-(in(3948 ^ [_126804, _126806], _126806))], (3952 ^ _39627) ^ [] : [in(3948 ^ [_126804, _126806], _126804)]], -(element(_126806, powerset(_126804)))], (3956 ^ _39627) ^ [_127177, _127179, _127181] : [relation(_127177), function(_127177), 3963 ^ _39627 : [(3964 ^ _39627) ^ [] : [in(_127179, relation_dom(relation_dom_restriction(_127177, _127181))), 3967 ^ _39627 : [(3968 ^ _39627) ^ [] : [-(in(_127179, relation_dom(_127177)))], (3970 ^ _39627) ^ [] : [-(in(_127179, _127181))]]], (3972 ^ _39627) ^ [] : [-(in(_127179, relation_dom(relation_dom_restriction(_127177, _127181)))), in(_127179, relation_dom(_127177)), in(_127179, _127181)]]], (3983 ^ _39627) ^ [] : [empty(3981 ^ [])], (3985 ^ _39627) ^ [] : [-(epsilon_transitive(3981 ^ []))], (3987 ^ _39627) ^ [] : [-(epsilon_connected(3981 ^ []))], (3989 ^ _39627) ^ [] : [-(ordinal(3981 ^ []))], (3991 ^ _39627) ^ [] : [-(natural(3981 ^ []))], (3994 ^ _39627) ^ [] : [empty(3992 ^ [])], (3996 ^ _39627) ^ [] : [-(finite(3992 ^ []))], (3999 ^ _39627) ^ [] : [-(relation(3997 ^ []))], (4001 ^ _39627) ^ [] : [-(function(3997 ^ []))], (4004 ^ _39627) ^ [_128622, _128624] : [-(relation_of2(4002 ^ [_128622, _128624], _128624, _128622))], (4006 ^ _39627) ^ [_128696, _128698] : [-(relation(4002 ^ [_128696, _128698]))], (4008 ^ _39627) ^ [_128768, _128770] : [-(function(4002 ^ [_128768, _128770]))], (4010 ^ _39627) ^ [_128820, _128822] : [-(quasi_total(4002 ^ [_128820, _128822], _128822, _128820))], (4013 ^ _39627) ^ [] : [-(epsilon_transitive(4011 ^ []))], (4015 ^ _39627) ^ [] : [-(epsilon_connected(4011 ^ []))], (4017 ^ _39627) ^ [] : [-(ordinal(4011 ^ []))], (4020 ^ _39627) ^ [] : [-(relation(4018 ^ []))], (4022 ^ _39627) ^ [] : [-(function(4018 ^ []))], (4024 ^ _39627) ^ [] : [-(one_to_one(4018 ^ []))], (4026 ^ _39627) ^ [] : [-(empty(4018 ^ []))], (4029 ^ _39627) ^ [] : [-(empty(4027 ^ []))], (4031 ^ _39627) ^ [] : [-(relation(4027 ^ []))], (4033 ^ _39627) ^ [_129556] : [-(empty(_129556)), 4037 ^ _39627 : [(4038 ^ _39627) ^ [] : [-(element(4036 ^ [_129556], powerset(_129556)))], (4040 ^ _39627) ^ [] : [empty(4036 ^ [_129556])]]], (4043 ^ _39627) ^ [] : [-(empty(4041 ^ []))], (4046 ^ _39627) ^ [_130068] : [-(element(4044 ^ [_130068], powerset(_130068)))], (4048 ^ _39627) ^ [_130139] : [-(empty(4044 ^ [_130139]))], (4050 ^ _39627) ^ [_130207] : [-(relation(4044 ^ [_130207]))], (4052 ^ _39627) ^ [_130275] : [-(function(4044 ^ [_130275]))], (4054 ^ _39627) ^ [_130343] : [-(one_to_one(4044 ^ [_130343]))], (4056 ^ _39627) ^ [_130411] : [-(epsilon_transitive(4044 ^ [_130411]))], (4058 ^ _39627) ^ [_130479] : [-(epsilon_connected(4044 ^ [_130479]))], (4060 ^ _39627) ^ [_130547] : [-(ordinal(4044 ^ [_130547]))], (4062 ^ _39627) ^ [_130615] : [-(natural(4044 ^ [_130615]))], (4064 ^ _39627) ^ [_130663] : [-(finite(4044 ^ [_130663]))], (4067 ^ _39627) ^ [] : [-(relation(4065 ^ []))], (4069 ^ _39627) ^ [] : [-(empty(4065 ^ []))], (4071 ^ _39627) ^ [] : [-(function(4065 ^ []))], (4074 ^ _39627) ^ [] : [-(relation(4072 ^ []))], (4076 ^ _39627) ^ [] : [-(function(4072 ^ []))], (4078 ^ _39627) ^ [] : [-(one_to_one(4072 ^ []))], (4080 ^ _39627) ^ [] : [-(empty(4072 ^ []))], (4082 ^ _39627) ^ [] : [-(epsilon_transitive(4072 ^ []))], (4084 ^ _39627) ^ [] : [-(epsilon_connected(4072 ^ []))], (4086 ^ _39627) ^ [] : [-(ordinal(4072 ^ []))], (4089 ^ _39627) ^ [_131507, _131509] : [-(relation_of2(4087 ^ [_131507, _131509], _131509, _131507))], (4091 ^ _39627) ^ [_131581, _131583] : [-(relation(4087 ^ [_131581, _131583]))], (4093 ^ _39627) ^ [_131633, _131635] : [-(function(4087 ^ [_131633, _131635]))], (4096 ^ _39627) ^ [] : [empty(4094 ^ [])], (4098 ^ _39627) ^ [] : [-(relation(4094 ^ []))], (4101 ^ _39627) ^ [_131939] : [-(element(4099 ^ [_131939], powerset(_131939)))], (4103 ^ _39627) ^ [_131990] : [-(empty(4099 ^ [_131990]))], (4106 ^ _39627) ^ [] : [empty(4104 ^ [])], (4108 ^ _39627) ^ [_132179] : [-(empty(_132179)), 4112 ^ _39627 : [(4113 ^ _39627) ^ [] : [-(element(4111 ^ [_132179], powerset(_132179)))], (4115 ^ _39627) ^ [] : [empty(4111 ^ [_132179])], (4117 ^ _39627) ^ [] : [-(finite(4111 ^ [_132179]))]]], (4120 ^ _39627) ^ [] : [-(relation(4118 ^ []))], (4122 ^ _39627) ^ [] : [-(function(4118 ^ []))], (4124 ^ _39627) ^ [] : [-(one_to_one(4118 ^ []))], (4127 ^ _39627) ^ [] : [empty(4125 ^ [])], (4129 ^ _39627) ^ [] : [-(epsilon_transitive(4125 ^ []))], (4131 ^ _39627) ^ [] : [-(epsilon_connected(4125 ^ []))], (4133 ^ _39627) ^ [] : [-(ordinal(4125 ^ []))], (4136 ^ _39627) ^ [] : [-(relation(4134 ^ []))], (4138 ^ _39627) ^ [] : [-(relation_empty_yielding(4134 ^ []))], (4141 ^ _39627) ^ [] : [-(relation(4139 ^ []))], (4143 ^ _39627) ^ [] : [-(relation_empty_yielding(4139 ^ []))], (4145 ^ _39627) ^ [] : [-(function(4139 ^ []))], (4147 ^ _39627) ^ [_133456, _133458, _133460] : [relation_of2(_133456, _133460, _133458), -(relation_dom_as_subset(_133460, _133458, _133456) = relation_dom(_133456))], (4153 ^ _39627) ^ [_133700, _133702, _133704] : [relation_of2(_133700, _133704, _133702), -(relation_rng_as_subset(_133704, _133702, _133700) = relation_rng(_133700))], (4159 ^ _39627) ^ [_133930, _133932] : [element(_133930, powerset(powerset(_133932))), -(union_of_subsets(_133932, _133930) = union(_133930))], (4165 ^ _39627) ^ [_134158, _134160] : [element(_134158, powerset(powerset(_134160))), -(meet_of_subsets(_134160, _134158) = set_meet(_134158))], (4171 ^ _39627) ^ [_134400, _134402, _134404] : [-(subset_difference(_134404, _134402, _134400) = set_difference(_134402, _134400)), element(_134402, powerset(_134404)), element(_134400, powerset(_134404))], (4181 ^ _39627) ^ [_134774, _134776, _134778] : [relation_of2_as_subset(_134774, _134778, _134776), -(relation_of2(_134774, _134778, _134776))], (4187 ^ _39627) ^ [_134946, _134948, _134950] : [relation_of2(_134946, _134950, _134948), -(relation_of2_as_subset(_134946, _134950, _134948))], (4193 ^ _39627) ^ [_135168, _135170] : [ordinal(_135170), ordinal(_135168), 4200 ^ _39627 : [(4201 ^ _39627) ^ [] : [ordinal_subset(_135170, _135168), -(subset(_135170, _135168))], (4207 ^ _39627) ^ [] : [subset(_135170, _135168), -(ordinal_subset(_135170, _135168))]]], (4213 ^ _39627) ^ [_135744, _135746] : [equipotent(_135746, _135744), -(are_equipotent(_135746, _135744))], (4219 ^ _39627) ^ [_135906, _135908] : [are_equipotent(_135908, _135906), -(equipotent(_135908, _135906))], (4225 ^ _39627) ^ [_136118, _136120] : [-(ordinal_subset(_136120, _136120)), ordinal(_136120), ordinal(_136118)], (4235 ^ _39627) ^ [_136398, _136400] : [-(subset(_136400, _136400))], (4237 ^ _39627) ^ [_136492, _136494] : [-(equipotent(_136494, _136494))], (4239 ^ _39627) ^ [_136601, _136603] : [-(empty(_136603)), relation(_136601), 4251 ^ _39627 : [(4278 ^ _39627) ^ [] : [4249 ^ [_136601, _136603] = 4250 ^ [_136601, _136603]], (4252 ^ _39627) ^ [] : [-(in(4248 ^ [_136601, _136603], _136603))], (4255 ^ _39627) ^ [] : [-(4248 ^ [_136601, _136603] = 4253 ^ [_136601, _136603])], (4257 ^ _39627) ^ [] : [-(in(4249 ^ [_136601, _136603], 4253 ^ [_136601, _136603]))], (4259 ^ _39627) ^ [_137883] : [in(_137883, 4253 ^ [_136601, _136603]), -(in(ordered_pair(4249 ^ [_136601, _136603], _137883), _136601))], (4265 ^ _39627) ^ [] : [-(in(4248 ^ [_136601, _136603], _136603))], (4268 ^ _39627) ^ [] : [-(4248 ^ [_136601, _136603] = 4266 ^ [_136601, _136603])], (4270 ^ _39627) ^ [] : [-(in(4250 ^ [_136601, _136603], 4266 ^ [_136601, _136603]))], (4272 ^ _39627) ^ [_138432] : [in(_138432, 4266 ^ [_136601, _136603]), -(in(ordered_pair(4250 ^ [_136601, _136603], _138432), _136601))]], 4280 ^ _39627 : [(4281 ^ _39627) ^ [] : [-(relation(4279 ^ [_136601, _136603]))], (4283 ^ _39627) ^ [] : [-(function(4279 ^ [_136601, _136603]))], (4285 ^ _39627) ^ [_139031, _139033] : [in(ordered_pair(_139033, _139031), 4279 ^ [_136601, _136603]), 4288 ^ _39627 : [(4289 ^ _39627) ^ [] : [-(in(_139033, _136603))], (4291 ^ _39627) ^ [] : [-(in(_139033, _136603))], (4294 ^ _39627) ^ [] : [-(_139033 = 4292 ^ [_136601, _136603, _139031, _139033])], (4296 ^ _39627) ^ [] : [-(in(_139031, 4292 ^ [_136601, _136603, _139031, _139033]))], (4298 ^ _39627) ^ [_139613] : [in(_139613, 4292 ^ [_136601, _136603, _139031, _139033]), -(in(ordered_pair(_139031, _139613), _136601))]]], (4304 ^ _39627) ^ [_139842, _139844] : [-(in(ordered_pair(_139844, _139842), 4279 ^ [_136601, _136603])), in(_139844, _136603), in(_139844, _136603), 4313 ^ _39627 : [(4314 ^ _39627) ^ [_140158] : [_139844 = _140158, in(_139842, _140158), 4322 ^ _39627 : [(4323 ^ _39627) ^ [] : [-(in(4321 ^ [_136601, _136603, _139842, _139844, _140158], _140158))], (4325 ^ _39627) ^ [] : [in(ordered_pair(_139842, 4321 ^ [_136601, _136603, _139842, _139844, _140158]), _136601)]]]]]]], (4329 ^ _39627) ^ [_140755] : [4333 ^ _39627 : [(4334 ^ _39627) ^ [] : [-(in(4330 ^ [_140755], _140755))], (4336 ^ _39627) ^ [] : [-(4331 ^ [_140755] = singleton(4330 ^ [_140755]))], (4338 ^ _39627) ^ [] : [-(in(4330 ^ [_140755], _140755))], (4340 ^ _39627) ^ [] : [-(4332 ^ [_140755] = singleton(4330 ^ [_140755]))], (4342 ^ _39627) ^ [] : [4331 ^ [_140755] = 4332 ^ [_140755]]], 4344 ^ _39627 : [(4345 ^ _39627) ^ [] : [-(relation(4343 ^ [_140755]))], (4347 ^ _39627) ^ [] : [-(function(4343 ^ [_140755]))], (4349 ^ _39627) ^ [_141817, _141819] : [in(ordered_pair(_141819, _141817), 4343 ^ [_140755]), 4352 ^ _39627 : [(4353 ^ _39627) ^ [] : [-(in(_141819, _140755))], (4355 ^ _39627) ^ [] : [-(in(_141819, _140755))], (4357 ^ _39627) ^ [] : [-(_141817 = singleton(_141819))]]], (4359 ^ _39627) ^ [_142160, _142162] : [-(in(ordered_pair(_142162, _142160), 4343 ^ [_140755])), in(_142162, _140755), in(_142162, _140755), _142160 = singleton(_142162)]]], (4373 ^ _39627) ^ [_142582] : [4374 ^ _39627 : [(4375 ^ _39627) ^ [_142703] : [ordinal(_142703), in(_142703, _142582)]], 4381 ^ _39627 : [(4382 ^ _39627) ^ [] : [-(ordinal(4380 ^ [_142582]))], (4384 ^ _39627) ^ [] : [-(in(4380 ^ [_142582], _142582))], (4386 ^ _39627) ^ [_143083] : [ordinal(_143083), in(_143083, _142582), -(ordinal_subset(4380 ^ [_142582], _143083))]]], (4396 ^ _39627) ^ [_143416, _143418, _143420] : [relation(_143418), relation(_143416), function(_143416), 4408 ^ _39627 : [(4409 ^ _39627) ^ [] : [-(relation(4407 ^ [_143416, _143418, _143420]))], (4411 ^ _39627) ^ [_143989, _143991] : [in(ordered_pair(_143991, _143989), 4407 ^ [_143416, _143418, _143420]), 4414 ^ _39627 : [(4415 ^ _39627) ^ [] : [-(in(_143991, _143420))], (4417 ^ _39627) ^ [] : [-(in(_143989, _143420))], (4419 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_143416, _143991), apply(_143416, _143989)), _143418))]]], (4421 ^ _39627) ^ [_144378, _144380] : [-(in(ordered_pair(_144380, _144378), 4407 ^ [_143416, _143418, _143420])), in(_144380, _143420), in(_144378, _143420), in(ordered_pair(apply(_143416, _144380), apply(_143416, _144378)), _143418)]]], (4435 ^ _39627) ^ [_144869, _144871] : [-(empty(_144871)), relation(_144869), 4447 ^ _39627 : [(4474 ^ _39627) ^ [] : [4445 ^ [_144869, _144871] = 4446 ^ [_144869, _144871]], (4448 ^ _39627) ^ [] : [-(in(4444 ^ [_144869, _144871], _144871))], (4451 ^ _39627) ^ [] : [-(4444 ^ [_144869, _144871] = 4449 ^ [_144869, _144871])], (4453 ^ _39627) ^ [] : [-(in(4445 ^ [_144869, _144871], 4449 ^ [_144869, _144871]))], (4455 ^ _39627) ^ [_146138] : [in(_146138, 4449 ^ [_144869, _144871]), -(in(ordered_pair(4445 ^ [_144869, _144871], _146138), _144869))], (4461 ^ _39627) ^ [] : [-(in(4444 ^ [_144869, _144871], _144871))], (4464 ^ _39627) ^ [] : [-(4444 ^ [_144869, _144871] = 4462 ^ [_144869, _144871])], (4466 ^ _39627) ^ [] : [-(in(4446 ^ [_144869, _144871], 4462 ^ [_144869, _144871]))], (4468 ^ _39627) ^ [_146687] : [in(_146687, 4462 ^ [_144869, _144871]), -(in(ordered_pair(4446 ^ [_144869, _144871], _146687), _144869))]], 4476 ^ _39627 : [(4477 ^ _39627) ^ [_147115] : [in(_147115, 4475 ^ [_144869, _144871]), 4481 ^ _39627 : [(4482 ^ _39627) ^ [] : [-(in(4480 ^ [_144869, _144871, _147115], _144871))], (4484 ^ _39627) ^ [] : [-(in(4480 ^ [_144869, _144871, _147115], _144871))], (4487 ^ _39627) ^ [] : [-(4480 ^ [_144869, _144871, _147115] = 4485 ^ [_144869, _144871, _147115])], (4489 ^ _39627) ^ [] : [-(in(_147115, 4485 ^ [_144869, _144871, _147115]))], (4491 ^ _39627) ^ [_147804] : [in(_147804, 4485 ^ [_144869, _144871, _147115]), -(in(ordered_pair(_147115, _147804), _144869))]]], (4497 ^ _39627) ^ [_148021] : [-(in(_148021, 4475 ^ [_144869, _144871])), 4498 ^ _39627 : [(4499 ^ _39627) ^ [_148163] : [in(_148163, _144871), in(_148163, _144871), 4506 ^ _39627 : [(4507 ^ _39627) ^ [_148427] : [_148163 = _148427, in(_148021, _148427), 4515 ^ _39627 : [(4516 ^ _39627) ^ [] : [-(in(4514 ^ [_144869, _144871, _148021, _148163, _148427], _148427))], (4518 ^ _39627) ^ [] : [in(ordered_pair(_148021, 4514 ^ [_144869, _144871, _148021, _148163, _148427]), _144869)]]]]]]]]], (4522 ^ _39627) ^ [_149030, _149032] : [-(empty(_149032)), relation(_149030), 4529 ^ _39627 : [(4530 ^ _39627) ^ [_149498] : [4534 ^ _39627 : [(4573 ^ _39627) ^ [] : [4532 ^ [_149030, _149032, _149498] = 4533 ^ [_149030, _149032, _149498]], (4535 ^ _39627) ^ [] : [-(4531 ^ [_149030, _149032, _149498] = 4532 ^ [_149030, _149032, _149498])], (4539 ^ _39627) ^ [] : [-(ordered_pair(4536 ^ [_149030, _149032, _149498], 4537 ^ [_149030, _149032, _149498]) = 4532 ^ [_149030, _149032, _149498])], (4541 ^ _39627) ^ [] : [-(in(4536 ^ [_149030, _149032, _149498], _149032))], (4544 ^ _39627) ^ [] : [-(4536 ^ [_149030, _149032, _149498] = 4542 ^ [_149030, _149032, _149498])], (4546 ^ _39627) ^ [] : [-(in(4537 ^ [_149030, _149032, _149498], 4542 ^ [_149030, _149032, _149498]))], (4548 ^ _39627) ^ [_151276] : [in(_151276, 4542 ^ [_149030, _149032, _149498]), -(in(ordered_pair(4537 ^ [_149030, _149032, _149498], _151276), _149030))], (4554 ^ _39627) ^ [] : [-(4531 ^ [_149030, _149032, _149498] = 4533 ^ [_149030, _149032, _149498])], (4558 ^ _39627) ^ [] : [-(ordered_pair(4555 ^ [_149030, _149032, _149498], 4556 ^ [_149030, _149032, _149498]) = 4533 ^ [_149030, _149032, _149498])], (4560 ^ _39627) ^ [] : [-(in(4555 ^ [_149030, _149032, _149498], _149032))], (4563 ^ _39627) ^ [] : [-(4555 ^ [_149030, _149032, _149498] = 4561 ^ [_149030, _149032, _149498])], (4565 ^ _39627) ^ [] : [-(in(4556 ^ [_149030, _149032, _149498], 4561 ^ [_149030, _149032, _149498]))], (4567 ^ _39627) ^ [_152295] : [in(_152295, 4561 ^ [_149030, _149032, _149498]), -(in(ordered_pair(4556 ^ [_149030, _149032, _149498], _152295), _149030))]], 4575 ^ _39627 : [(4576 ^ _39627) ^ [_152785] : [in(_152785, 4574 ^ [_149030, _149032, _149498]), 4580 ^ _39627 : [(4581 ^ _39627) ^ [] : [-(in(4579 ^ [_149030, _149032, _149498, _152785], cartesian_product2(_149032, _149498)))], (4583 ^ _39627) ^ [] : [-(4579 ^ [_149030, _149032, _149498, _152785] = _152785)], (4587 ^ _39627) ^ [] : [-(ordered_pair(4584 ^ [_149030, _149032, _149498, _152785], 4585 ^ [_149030, _149032, _149498, _152785]) = _152785)], (4589 ^ _39627) ^ [] : [-(in(4584 ^ [_149030, _149032, _149498, _152785], _149032))], (4592 ^ _39627) ^ [] : [-(4584 ^ [_149030, _149032, _149498, _152785] = 4590 ^ [_149030, _149032, _149498, _152785])], (4594 ^ _39627) ^ [] : [-(in(4585 ^ [_149030, _149032, _149498, _152785], 4590 ^ [_149030, _149032, _149498, _152785]))], (4596 ^ _39627) ^ [_154016] : [in(_154016, 4590 ^ [_149030, _149032, _149498, _152785]), -(in(ordered_pair(4585 ^ [_149030, _149032, _149498, _152785], _154016), _149030))]]], (4602 ^ _39627) ^ [_154271] : [-(in(_154271, 4574 ^ [_149030, _149032, _149498])), 4603 ^ _39627 : [(4604 ^ _39627) ^ [_154447] : [in(_154447, cartesian_product2(_149032, _149498)), _154447 = _154271, 4611 ^ _39627 : [(4612 ^ _39627) ^ [_154766, _154768] : [ordered_pair(_154768, _154766) = _154271, in(_154768, _149032), 4619 ^ _39627 : [(4620 ^ _39627) ^ [_155064] : [_154768 = _155064, in(_154766, _155064), 4628 ^ _39627 : [(4629 ^ _39627) ^ [] : [-(in(4627 ^ [_149030, _149032, _149498, _154271, _154447, _154766, _154768, _155064], _155064))], (4631 ^ _39627) ^ [] : [in(ordered_pair(_154766, 4627 ^ [_149030, _149032, _149498, _154271, _154447, _154766, _154768, _155064]), _149030)]]]]]]]]]]]]], (4635 ^ _39627) ^ [_155733] : [4639 ^ _39627 : [(4640 ^ _39627) ^ [] : [-(in(4636 ^ [_155733], _155733))], (4642 ^ _39627) ^ [] : [-(4637 ^ [_155733] = singleton(4636 ^ [_155733]))], (4644 ^ _39627) ^ [] : [-(in(4636 ^ [_155733], _155733))], (4646 ^ _39627) ^ [] : [-(4638 ^ [_155733] = singleton(4636 ^ [_155733]))], (4648 ^ _39627) ^ [] : [4637 ^ [_155733] = 4638 ^ [_155733]]], 4650 ^ _39627 : [(4651 ^ _39627) ^ [_156619] : [in(_156619, 4649 ^ [_155733]), 4655 ^ _39627 : [(4656 ^ _39627) ^ [] : [-(in(4654 ^ [_155733, _156619], _155733))], (4658 ^ _39627) ^ [] : [-(in(4654 ^ [_155733, _156619], _155733))], (4660 ^ _39627) ^ [] : [-(_156619 = singleton(4654 ^ [_155733, _156619]))]]], (4662 ^ _39627) ^ [_157031] : [-(in(_157031, 4649 ^ [_155733])), 4663 ^ _39627 : [(4664 ^ _39627) ^ [_157138] : [in(_157138, _155733), in(_157138, _155733), _157031 = singleton(_157138)]]]]], (4676 ^ _39627) ^ [_157518, _157520] : [4680 ^ _39627 : [(4681 ^ _39627) ^ [] : [-(4677 ^ [_157518, _157520] = 4678 ^ [_157518, _157520])], (4685 ^ _39627) ^ [] : [-(ordered_pair(4682 ^ [_157518, _157520], 4683 ^ [_157518, _157520]) = 4678 ^ [_157518, _157520])], (4687 ^ _39627) ^ [] : [-(in(4682 ^ [_157518, _157520], _157520))], (4689 ^ _39627) ^ [] : [-(4683 ^ [_157518, _157520] = singleton(4682 ^ [_157518, _157520]))], (4691 ^ _39627) ^ [] : [-(4677 ^ [_157518, _157520] = 4679 ^ [_157518, _157520])], (4695 ^ _39627) ^ [] : [-(ordered_pair(4692 ^ [_157518, _157520], 4693 ^ [_157518, _157520]) = 4679 ^ [_157518, _157520])], (4697 ^ _39627) ^ [] : [-(in(4692 ^ [_157518, _157520], _157520))], (4699 ^ _39627) ^ [] : [-(4693 ^ [_157518, _157520] = singleton(4692 ^ [_157518, _157520]))], (4701 ^ _39627) ^ [] : [4678 ^ [_157518, _157520] = 4679 ^ [_157518, _157520]]], 4703 ^ _39627 : [(4704 ^ _39627) ^ [_159391] : [in(_159391, 4702 ^ [_157518, _157520]), 4708 ^ _39627 : [(4709 ^ _39627) ^ [] : [-(in(4707 ^ [_157518, _157520, _159391], cartesian_product2(_157520, _157518)))], (4711 ^ _39627) ^ [] : [-(4707 ^ [_157518, _157520, _159391] = _159391)], (4715 ^ _39627) ^ [] : [-(ordered_pair(4712 ^ [_157518, _157520, _159391], 4713 ^ [_157518, _157520, _159391]) = _159391)], (4717 ^ _39627) ^ [] : [-(in(4712 ^ [_157518, _157520, _159391], _157520))], (4719 ^ _39627) ^ [] : [-(4713 ^ [_157518, _157520, _159391] = singleton(4712 ^ [_157518, _157520, _159391]))]]], (4721 ^ _39627) ^ [_160231] : [-(in(_160231, 4702 ^ [_157518, _157520])), 4722 ^ _39627 : [(4723 ^ _39627) ^ [_160372] : [in(_160372, cartesian_product2(_157520, _157518)), _160372 = _160231, 4730 ^ _39627 : [(4731 ^ _39627) ^ [_160652, _160654] : [ordered_pair(_160654, _160652) = _160231, in(_160654, _157520), _160652 = singleton(_160654)]]]]]]], (4743 ^ _39627) ^ [_161099, _161101, _161103] : [relation(_161101), relation(_161099), function(_161099), 4759 ^ _39627 : [(4760 ^ _39627) ^ [] : [-(4756 ^ [_161099, _161101, _161103] = 4757 ^ [_161099, _161101, _161103])], (4764 ^ _39627) ^ [] : [-(4757 ^ [_161099, _161101, _161103] = ordered_pair(4761 ^ [_161099, _161101, _161103], 4762 ^ [_161099, _161101, _161103]))], (4766 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_161099, 4761 ^ [_161099, _161101, _161103]), apply(_161099, 4762 ^ [_161099, _161101, _161103])), _161101))], (4768 ^ _39627) ^ [] : [-(4756 ^ [_161099, _161101, _161103] = 4758 ^ [_161099, _161101, _161103])], (4772 ^ _39627) ^ [] : [-(4758 ^ [_161099, _161101, _161103] = ordered_pair(4769 ^ [_161099, _161101, _161103], 4770 ^ [_161099, _161101, _161103]))], (4774 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_161099, 4769 ^ [_161099, _161101, _161103]), apply(_161099, 4770 ^ [_161099, _161101, _161103])), _161101))], (4776 ^ _39627) ^ [] : [4757 ^ [_161099, _161101, _161103] = 4758 ^ [_161099, _161101, _161103]]], 4778 ^ _39627 : [(4779 ^ _39627) ^ [_163209] : [in(_163209, 4777 ^ [_161099, _161101, _161103]), 4783 ^ _39627 : [(4784 ^ _39627) ^ [] : [-(in(4782 ^ [_161099, _161101, _161103, _163209], cartesian_product2(_161103, _161103)))], (4786 ^ _39627) ^ [] : [-(4782 ^ [_161099, _161101, _161103, _163209] = _163209)], (4790 ^ _39627) ^ [] : [-(_163209 = ordered_pair(4787 ^ [_161099, _161101, _161103, _163209], 4788 ^ [_161099, _161101, _161103, _163209]))], (4792 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_161099, 4787 ^ [_161099, _161101, _161103, _163209]), apply(_161099, 4788 ^ [_161099, _161101, _161103, _163209])), _161101))]]], (4794 ^ _39627) ^ [_164018] : [-(in(_164018, 4777 ^ [_161099, _161101, _161103])), 4795 ^ _39627 : [(4796 ^ _39627) ^ [_164166] : [in(_164166, cartesian_product2(_161103, _161103)), _164166 = _164018, 4803 ^ _39627 : [(4804 ^ _39627) ^ [_164457, _164459] : [_164018 = ordered_pair(_164459, _164457), in(ordered_pair(apply(_161099, _164459), apply(_161099, _164457)), _161101)]]]]]]], (4812 ^ _39627) ^ [_164805] : [4816 ^ _39627 : [(4817 ^ _39627) ^ [] : [-(4813 ^ [_164805] = 4814 ^ [_164805])], (4819 ^ _39627) ^ [] : [-(ordinal(4814 ^ [_164805]))], (4821 ^ _39627) ^ [] : [-(4813 ^ [_164805] = 4815 ^ [_164805])], (4823 ^ _39627) ^ [] : [-(ordinal(4815 ^ [_164805]))], (4825 ^ _39627) ^ [] : [4814 ^ [_164805] = 4815 ^ [_164805]]], 4827 ^ _39627 : [(4828 ^ _39627) ^ [_165640] : [in(_165640, 4826 ^ [_164805]), 4832 ^ _39627 : [(4833 ^ _39627) ^ [] : [-(in(4831 ^ [_164805, _165640], _164805))], (4835 ^ _39627) ^ [] : [-(4831 ^ [_164805, _165640] = _165640)], (4837 ^ _39627) ^ [] : [-(ordinal(_165640))]]], (4839 ^ _39627) ^ [_166036] : [-(in(_166036, 4826 ^ [_164805])), 4840 ^ _39627 : [(4841 ^ _39627) ^ [_166140] : [in(_166140, _164805), _166140 = _166036, ordinal(_166036)]]]]], (4853 ^ _39627) ^ [_166514, _166516] : [ordinal(_166514), 4861 ^ _39627 : [(4862 ^ _39627) ^ [] : [-(4858 ^ [_166514, _166516] = 4859 ^ [_166514, _166516])], (4865 ^ _39627) ^ [] : [-(ordinal(4863 ^ [_166514, _166516]))], (4867 ^ _39627) ^ [] : [-(4859 ^ [_166514, _166516] = 4863 ^ [_166514, _166516])], (4869 ^ _39627) ^ [] : [-(in(4863 ^ [_166514, _166516], _166516))], (4871 ^ _39627) ^ [] : [-(4858 ^ [_166514, _166516] = 4860 ^ [_166514, _166516])], (4874 ^ _39627) ^ [] : [-(ordinal(4872 ^ [_166514, _166516]))], (4876 ^ _39627) ^ [] : [-(4860 ^ [_166514, _166516] = 4872 ^ [_166514, _166516])], (4878 ^ _39627) ^ [] : [-(in(4872 ^ [_166514, _166516], _166516))], (4880 ^ _39627) ^ [] : [4859 ^ [_166514, _166516] = 4860 ^ [_166514, _166516]]], 4882 ^ _39627 : [(4883 ^ _39627) ^ [_168116] : [in(_168116, 4881 ^ [_166514, _166516]), 4887 ^ _39627 : [(4888 ^ _39627) ^ [] : [-(in(4886 ^ [_166514, _166516, _168116], succ(_166514)))], (4890 ^ _39627) ^ [] : [-(4886 ^ [_166514, _166516, _168116] = _168116)], (4893 ^ _39627) ^ [] : [-(ordinal(4891 ^ [_166514, _166516, _168116]))], (4895 ^ _39627) ^ [] : [-(_168116 = 4891 ^ [_166514, _166516, _168116])], (4897 ^ _39627) ^ [] : [-(in(4891 ^ [_166514, _166516, _168116], _166516))]]], (4899 ^ _39627) ^ [_168803] : [-(in(_168803, 4881 ^ [_166514, _166516])), 4900 ^ _39627 : [(4901 ^ _39627) ^ [_168932] : [in(_168932, succ(_166514)), _168932 = _168803, 4908 ^ _39627 : [(4909 ^ _39627) ^ [_169185] : [ordinal(_169185), _168803 = _169185, in(_169185, _166516)]]]]]]], (4921 ^ _39627) ^ [_169600, _169602] : [-(empty(_169602)), relation(_169600), 4929 ^ _39627 : [(4930 ^ _39627) ^ [_170066, _170068] : [in(_170066, 4928 ^ [_169600, _169602, _170068]), 4933 ^ _39627 : [(4934 ^ _39627) ^ [] : [-(in(_170066, cartesian_product2(_169602, _170068)))], (4938 ^ _39627) ^ [] : [-(ordered_pair(4935 ^ [_169600, _169602, _170066, _170068], 4936 ^ [_169600, _169602, _170066, _170068]) = _170066)], (4940 ^ _39627) ^ [] : [-(in(4935 ^ [_169600, _169602, _170066, _170068], _169602))], (4943 ^ _39627) ^ [] : [-(4935 ^ [_169600, _169602, _170066, _170068] = 4941 ^ [_169600, _169602, _170066, _170068])], (4945 ^ _39627) ^ [] : [-(in(4936 ^ [_169600, _169602, _170066, _170068], 4941 ^ [_169600, _169602, _170066, _170068]))], (4947 ^ _39627) ^ [_171068] : [in(_171068, 4941 ^ [_169600, _169602, _170066, _170068]), -(in(ordered_pair(4936 ^ [_169600, _169602, _170066, _170068], _171068), _169600))]]], (4953 ^ _39627) ^ [_171321, _171323] : [-(in(_171321, 4928 ^ [_169600, _169602, _171323])), in(_171321, cartesian_product2(_169602, _171323)), 4958 ^ _39627 : [(4959 ^ _39627) ^ [_171588, _171590] : [ordered_pair(_171590, _171588) = _171321, in(_171590, _169602), 4966 ^ _39627 : [(4967 ^ _39627) ^ [_171876] : [_171590 = _171876, in(_171588, _171876), 4975 ^ _39627 : [(4976 ^ _39627) ^ [] : [-(in(4974 ^ [_169600, _169602, _171321, _171323, _171588, _171590, _171876], _171876))], (4978 ^ _39627) ^ [] : [in(ordered_pair(_171588, 4974 ^ [_169600, _169602, _171321, _171323, _171588, _171590, _171876]), _169600)]]]]]]]]], (4983 ^ _39627) ^ [_172657, _172659, _172661] : [in(_172657, 4981 ^ [_172659, _172661]), 4986 ^ _39627 : [(4987 ^ _39627) ^ [] : [-(in(_172657, cartesian_product2(_172661, _172659)))], (4991 ^ _39627) ^ [] : [-(ordered_pair(4988 ^ [_172657, _172659, _172661], 4989 ^ [_172657, _172659, _172661]) = _172657)], (4993 ^ _39627) ^ [] : [-(in(4988 ^ [_172657, _172659, _172661], _172661))], (4995 ^ _39627) ^ [] : [-(4989 ^ [_172657, _172659, _172661] = singleton(4988 ^ [_172657, _172659, _172661]))]]], (4997 ^ _39627) ^ [_173303, _173305, _173307] : [-(in(_173303, 4981 ^ [_173305, _173307])), in(_173303, cartesian_product2(_173307, _173305)), 5002 ^ _39627 : [(5003 ^ _39627) ^ [_173529, _173531] : [ordered_pair(_173531, _173529) = _173303, in(_173531, _173307), _173529 = singleton(_173531)]]], (5015 ^ _39627) ^ [_173953, _173955, _173957] : [relation(_173955), relation(_173953), function(_173953), 5027 ^ _39627 : [(5028 ^ _39627) ^ [_174442] : [in(_174442, 5026 ^ [_173953, _173955, _173957]), 5031 ^ _39627 : [(5032 ^ _39627) ^ [] : [-(in(_174442, cartesian_product2(_173957, _173957)))], (5036 ^ _39627) ^ [] : [-(_174442 = ordered_pair(5033 ^ [_173953, _173955, _173957, _174442], 5034 ^ [_173953, _173955, _173957, _174442]))], (5038 ^ _39627) ^ [] : [-(in(ordered_pair(apply(_173953, 5033 ^ [_173953, _173955, _173957, _174442]), apply(_173953, 5034 ^ [_173953, _173955, _173957, _174442])), _173955))]]], (5040 ^ _39627) ^ [_175050] : [-(in(_175050, 5026 ^ [_173953, _173955, _173957])), in(_175050, cartesian_product2(_173957, _173957)), 5045 ^ _39627 : [(5046 ^ _39627) ^ [_175291, _175293] : [_175050 = ordered_pair(_175293, _175291), in(ordered_pair(apply(_173953, _175293), apply(_173953, _175291)), _173955)]]]]], (5055 ^ _39627) ^ [_175719, _175721] : [in(_175719, 5053 ^ [_175721]), 5058 ^ _39627 : [(5059 ^ _39627) ^ [] : [-(in(_175719, _175721))], (5061 ^ _39627) ^ [] : [-(ordinal(_175719))]]], (5063 ^ _39627) ^ [_175964, _175966] : [-(in(_175964, 5053 ^ [_175966])), in(_175964, _175966), ordinal(_175964)], (5073 ^ _39627) ^ [_176273, _176275] : [ordinal(_176273), 5077 ^ _39627 : [(5078 ^ _39627) ^ [_176546] : [in(_176546, 5076 ^ [_176273, _176275]), 5081 ^ _39627 : [(5082 ^ _39627) ^ [] : [-(in(_176546, succ(_176273)))], (5085 ^ _39627) ^ [] : [-(ordinal(5083 ^ [_176273, _176275, _176546]))], (5087 ^ _39627) ^ [] : [-(_176546 = 5083 ^ [_176273, _176275, _176546])], (5089 ^ _39627) ^ [] : [-(in(5083 ^ [_176273, _176275, _176546], _176275))]]], (5091 ^ _39627) ^ [_177055] : [-(in(_177055, 5076 ^ [_176273, _176275])), in(_177055, succ(_176273)), 5096 ^ _39627 : [(5097 ^ _39627) ^ [_177258] : [ordinal(_177258), _177055 = _177258, in(_177258, _176275)]]]]], (5109 ^ _39627) ^ [_177651, _177653] : [-(empty(_177653)), relation(_177651), 5166 ^ _39627 : [(5167 ^ _39627) ^ [] : [-(relation(5165 ^ [_177651, _177653]))], (5169 ^ _39627) ^ [] : [-(function(5165 ^ [_177651, _177653]))], (5171 ^ _39627) ^ [] : [-(relation_dom(5165 ^ [_177651, _177653]) = _177653)], (5173 ^ _39627) ^ [_180741] : [in(_180741, _177653), 5177 ^ _39627 : [(5178 ^ _39627) ^ [] : [-(_180741 = 5176 ^ [_177651, _177653, _180741])], (5180 ^ _39627) ^ [] : [-(in(apply(5165 ^ [_177651, _177653], _180741), 5176 ^ [_177651, _177653, _180741]))], (5182 ^ _39627) ^ [_181185] : [in(_181185, 5176 ^ [_177651, _177653, _180741]), -(in(ordered_pair(apply(5165 ^ [_177651, _177653], _180741), _181185), _177651))]]]], 5150 ^ _39627 : [(5151 ^ _39627) ^ [] : [-(in(5149 ^ [_177651, _177653], _177653))], (5153 ^ _39627) ^ [_179927, _179929] : [5149 ^ [_177651, _177653] = _179927, in(_179929, _179927), 5161 ^ _39627 : [(5162 ^ _39627) ^ [] : [-(in(5160 ^ [_177651, _177653, _179927, _179929], _179927))], (5164 ^ _39627) ^ [] : [in(ordered_pair(_179929, 5160 ^ [_177651, _177653, _179927, _179929]), _177651)]]]], 5123 ^ _39627 : [(5148 ^ _39627) ^ [] : [5121 ^ [_177651, _177653] = 5122 ^ [_177651, _177653]], (5124 ^ _39627) ^ [] : [-(in(5120 ^ [_177651, _177653], _177653))], (5127 ^ _39627) ^ [] : [-(5120 ^ [_177651, _177653] = 5125 ^ [_177651, _177653])], (5129 ^ _39627) ^ [] : [-(in(5121 ^ [_177651, _177653], 5125 ^ [_177651, _177653]))], (5131 ^ _39627) ^ [_178980] : [in(_178980, 5125 ^ [_177651, _177653]), -(in(ordered_pair(5121 ^ [_177651, _177653], _178980), _177651))], (5138 ^ _39627) ^ [] : [-(5120 ^ [_177651, _177653] = 5136 ^ [_177651, _177653])], (5140 ^ _39627) ^ [] : [-(in(5122 ^ [_177651, _177653], 5136 ^ [_177651, _177653]))], (5142 ^ _39627) ^ [_179456] : [in(_179456, 5136 ^ [_177651, _177653]), -(in(ordered_pair(5122 ^ [_177651, _177653], _179456), _177651))]]], (5188 ^ _39627) ^ [_181469] : [5194 ^ _39627 : [(5195 ^ _39627) ^ [] : [-(in(5191 ^ [_181469], _181469))], (5197 ^ _39627) ^ [] : [-(5192 ^ [_181469] = singleton(5191 ^ [_181469]))], (5199 ^ _39627) ^ [] : [-(5193 ^ [_181469] = singleton(5191 ^ [_181469]))], (5201 ^ _39627) ^ [] : [5192 ^ [_181469] = 5193 ^ [_181469]]], 5203 ^ _39627 : [(5204 ^ _39627) ^ [] : [-(in(5202 ^ [_181469], _181469))], (5206 ^ _39627) ^ [_182323] : [_182323 = singleton(5202 ^ [_181469])]], 5208 ^ _39627 : [(5209 ^ _39627) ^ [] : [-(relation(5207 ^ [_181469]))], (5211 ^ _39627) ^ [] : [-(function(5207 ^ [_181469]))], (5213 ^ _39627) ^ [] : [-(relation_dom(5207 ^ [_181469]) = _181469)], (5215 ^ _39627) ^ [_182695] : [in(_182695, _181469), -(apply(5207 ^ [_181469], _182695) = singleton(_182695))]]], (5222 ^ _39627) ^ [_183004] : [-(relation(5220 ^ [_183004]))], (5224 ^ _39627) ^ [_183072] : [-(function(5220 ^ [_183072]))], (5226 ^ _39627) ^ [_183140] : [-(relation_dom(5220 ^ [_183140]) = _183140)], (5228 ^ _39627) ^ [_183220, _183222] : [in(_183220, _183222), -(apply(5220 ^ [_183222], _183220) = singleton(_183220))], (5234 ^ _39627) ^ [_183456, _183458] : [disjoint(_183458, _183456), -(disjoint(_183456, _183458))], (5240 ^ _39627) ^ [_183666, _183668] : [equipotent(_183668, _183666), -(equipotent(_183666, _183668))], (5246 ^ _39627) ^ [_183933, _183935, _183937, _183939] : [in(ordered_pair(_183939, _183937), cartesian_product2(_183935, _183933)), 5249 ^ _39627 : [(5250 ^ _39627) ^ [] : [-(in(_183939, _183935))], (5252 ^ _39627) ^ [] : [-(in(_183937, _183933))]]], (5254 ^ _39627) ^ [_184198, _184200, _184202, _184204] : [-(in(ordered_pair(_184204, _184202), cartesian_product2(_184200, _184198))), in(_184204, _184200), in(_184202, _184198)], (5264 ^ _39627) ^ [_184502] : [-(in(_184502, succ(_184502)))], (5266 ^ _39627) ^ [_184639, _184641, _184643, _184645] : [unordered_pair(_184645, _184643) = unordered_pair(_184641, _184639), -(_184645 = _184641), -(_184645 = _184639)], (5276 ^ _39627) ^ [_184989, _184991, _184993] : [relation(_184989), 5279 ^ _39627 : [(5280 ^ _39627) ^ [] : [in(_184993, relation_rng(relation_rng_restriction(_184991, _184989))), 5283 ^ _39627 : [(5284 ^ _39627) ^ [] : [-(in(_184993, _184991))], (5286 ^ _39627) ^ [] : [-(in(_184993, relation_rng(_184989)))]]], (5288 ^ _39627) ^ [] : [-(in(_184993, relation_rng(relation_rng_restriction(_184991, _184989)))), in(_184993, _184991), in(_184993, relation_rng(_184989))]]], (5298 ^ _39627) ^ [_185648, _185650] : [relation(_185648), -(subset(relation_rng(relation_rng_restriction(_185650, _185648)), _185650))], (5304 ^ _39627) ^ [_185866, _185868] : [relation(_185866), -(subset(relation_rng_restriction(_185868, _185866), _185866))], (5310 ^ _39627) ^ [_186080, _186082] : [relation(_186080), -(subset(relation_rng(relation_rng_restriction(_186082, _186080)), relation_rng(_186080)))], (5316 ^ _39627) ^ [_186316, _186318, _186320] : [subset(_186320, _186318), 5319 ^ _39627 : [(5320 ^ _39627) ^ [] : [-(subset(cartesian_product2(_186320, _186316), cartesian_product2(_186318, _186316)))], (5322 ^ _39627) ^ [] : [-(subset(cartesian_product2(_186316, _186320), cartesian_product2(_186316, _186318)))]]], (5324 ^ _39627) ^ [_186633, _186635] : [relation(_186633), -(relation_rng(relation_rng_restriction(_186635, _186633)) = set_intersection2(relation_rng(_186633), _186635))], (5330 ^ _39627) ^ [_186889, _186891, _186893, _186895] : [-(subset(cartesian_product2(_186895, _186891), cartesian_product2(_186893, _186889))), subset(_186895, _186893), subset(_186891, _186889)], (5340 ^ _39627) ^ [_187234, _187236, _187238] : [relation_of2_as_subset(_187234, _187238, _187236), 5343 ^ _39627 : [(5344 ^ _39627) ^ [] : [-(subset(relation_dom(_187234), _187238))], (5346 ^ _39627) ^ [] : [-(subset(relation_rng(_187234), _187236))]]], (5348 ^ _39627) ^ [_187537, _187539] : [subset(_187539, _187537), -(set_union2(_187539, _187537) = _187537)], (5355 ^ _39627) ^ [_187859] : [-(in(_187859, 5353 ^ [_187859]))], (5357 ^ _39627) ^ [_187971, _187973, _187975] : [-(in(_187971, 5353 ^ [_187975])), in(_187973, 5353 ^ [_187975]), subset(_187971, _187973)], (5367 ^ _39627) ^ [_188286, _188288] : [in(_188286, 5353 ^ [_188288]), -(in(powerset(_188286), 5353 ^ [_188288]))], (5373 ^ _39627) ^ [_188486, _188488] : [subset(_188486, 5353 ^ [_188488]), -(are_equipotent(_188486, 5353 ^ [_188488])), -(in(_188486, 5353 ^ [_188488]))], (5383 ^ _39627) ^ [_188840, _188842, _188844] : [relation(_188840), -(relation_dom_restriction(relation_rng_restriction(_188844, _188840), _188842) = relation_rng_restriction(_188844, relation_dom_restriction(_188840, _188842)))], (5389 ^ _39627) ^ [_189092, _189094, _189096] : [relation(_189092), 5392 ^ _39627 : [(5393 ^ _39627) ^ [] : [in(_189096, relation_image(_189092, _189094)), 5397 ^ _39627 : [(5398 ^ _39627) ^ [] : [-(in(5396 ^ [_189092, _189094, _189096], relation_dom(_189092)))], (5400 ^ _39627) ^ [] : [-(in(ordered_pair(5396 ^ [_189092, _189094, _189096], _189096), _189092))], (5402 ^ _39627) ^ [] : [-(in(5396 ^ [_189092, _189094, _189096], _189094))]]], (5404 ^ _39627) ^ [] : [-(in(_189096, relation_image(_189092, _189094))), 5405 ^ _39627 : [(5406 ^ _39627) ^ [_189693] : [in(_189693, relation_dom(_189092)), in(ordered_pair(_189693, _189096), _189092), in(_189693, _189094)]]]]], (5418 ^ _39627) ^ [_190090, _190092] : [relation(_190090), -(subset(relation_image(_190090, _190092), relation_rng(_190090)))], (5424 ^ _39627) ^ [_190308, _190310] : [-(subset(relation_image(_190308, relation_inverse_image(_190308, _190310)), _190310)), relation(_190308), function(_190308)], (5434 ^ _39627) ^ [_190615, _190617] : [relation(_190615), -(relation_image(_190615, _190617) = relation_image(_190615, set_intersection2(relation_dom(_190615), _190617)))], (5440 ^ _39627) ^ [_190845, _190847] : [relation(_190845), subset(_190847, relation_dom(_190845)), -(subset(_190847, relation_inverse_image(_190845, relation_image(_190845, _190847))))], (5450 ^ _39627) ^ [_191144] : [relation(_191144), -(relation_image(_191144, relation_dom(_191144)) = relation_rng(_191144))], (5456 ^ _39627) ^ [_191360, _191362] : [relation(_191360), function(_191360), subset(_191362, relation_rng(_191360)), -(relation_image(_191360, relation_inverse_image(_191360, _191362)) = _191362)], (5470 ^ _39627) ^ [_191790, _191792, _191794, _191796] : [relation_of2_as_subset(_191790, _191792, _191796), subset(relation_rng(_191790), _191794), -(relation_of2_as_subset(_191790, _191792, _191794))], (5480 ^ _39627) ^ [_192103] : [relation(_192103), 5483 ^ _39627 : [(5484 ^ _39627) ^ [_192243] : [relation(_192243), -(relation_rng(relation_composition(_192103, _192243)) = relation_image(_192243, relation_rng(_192103)))]]], (5490 ^ _39627) ^ [_192492, _192494, _192496] : [relation(_192492), 5493 ^ _39627 : [(5494 ^ _39627) ^ [] : [in(_192496, relation_inverse_image(_192492, _192494)), 5498 ^ _39627 : [(5499 ^ _39627) ^ [] : [-(in(5497 ^ [_192492, _192494, _192496], relation_rng(_192492)))], (5501 ^ _39627) ^ [] : [-(in(ordered_pair(_192496, 5497 ^ [_192492, _192494, _192496]), _192492))], (5503 ^ _39627) ^ [] : [-(in(5497 ^ [_192492, _192494, _192496], _192494))]]], (5505 ^ _39627) ^ [] : [-(in(_192496, relation_inverse_image(_192492, _192494))), 5506 ^ _39627 : [(5507 ^ _39627) ^ [_193093] : [in(_193093, relation_rng(_192492)), in(ordered_pair(_192496, _193093), _192492), in(_193093, _192494)]]]]], (5519 ^ _39627) ^ [_193490, _193492] : [relation(_193490), -(subset(relation_inverse_image(_193490, _193492), relation_dom(_193490)))], (5525 ^ _39627) ^ [_193736, _193738, _193740, _193742] : [relation_of2_as_subset(_193736, _193738, _193742), subset(_193742, _193740), -(relation_of2_as_subset(_193736, _193738, _193740))], (5535 ^ _39627) ^ [_194073, _194075, _194077] : [relation(_194073), 5538 ^ _39627 : [(5539 ^ _39627) ^ [] : [in(_194077, relation_restriction(_194073, _194075)), 5542 ^ _39627 : [(5543 ^ _39627) ^ [] : [-(in(_194077, _194073))], (5545 ^ _39627) ^ [] : [-(in(_194077, cartesian_product2(_194075, _194075)))]]], (5547 ^ _39627) ^ [] : [-(in(_194077, relation_restriction(_194073, _194075))), in(_194077, _194073), in(_194077, cartesian_product2(_194075, _194075))]]], (5557 ^ _39627) ^ [_194729, _194731] : [relation(_194729), -(_194731 = empty_set), subset(_194731, relation_rng(_194729)), relation_inverse_image(_194729, _194731) = empty_set], (5571 ^ _39627) ^ [_195143, _195145, _195147] : [relation(_195143), subset(_195147, _195145), -(subset(relation_inverse_image(_195143, _195147), relation_inverse_image(_195143, _195145)))], (5581 ^ _39627) ^ [_195462, _195464] : [relation(_195462), -(relation_restriction(_195462, _195464) = relation_dom_restriction(relation_rng_restriction(_195464, _195462), _195464))], (5587 ^ _39627) ^ [_195673, _195675] : [-(subset(set_intersection2(_195675, _195673), _195675))], (5589 ^ _39627) ^ [_195785, _195787] : [relation(_195785), -(relation_restriction(_195785, _195787) = relation_rng_restriction(_195787, relation_dom_restriction(_195785, _195787)))], (5595 ^ _39627) ^ [_196025, _196027, _196029] : [relation(_196025), in(_196029, relation_field(relation_restriction(_196025, _196027))), 5602 ^ _39627 : [(5603 ^ _39627) ^ [] : [-(in(_196029, relation_field(_196025)))], (5605 ^ _39627) ^ [] : [-(in(_196029, _196027))]]], (5607 ^ _39627) ^ [_196437, _196439, _196441] : [-(subset(_196441, set_intersection2(_196439, _196437))), subset(_196441, _196439), subset(_196441, _196437)], (5617 ^ _39627) ^ [_196723] : [-(set_union2(_196723, empty_set) = _196723)], (5619 ^ _39627) ^ [_196833, _196835] : [in(_196835, _196833), -(element(_196835, _196833))], (5625 ^ _39627) ^ [_197057, _197059, _197061] : [-(subset(_197061, _197057)), subset(_197061, _197059), subset(_197059, _197057)], (5635 ^ _39627) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (5637 ^ _39627) ^ [_197433, _197435, _197437] : [relation(_197433), in(ordered_pair(_197437, _197435), _197433), 5644 ^ _39627 : [(5645 ^ _39627) ^ [] : [-(in(_197437, relation_dom(_197433)))], (5647 ^ _39627) ^ [] : [-(in(_197435, relation_rng(_197433)))]]], (5649 ^ _39627) ^ [_197831, _197833] : [relation(_197831), 5652 ^ _39627 : [(5653 ^ _39627) ^ [] : [-(subset(relation_field(relation_restriction(_197831, _197833)), relation_field(_197831)))], (5655 ^ _39627) ^ [] : [-(subset(relation_field(relation_restriction(_197831, _197833)), _197833))]]], (5657 ^ _39627) ^ [_198138, _198140] : [relation(_198138), function(_198138), 5664 ^ _39627 : [(5665 ^ _39627) ^ [_198388] : [relation(_198388), function(_198388), 5672 ^ _39627 : [(5673 ^ _39627) ^ [] : [in(_198140, relation_dom(relation_composition(_198388, _198138))), 5676 ^ _39627 : [(5677 ^ _39627) ^ [] : [-(in(_198140, relation_dom(_198388)))], (5679 ^ _39627) ^ [] : [-(in(apply(_198388, _198140), relation_dom(_198138)))]]], (5681 ^ _39627) ^ [] : [-(in(_198140, relation_dom(relation_composition(_198388, _198138)))), in(_198140, relation_dom(_198388)), in(apply(_198388, _198140), relation_dom(_198138))]]]]], (5691 ^ _39627) ^ [_199194, _199196, _199198, _199200] : [function(_199194), quasi_total(_199194, _199200, _199198), relation_of2_as_subset(_199194, _199200, _199198), 5702 ^ _39627 : [(5703 ^ _39627) ^ [_199563] : [relation(_199563), function(_199563), in(_199196, _199200), -(_199198 = empty_set), -(apply(relation_composition(_199194, _199563), _199196) = apply(_199563, apply(_199194, _199196)))]]], (5721 ^ _39627) ^ [_200120] : [epsilon_transitive(_200120), 5724 ^ _39627 : [(5725 ^ _39627) ^ [_200256] : [ordinal(_200256), proper_subset(_200120, _200256), -(in(_200120, _200256))]]], (5735 ^ _39627) ^ [_200546] : [relation(_200546), -(subset(_200546, cartesian_product2(relation_dom(_200546), relation_rng(_200546))))], (5741 ^ _39627) ^ [_200776, _200778, _200780] : [relation(_200776), -(subset(fiber(relation_restriction(_200776, _200780), _200778), fiber(_200776, _200778)))], (5747 ^ _39627) ^ [_201008, _201010] : [relation(_201008), function(_201008), 5754 ^ _39627 : [(5755 ^ _39627) ^ [_201257] : [relation(_201257), function(_201257), in(_201010, relation_dom(relation_composition(_201257, _201008))), -(apply(relation_composition(_201257, _201008), _201010) = apply(_201008, apply(_201257, _201010)))]]], (5769 ^ _39627) ^ [_201716, _201718, _201720] : [relation_of2_as_subset(_201716, _201718, _201720), 5772 ^ _39627 : [(5773 ^ _39627) ^ [] : [5775 ^ _39627 : [(5776 ^ _39627) ^ [] : [-(in(5774 ^ [_201716, _201718, _201720], _201718))], (5778 ^ _39627) ^ [_202074] : [in(ordered_pair(5774 ^ [_201716, _201718, _201720], _202074), _201716)]], -(relation_dom_as_subset(_201718, _201720, _201716) = _201718)], (5782 ^ _39627) ^ [] : [relation_dom_as_subset(_201718, _201720, _201716) = _201718, 5785 ^ _39627 : [(5786 ^ _39627) ^ [_202311] : [in(_202311, _201718), -(in(ordered_pair(_202311, 5789 ^ [_201716, _201718, _201720, _202311]), _201716))]]]]], (5793 ^ _39627) ^ [_202633, _202635] : [relation(_202633), reflexive(_202633), -(reflexive(relation_restriction(_202633, _202635)))], (5803 ^ _39627) ^ [_202932, _202934] : [relation(_202932), function(_202932), 5810 ^ _39627 : [(5811 ^ _39627) ^ [_203178] : [relation(_203178), function(_203178), in(_202934, relation_dom(_202932)), -(apply(relation_composition(_202932, _203178), _202934) = apply(_203178, apply(_202932, _202934)))]]], (5825 ^ _39627) ^ [_203617, _203619] : [ordinal(_203617), in(_203619, _203617), -(ordinal(_203619))], (5835 ^ _39627) ^ [_203926, _203928, _203930] : [relation_of2_as_subset(_203926, _203930, _203928), 5838 ^ _39627 : [(5839 ^ _39627) ^ [] : [5841 ^ _39627 : [(5842 ^ _39627) ^ [] : [-(in(5840 ^ [_203926, _203928, _203930], _203928))], (5844 ^ _39627) ^ [_204284] : [in(ordered_pair(_204284, 5840 ^ [_203926, _203928, _203930]), _203926)]], -(relation_rng_as_subset(_203930, _203928, _203926) = _203928)], (5848 ^ _39627) ^ [] : [relation_rng_as_subset(_203930, _203928, _203926) = _203928, 5851 ^ _39627 : [(5852 ^ _39627) ^ [_204521] : [in(_204521, _203928), -(in(ordered_pair(5855 ^ [_203926, _203928, _203930, _204521], _204521), _203926))]]]]], (5859 ^ _39627) ^ [_204843, _204845] : [relation(_204843), connected(_204843), -(connected(relation_restriction(_204843, _204845)))], (5869 ^ _39627) ^ [_205128] : [ordinal(_205128), 5872 ^ _39627 : [(5873 ^ _39627) ^ [_205278] : [ordinal(_205278), -(in(_205128, _205278)), -(_205128 = _205278), -(in(_205278, _205128))]]], (5887 ^ _39627) ^ [_205681, _205683] : [relation(_205681), transitive(_205681), -(transitive(relation_restriction(_205681, _205683)))], (5897 ^ _39627) ^ [_205966] : [relation(_205966), 5900 ^ _39627 : [(5901 ^ _39627) ^ [_206116] : [relation(_206116), subset(_205966, _206116), 5908 ^ _39627 : [(5909 ^ _39627) ^ [] : [-(subset(relation_dom(_205966), relation_dom(_206116)))], (5911 ^ _39627) ^ [] : [-(subset(relation_rng(_205966), relation_rng(_206116)))]]]]], (5913 ^ _39627) ^ [_206511, _206513] : [relation(_206511), antisymmetric(_206511), -(antisymmetric(relation_restriction(_206511, _206513)))], (5923 ^ _39627) ^ [_206810, _206812] : [relation(_206810), well_orders(_206810, _206812), 5930 ^ _39627 : [(5931 ^ _39627) ^ [] : [-(relation_field(relation_restriction(_206810, _206812)) = _206812)], (5933 ^ _39627) ^ [] : [-(well_ordering(relation_restriction(_206810, _206812)))]]], (5936 ^ _39627) ^ [_207231] : [-(relation(5934 ^ [_207231]))], (5938 ^ _39627) ^ [_207279] : [-(well_orders(5934 ^ [_207279], _207279))], (5940 ^ _39627) ^ [_207407, _207409, _207411] : [subset(_207411, _207409), -(subset(set_intersection2(_207411, _207407), set_intersection2(_207409, _207407)))], (5946 ^ _39627) ^ [_207621] : [-(empty(_207621)), 5952 ^ _39627 : [(5953 ^ _39627) ^ [] : [-(in(5951 ^ [_207621], _207621))], (5955 ^ _39627) ^ [] : [-(5951 ^ [_207621] = empty_set)]], 5957 ^ _39627 : [(5958 ^ _39627) ^ [] : [-(relation(5956 ^ [_207621]))], (5960 ^ _39627) ^ [] : [-(function(5956 ^ [_207621]))], (5962 ^ _39627) ^ [] : [-(relation_dom(5956 ^ [_207621]) = _207621)], (5964 ^ _39627) ^ [_208289] : [in(_208289, _207621), -(in(apply(5956 ^ [_207621], _208289), _208289))]]], (5970 ^ _39627) ^ [_208533, _208535] : [subset(_208535, _208533), -(set_intersection2(_208535, _208533) = _208535)], (5976 ^ _39627) ^ [_208720] : [-(set_intersection2(_208720, empty_set) = empty_set)], (5978 ^ _39627) ^ [_208830, _208832] : [element(_208832, _208830), -(empty(_208830)), -(in(_208832, _208830))], (5988 ^ _39627) ^ [_209128, _209130] : [-(_209130 = _209128), 5992 ^ _39627 : [(5993 ^ _39627) ^ [] : [-(in(5989 ^ [_209128, _209130], _209130))], (5995 ^ _39627) ^ [] : [in(5989 ^ [_209128, _209130], _209128)]], 5996 ^ _39627 : [(5997 ^ _39627) ^ [] : [-(in(5989 ^ [_209128, _209130], _209128))], (5999 ^ _39627) ^ [] : [in(5989 ^ [_209128, _209130], _209130)]]], (6003 ^ _39627) ^ [_209629] : [-(reflexive(inclusion_relation(_209629)))], (6005 ^ _39627) ^ [_209708] : [-(subset(empty_set, _209708))], (6007 ^ _39627) ^ [_209829, _209831, _209833] : [relation(_209829), in(ordered_pair(_209833, _209831), _209829), 6014 ^ _39627 : [(6015 ^ _39627) ^ [] : [-(in(_209833, relation_field(_209829)))], (6017 ^ _39627) ^ [] : [-(in(_209831, relation_field(_209829)))]]], (6019 ^ _39627) ^ [_210213] : [-(ordinal(_210213)), 6021 ^ _39627 : [(6022 ^ _39627) ^ [] : [-(in(6020 ^ [_210213], _210213))], (6024 ^ _39627) ^ [] : [ordinal(6020 ^ [_210213]), subset(6020 ^ [_210213], _210213)]]], (6032 ^ _39627) ^ [_210643, _210645] : [relation(_210643), well_founded_relation(_210643), -(well_founded_relation(relation_restriction(_210643, _210645)))], (6042 ^ _39627) ^ [_210942, _210944] : [ordinal(_210942), subset(_210944, _210942), -(_210944 = empty_set), 6054 ^ _39627 : [(6055 ^ _39627) ^ [] : [-(ordinal(6053 ^ [_210942, _210944]))], (6057 ^ _39627) ^ [] : [-(in(6053 ^ [_210942, _210944], _210944))], (6059 ^ _39627) ^ [_211494] : [ordinal(_211494), in(_211494, _210944), -(ordinal_subset(6053 ^ [_210942, _210944], _211494))]]], (6069 ^ _39627) ^ [_211836, _211838] : [relation(_211836), well_ordering(_211836), -(well_ordering(relation_restriction(_211836, _211838)))], (6079 ^ _39627) ^ [_212121] : [ordinal(_212121), 6082 ^ _39627 : [(6083 ^ _39627) ^ [_212259] : [ordinal(_212259), 6086 ^ _39627 : [(6087 ^ _39627) ^ [] : [in(_212121, _212259), -(ordinal_subset(succ(_212121), _212259))], (6093 ^ _39627) ^ [] : [ordinal_subset(succ(_212121), _212259), -(in(_212121, _212259))]]]]], (6099 ^ _39627) ^ [_212744, _212746, _212748] : [subset(_212748, _212746), -(subset(set_difference(_212748, _212744), set_difference(_212746, _212744)))], (6105 ^ _39627) ^ [_213000, _213002, _213004, _213006] : [ordered_pair(_213006, _213004) = ordered_pair(_213002, _213000), 6108 ^ _39627 : [(6109 ^ _39627) ^ [] : [-(_213006 = _213002)], (6111 ^ _39627) ^ [] : [-(_213004 = _213000)]]], (6113 ^ _39627) ^ [_213313, _213315] : [relation(_213313), function(_213313), 6120 ^ _39627 : [(6121 ^ _39627) ^ [] : [_213313 = identity_relation(_213315), 6124 ^ _39627 : [(6125 ^ _39627) ^ [] : [-(relation_dom(_213313) = _213315)], (6127 ^ _39627) ^ [_213732] : [in(_213732, _213315), -(apply(_213313, _213732) = _213732)]]], (6133 ^ _39627) ^ [] : [-(_213313 = identity_relation(_213315)), relation_dom(_213313) = _213315, 6139 ^ _39627 : [(6140 ^ _39627) ^ [] : [-(in(6138 ^ [_213313, _213315], _213315))], (6142 ^ _39627) ^ [] : [apply(_213313, 6138 ^ [_213313, _213315]) = 6138 ^ [_213313, _213315]]]]]], (6146 ^ _39627) ^ [_214337, _214339] : [in(_214337, _214339), -(apply(identity_relation(_214339), _214337) = _214337)], (6152 ^ _39627) ^ [_214542, _214544] : [-(subset(set_difference(_214544, _214542), _214544))], (6154 ^ _39627) ^ [_214640] : [relation(_214640), 6157 ^ _39627 : [(6158 ^ _39627) ^ [] : [-(relation_rng(_214640) = relation_dom(relation_inverse(_214640)))], (6160 ^ _39627) ^ [] : [-(relation_dom(_214640) = relation_rng(relation_inverse(_214640)))]]], (6162 ^ _39627) ^ [_214968, _214970] : [set_difference(_214970, _214968) = empty_set, -(subset(_214970, _214968))], (6168 ^ _39627) ^ [_215136, _215138] : [subset(_215138, _215136), -(set_difference(_215138, _215136) = empty_set)], (6174 ^ _39627) ^ [_215383, _215385] : [subset(singleton(_215385), _215383), -(in(_215385, _215383))], (6180 ^ _39627) ^ [_215549, _215551] : [in(_215551, _215549), -(subset(singleton(_215551), _215549))], (6186 ^ _39627) ^ [_215808, _215810, _215812] : [subset(unordered_pair(_215812, _215810), _215808), 6189 ^ _39627 : [(6190 ^ _39627) ^ [] : [-(in(_215812, _215808))], (6192 ^ _39627) ^ [] : [-(in(_215810, _215808))]]], (6194 ^ _39627) ^ [_216059, _216061, _216063] : [-(subset(unordered_pair(_216063, _216061), _216059)), in(_216063, _216059), in(_216061, _216059)], (6204 ^ _39627) ^ [_216376, _216378] : [relation(_216376), -(relation_field(relation_restriction(_216376, _216378)) = _216378), well_ordering(_216376), subset(_216378, relation_field(_216376))], (6218 ^ _39627) ^ [_216759, _216761] : [-(set_union2(_216761, set_difference(_216759, _216761)) = set_union2(_216761, _216759))], (6230 ^ _39627) ^ [_217166, _217168] : [6231 ^ _39627 : [(6232 ^ _39627) ^ [] : [_217168 = empty_set], (6234 ^ _39627) ^ [] : [_217168 = singleton(_217166)]], -(subset(_217168, singleton(_217166)))], (6220 ^ _39627) ^ [_216906, _216908] : [subset(_216908, singleton(_216906)), -(_216908 = empty_set), -(_216908 = singleton(_216906))], (6238 ^ _39627) ^ [_217431] : [-(set_difference(_217431, empty_set) = _217431)], (6240 ^ _39627) ^ [_217555, _217557, _217559] : [in(_217559, _217557), in(_217557, _217555), in(_217555, _217559)], (6250 ^ _39627) ^ [_217892, _217894] : [element(_217894, powerset(_217892)), -(subset(_217894, _217892))], (6256 ^ _39627) ^ [_218058, _218060] : [subset(_218060, _218058), -(element(_218060, powerset(_218058)))], (6262 ^ _39627) ^ [_218245] : [-(transitive(inclusion_relation(_218245)))], (6264 ^ _39627) ^ [_218373, _218375] : [-(disjoint(_218375, _218373)), 6268 ^ _39627 : [(6269 ^ _39627) ^ [] : [-(in(6267 ^ [_218373, _218375], _218375))], (6271 ^ _39627) ^ [] : [-(in(6267 ^ [_218373, _218375], _218373))]]], (6273 ^ _39627) ^ [_218687, _218689] : [disjoint(_218689, _218687), 6274 ^ _39627 : [(6275 ^ _39627) ^ [_218779] : [in(_218779, _218689), in(_218779, _218687)]]], (6283 ^ _39627) ^ [_219036] : [subset(_219036, empty_set), -(_219036 = empty_set)], (6289 ^ _39627) ^ [_219225, _219227] : [-(set_difference(set_union2(_219227, _219225), _219225) = set_difference(_219227, _219225))], (6291 ^ _39627) ^ [_219329] : [ordinal(_219329), 6294 ^ _39627 : [(6309 ^ _39627) ^ [] : [6311 ^ _39627 : [(6312 ^ _39627) ^ [] : [-(ordinal(6310 ^ [_219329]))], (6314 ^ _39627) ^ [] : [-(in(6310 ^ [_219329], _219329))], (6316 ^ _39627) ^ [] : [in(succ(6310 ^ [_219329]), _219329)]], -(being_limit_ordinal(_219329))], (6295 ^ _39627) ^ [] : [being_limit_ordinal(_219329), 6298 ^ _39627 : [(6299 ^ _39627) ^ [_219575] : [ordinal(_219575), in(_219575, _219329), -(in(succ(_219575), _219329))]]]]], (6320 ^ _39627) ^ [_220201] : [ordinal(_220201), 6323 ^ _39627 : [(6324 ^ _39627) ^ [] : [-(being_limit_ordinal(_220201)), 6328 ^ _39627 : [(6329 ^ _39627) ^ [] : [-(ordinal(6327 ^ [_220201]))], (6331 ^ _39627) ^ [] : [-(_220201 = succ(6327 ^ [_220201]))]]], (6333 ^ _39627) ^ [] : [being_limit_ordinal(_220201), 6334 ^ _39627 : [(6335 ^ _39627) ^ [_220672] : [ordinal(_220672), _220201 = succ(_220672)]]]]], (6343 ^ _39627) ^ [_220939, _220941] : [element(_220939, powerset(_220941)), 6346 ^ _39627 : [(6347 ^ _39627) ^ [_221091] : [element(_221091, powerset(_220941)), 6350 ^ _39627 : [(6351 ^ _39627) ^ [] : [disjoint(_220939, _221091), -(subset(_220939, subset_complement(_220941, _221091)))], (6357 ^ _39627) ^ [] : [subset(_220939, subset_complement(_220941, _221091)), -(disjoint(_220939, _221091))]]]]], (6363 ^ _39627) ^ [_221575] : [relation(_221575), 6366 ^ _39627 : [(6367 ^ _39627) ^ [_221712] : [relation(_221712), -(subset(relation_dom(relation_composition(_221575, _221712)), relation_dom(_221575)))]]], (6373 ^ _39627) ^ [_221927] : [relation(_221927), 6376 ^ _39627 : [(6377 ^ _39627) ^ [_222064] : [relation(_222064), -(subset(relation_rng(relation_composition(_221927, _222064)), relation_rng(_222064)))]]], (6383 ^ _39627) ^ [_222293, _222295] : [subset(_222295, _222293), -(_222293 = set_union2(_222295, set_difference(_222293, _222295)))], (6389 ^ _39627) ^ [_222543, _222545, _222547, _222549] : [function(_222543), quasi_total(_222543, _222549, _222547), relation_of2_as_subset(_222543, _222549, _222547), -(_222547 = empty_set), 6404 ^ _39627 : [(6405 ^ _39627) ^ [_223021] : [in(_223021, relation_inverse_image(_222543, _222545)), 6408 ^ _39627 : [(6409 ^ _39627) ^ [] : [-(in(_223021, _222549))], (6411 ^ _39627) ^ [] : [-(in(apply(_222543, _223021), _222545))]]], (6413 ^ _39627) ^ [_223302] : [-(in(_223302, relation_inverse_image(_222543, _222545))), in(_223302, _222549), in(apply(_222543, _223302), _222545)]]], (6423 ^ _39627) ^ [_223652] : [relation(_223652), 6426 ^ _39627 : [(6427 ^ _39627) ^ [_223799] : [relation(_223799), subset(relation_rng(_223652), relation_dom(_223799)), -(relation_dom(relation_composition(_223652, _223799)) = relation_dom(_223652))]]], (6437 ^ _39627) ^ [_224125, _224127] : [element(_224125, powerset(powerset(_224127))), -(_224125 = empty_set), complements_of_subsets(_224127, _224125) = empty_set], (6447 ^ _39627) ^ [_224442, _224444] : [in(_224444, _224442), -(set_union2(singleton(_224444), _224442) = _224442)], (6453 ^ _39627) ^ [_224648] : [relation(_224648), 6456 ^ _39627 : [(6457 ^ _39627) ^ [_224795] : [relation(_224795), subset(relation_dom(_224648), relation_rng(_224795)), -(relation_rng(relation_composition(_224795, _224648)) = relation_rng(_224648))]]], (6467 ^ _39627) ^ [_225121, _225123] : [element(_225121, powerset(powerset(_225123))), -(_225121 = empty_set), -(subset_difference(_225123, cast_to_subset(_225123), union_of_subsets(_225123, _225121)) = meet_of_subsets(_225123, complements_of_subsets(_225123, _225121)))], (6477 ^ _39627) ^ [_225461, _225463] : [element(_225461, powerset(powerset(_225463))), -(_225461 = empty_set), -(union_of_subsets(_225463, complements_of_subsets(_225463, _225461)) = subset_difference(_225463, cast_to_subset(_225463), meet_of_subsets(_225463, _225461)))], (6487 ^ _39627) ^ [_225786, _225788] : [-(set_difference(_225788, set_difference(_225788, _225786)) = set_intersection2(_225788, _225786))], (6489 ^ _39627) ^ [_225890] : [relation(_225890), 6492 ^ _39627 : [(6493 ^ _39627) ^ [_226045] : [relation(_226045), 6496 ^ _39627 : [(6497 ^ _39627) ^ [_226196] : [relation(_226196), function(_226196), relation_isomorphism(_225890, _226045, _226196), -(relation_isomorphism(_226045, _225890, function_inverse(_226196)))]]]]], (6511 ^ _39627) ^ [_226589] : [-(set_difference(empty_set, _226589) = empty_set)], (6513 ^ _39627) ^ [_226713, _226715, _226717] : [-(element(_226717, _226713)), in(_226717, _226715), element(_226715, powerset(_226713))], (6523 ^ _39627) ^ [_227012] : [ordinal(_227012), -(connected(inclusion_relation(_227012)))], (6529 ^ _39627) ^ [_227236, _227238] : [-(disjoint(_227238, _227236)), -(in(6532 ^ [_227236, _227238], set_intersection2(_227238, _227236)))], (6536 ^ _39627) ^ [_227471, _227473] : [6537 ^ _39627 : [(6538 ^ _39627) ^ [_227544] : [in(_227544, set_intersection2(_227473, _227471))]], disjoint(_227473, _227471)], (6542 ^ _39627) ^ [_227696] : [-(_227696 = empty_set), 6545 ^ _39627 : [(6546 ^ _39627) ^ [_227856] : [element(_227856, powerset(_227696)), 6549 ^ _39627 : [(6550 ^ _39627) ^ [_228010] : [element(_228010, _227696), -(in(_228010, _227856)), -(in(_228010, subset_complement(_227696, _227856)))]]]]], (6560 ^ _39627) ^ [_228328] : [relation(_228328), 6563 ^ _39627 : [(6564 ^ _39627) ^ [_228524] : [relation(_228524), 6567 ^ _39627 : [(6568 ^ _39627) ^ [_228716] : [relation(_228716), function(_228716), relation_isomorphism(_228328, _228524, _228716), 6579 ^ _39627 : [(6580 ^ _39627) ^ [] : [reflexive(_228328), -(reflexive(_228524))], (6586 ^ _39627) ^ [] : [transitive(_228328), -(transitive(_228524))], (6592 ^ _39627) ^ [] : [connected(_228328), -(connected(_228524))], (6598 ^ _39627) ^ [] : [antisymmetric(_228328), -(antisymmetric(_228524))], (6604 ^ _39627) ^ [] : [well_founded_relation(_228328), -(well_founded_relation(_228524))]]]]]]], (6610 ^ _39627) ^ [_229868] : [relation(_229868), function(_229868), one_to_one(_229868), 6621 ^ _39627 : [(6622 ^ _39627) ^ [_230255] : [relation(_230255), function(_230255), 6629 ^ _39627 : [(6660 ^ _39627) ^ [] : [-(_230255 = function_inverse(_229868)), relation_dom(_230255) = relation_rng(_229868), 6669 ^ _39627 : [(6670 ^ _39627) ^ [] : [-(in(6665 ^ [_229868, _230255], relation_rng(_229868)))], (6672 ^ _39627) ^ [] : [-(6666 ^ [_229868, _230255] = apply(_230255, 6665 ^ [_229868, _230255]))], (6674 ^ _39627) ^ [] : [in(6666 ^ [_229868, _230255], relation_dom(_229868)), 6665 ^ [_229868, _230255] = apply(_229868, 6666 ^ [_229868, _230255])]], 6679 ^ _39627 : [(6680 ^ _39627) ^ [] : [-(in(6666 ^ [_229868, _230255], relation_dom(_229868)))], (6682 ^ _39627) ^ [] : [-(6665 ^ [_229868, _230255] = apply(_229868, 6666 ^ [_229868, _230255]))], (6684 ^ _39627) ^ [] : [in(6665 ^ [_229868, _230255], relation_rng(_229868)), 6666 ^ [_229868, _230255] = apply(_230255, 6665 ^ [_229868, _230255])]]], (6630 ^ _39627) ^ [] : [_230255 = function_inverse(_229868), 6633 ^ _39627 : [(6634 ^ _39627) ^ [] : [-(relation_dom(_230255) = relation_rng(_229868))], (6636 ^ _39627) ^ [_230772, _230774] : [6643 ^ _39627 : [(6644 ^ _39627) ^ [] : [-(in(_230772, relation_dom(_229868)))], (6646 ^ _39627) ^ [] : [-(_230774 = apply(_229868, _230772))]], in(_230774, relation_rng(_229868)), _230772 = apply(_230255, _230774)], (6648 ^ _39627) ^ [_231146, _231148] : [6655 ^ _39627 : [(6656 ^ _39627) ^ [] : [-(in(_231148, relation_rng(_229868)))], (6658 ^ _39627) ^ [] : [-(_231146 = apply(_230255, _231148))]], in(_231146, relation_dom(_229868)), _231148 = apply(_229868, _231146)]]]]]]], (6692 ^ _39627) ^ [_232721, _232723, _232725] : [element(_232721, powerset(_232725)), in(_232723, subset_complement(_232725, _232721)), in(_232723, _232721)], (6702 ^ _39627) ^ [_233027] : [relation(_233027), 6705 ^ _39627 : [(6706 ^ _39627) ^ [_233183] : [relation(_233183), 6709 ^ _39627 : [(6710 ^ _39627) ^ [_233335] : [relation(_233335), function(_233335), -(well_ordering(_233183)), well_ordering(_233027), relation_isomorphism(_233027, _233183, _233335)]]]]], (6728 ^ _39627) ^ [_233826] : [relation(_233826), function(_233826), one_to_one(_233826), 6739 ^ _39627 : [(6740 ^ _39627) ^ [] : [-(relation_rng(_233826) = relation_dom(function_inverse(_233826)))], (6742 ^ _39627) ^ [] : [-(relation_dom(_233826) = relation_rng(function_inverse(_233826)))]]], (6744 ^ _39627) ^ [_234279] : [relation(_234279), -(in(ordered_pair(6749 ^ [_234279], 6750 ^ [_234279]), _234279)), -(_234279 = empty_set)], (6756 ^ _39627) ^ [_234697, _234699] : [relation(_234697), function(_234697), 6771 ^ _39627 : [(6772 ^ _39627) ^ [] : [-(_234699 = apply(_234697, apply(function_inverse(_234697), _234699)))], (6774 ^ _39627) ^ [] : [-(_234699 = apply(relation_composition(function_inverse(_234697), _234697), _234699))]], one_to_one(_234697), in(_234699, relation_rng(_234697))], (6776 ^ _39627) ^ [_235295, _235297, _235299] : [in(_235299, _235297), element(_235297, powerset(_235295)), empty(_235295)], (6786 ^ _39627) ^ [_235591] : [relation(_235591), 6789 ^ _39627 : [(6790 ^ _39627) ^ [] : [well_founded_relation(_235591), -(is_well_founded_in(_235591, relation_field(_235591)))], (6796 ^ _39627) ^ [] : [is_well_founded_in(_235591, relation_field(_235591)), -(well_founded_relation(_235591))]]], (6802 ^ _39627) ^ [_236007] : [-(antisymmetric(inclusion_relation(_236007)))], (6804 ^ _39627) ^ [] : [-(relation_dom(empty_set) = empty_set)], (6806 ^ _39627) ^ [] : [-(relation_rng(empty_set) = empty_set)], (6808 ^ _39627) ^ [_236223, _236225] : [subset(_236225, _236223), proper_subset(_236223, _236225)], (6814 ^ _39627) ^ [_236418] : [relation(_236418), function(_236418), one_to_one(_236418), -(one_to_one(function_inverse(_236418)))], (6828 ^ _39627) ^ [_236804, _236806, _236808] : [-(disjoint(_236808, _236804)), subset(_236808, _236806), disjoint(_236806, _236804)], (6838 ^ _39627) ^ [_237099] : [relation(_237099), 6843 ^ _39627 : [(6844 ^ _39627) ^ [] : [relation_dom(_237099) = empty_set], (6846 ^ _39627) ^ [] : [relation_rng(_237099) = empty_set]], -(_237099 = empty_set)], (6850 ^ _39627) ^ [_237452] : [relation(_237452), 6853 ^ _39627 : [(6854 ^ _39627) ^ [] : [relation_dom(_237452) = empty_set, -(relation_rng(_237452) = empty_set)], (6860 ^ _39627) ^ [] : [relation_rng(_237452) = empty_set, -(relation_dom(_237452) = empty_set)]]], (6866 ^ _39627) ^ [_237935, _237937] : [set_difference(_237937, singleton(_237935)) = _237937, in(_237935, _237937)], (6872 ^ _39627) ^ [_238108, _238110] : [-(in(_238108, _238110)), -(set_difference(_238110, singleton(_238108)) = _238110)], (6878 ^ _39627) ^ [_238333, _238335] : [relation(_238333), function(_238333), 6885 ^ _39627 : [(6886 ^ _39627) ^ [_238600] : [relation(_238600), function(_238600), 6893 ^ _39627 : [(6894 ^ _39627) ^ [] : [_238333 = relation_dom_restriction(_238600, _238335), 6897 ^ _39627 : [(6898 ^ _39627) ^ [] : [-(relation_dom(_238333) = set_intersection2(relation_dom(_238600), _238335))], (6900 ^ _39627) ^ [_239054] : [in(_239054, relation_dom(_238333)), -(apply(_238333, _239054) = apply(_238600, _239054))]]], (6906 ^ _39627) ^ [] : [-(_238333 = relation_dom_restriction(_238600, _238335)), relation_dom(_238333) = set_intersection2(relation_dom(_238600), _238335), 6912 ^ _39627 : [(6913 ^ _39627) ^ [] : [-(in(6911 ^ [_238333, _238335, _238600], relation_dom(_238333)))], (6915 ^ _39627) ^ [] : [apply(_238333, 6911 ^ [_238333, _238335, _238600]) = apply(_238600, 6911 ^ [_238333, _238335, _238600])]]]]]]], (6919 ^ _39627) ^ [_239693] : [-(unordered_pair(_239693, _239693) = singleton(_239693))], (6921 ^ _39627) ^ [_239791] : [empty(_239791), -(_239791 = empty_set)], (6927 ^ _39627) ^ [_240021, _240023, _240025, _240027] : [function(_240021), quasi_total(_240021, _240027, _240025), relation_of2_as_subset(_240021, _240027, _240025), in(_240023, _240027), -(_240025 = empty_set), -(in(apply(_240021, _240023), relation_rng(_240021)))], (6949 ^ _39627) ^ [_240634] : [ordinal(_240634), -(well_founded_relation(inclusion_relation(_240634)))], (6955 ^ _39627) ^ [_240838, _240840] : [subset(singleton(_240840), singleton(_240838)), -(_240840 = _240838)], (6961 ^ _39627) ^ [_241070, _241072, _241074] : [relation(_241070), function(_241070), in(_241072, relation_dom(relation_dom_restriction(_241070, _241074))), -(apply(relation_dom_restriction(_241070, _241074), _241072) = apply(_241070, _241072))], (6975 ^ _39627) ^ [_241489] : [-(relation_dom(identity_relation(_241489)) = _241489)], (6977 ^ _39627) ^ [_241537] : [-(relation_rng(identity_relation(_241537)) = _241537)], (6979 ^ _39627) ^ [_241664, _241666, _241668] : [relation(_241664), function(_241664), in(_241666, _241668), -(apply(relation_dom_restriction(_241664, _241668), _241666) = apply(_241664, _241666))], (6993 ^ _39627) ^ [_242110, _242112, _242114, _242116] : [relation(_242110), 6996 ^ _39627 : [(6997 ^ _39627) ^ [] : [in(ordered_pair(_242116, _242114), relation_composition(identity_relation(_242112), _242110)), 7000 ^ _39627 : [(7001 ^ _39627) ^ [] : [-(in(_242116, _242112))], (7003 ^ _39627) ^ [] : [-(in(ordered_pair(_242116, _242114), _242110))]]], (7005 ^ _39627) ^ [] : [-(in(ordered_pair(_242116, _242114), relation_composition(identity_relation(_242112), _242110))), in(_242116, _242112), in(ordered_pair(_242116, _242114), _242110)]]], (7015 ^ _39627) ^ [_242803, _242805] : [in(_242805, _242803), empty(_242803)], (7021 ^ _39627) ^ [_243015, _243017] : [-(pair_first(ordered_pair(_243017, _243015)) = _243017)], (7023 ^ _39627) ^ [_243066, _243068] : [-(pair_second(ordered_pair(_243068, _243066)) = _243066)], (7025 ^ _39627) ^ [_243182, _243184] : [in(_243184, _243182), 7029 ^ _39627 : [(7030 ^ _39627) ^ [] : [-(in(7028 ^ [_243182, _243184], _243182))], (7032 ^ _39627) ^ [_243473] : [in(_243473, _243182), in(_243473, 7028 ^ [_243182, _243184])]]], (7038 ^ _39627) ^ [_243699] : [ordinal(_243699), -(well_ordering(inclusion_relation(_243699)))], (7044 ^ _39627) ^ [_243888, _243890] : [-(subset(_243890, set_union2(_243890, _243888)))], (7046 ^ _39627) ^ [_244029, _244031] : [disjoint(_244031, _244029), -(set_difference(_244031, _244029) = _244031)], (7052 ^ _39627) ^ [_244197, _244199] : [set_difference(_244199, _244197) = _244199, -(disjoint(_244199, _244197))], (7058 ^ _39627) ^ [_244429, _244431, _244433] : [relation(_244429), 7061 ^ _39627 : [(7062 ^ _39627) ^ [] : [in(_244433, relation_dom(relation_dom_restriction(_244429, _244431))), 7065 ^ _39627 : [(7066 ^ _39627) ^ [] : [-(in(_244433, _244431))], (7068 ^ _39627) ^ [] : [-(in(_244433, relation_dom(_244429)))]]], (7070 ^ _39627) ^ [] : [-(in(_244433, relation_dom(relation_dom_restriction(_244429, _244431)))), in(_244433, _244431), in(_244433, relation_dom(_244429))]]], (7080 ^ _39627) ^ [_245088, _245090] : [relation(_245088), -(subset(relation_dom_restriction(_245088, _245090), _245088))], (7086 ^ _39627) ^ [_245302, _245304] : [empty(_245304), -(_245304 = _245302), empty(_245302)], (7096 ^ _39627) ^ [_245613, _245615, _245617] : [relation(_245613), function(_245613), 7103 ^ _39627 : [(7104 ^ _39627) ^ [] : [in(ordered_pair(_245617, _245615), _245613), 7107 ^ _39627 : [(7108 ^ _39627) ^ [] : [-(in(_245617, relation_dom(_245613)))], (7110 ^ _39627) ^ [] : [-(_245615 = apply(_245613, _245617))]]], (7112 ^ _39627) ^ [] : [-(in(ordered_pair(_245617, _245615), _245613)), in(_245617, relation_dom(_245613)), _245615 = apply(_245613, _245617)]]], (7122 ^ _39627) ^ [_246354] : [relation(_246354), 7125 ^ _39627 : [(7126 ^ _39627) ^ [] : [well_orders(_246354, relation_field(_246354)), -(well_ordering(_246354))], (7132 ^ _39627) ^ [] : [well_ordering(_246354), -(well_orders(_246354, relation_field(_246354)))]]], (7138 ^ _39627) ^ [_246813, _246815, _246817] : [-(subset(set_union2(_246817, _246813), _246815)), subset(_246817, _246815), subset(_246813, _246815)], (7148 ^ _39627) ^ [_247142, _247144, _247146] : [singleton(_247146) = unordered_pair(_247144, _247142), -(_247146 = _247144)], (7154 ^ _39627) ^ [_247368, _247370] : [relation(_247368), -(relation_dom(relation_dom_restriction(_247368, _247370)) = set_intersection2(relation_dom(_247368), _247370))], (7160 ^ _39627) ^ [_247596, _247598] : [in(_247598, _247596), -(subset(_247598, union(_247596)))], (7166 ^ _39627) ^ [_247810, _247812] : [relation(_247810), -(relation_dom_restriction(_247810, _247812) = relation_composition(identity_relation(_247812), _247810))], (7172 ^ _39627) ^ [_248034, _248036] : [relation(_248034), -(subset(relation_rng(relation_dom_restriction(_248034, _248036)), relation_rng(_248034)))], (7178 ^ _39627) ^ [_248227] : [-(union(powerset(_248227)) = _248227)], (7180 ^ _39627) ^ [_248366, _248368, _248370, _248372] : [function(_248366), quasi_total(_248366, _248372, _248370), relation_of2_as_subset(_248366, _248372, _248370), subset(_248370, _248368), 7197 ^ _39627 : [(7198 ^ _39627) ^ [] : [-(_248370 = empty_set)], (7200 ^ _39627) ^ [] : [_248372 = empty_set]], 7201 ^ _39627 : [(7202 ^ _39627) ^ [] : [-(function(_248366))], (7204 ^ _39627) ^ [] : [-(quasi_total(_248366, _248372, _248368))], (7206 ^ _39627) ^ [] : [-(relation_of2_as_subset(_248366, _248372, _248368))]]], (7244 ^ _39627) ^ [_250632, _250634, _250636] : [singleton(_250636) = unordered_pair(_250634, _250632), -(_250634 = _250632)], (7209 ^ _39627) ^ [_249352] : [-(in(_249352, 7207 ^ [_249352]))], (7211 ^ _39627) ^ [_249464, _249466, _249468] : [-(in(_249464, 7207 ^ [_249468])), in(_249466, 7207 ^ [_249468]), subset(_249464, _249466)], (7221 ^ _39627) ^ [_249779, _249781] : [in(_249779, 7207 ^ [_249781]), 7225 ^ _39627 : [(7226 ^ _39627) ^ [] : [-(in(7224 ^ [_249779, _249781], 7207 ^ [_249781]))], (7228 ^ _39627) ^ [_250091] : [subset(_250091, _249779), -(in(_250091, 7224 ^ [_249779, _249781]))]]], (7234 ^ _39627) ^ [_250298, _250300] : [subset(_250298, 7207 ^ [_250300]), -(are_equipotent(_250298, 7207 ^ [_250300])), -(in(_250298, 7207 ^ [_250300]))]], input).
% 2.73/3.39 ncf('1',plain,[finite(7249 ^ [])],start(7256 ^ 0)).
% 2.73/3.39 ncf('1.1',plain,[-(finite(7249 ^ [])), 862 : element(7249 ^ [], powerset(7250 ^ [])), 862 : finite(7250 ^ [])],extension(858 ^ 1,bind([[_51780, _51840], [7250 ^ [], 7249 ^ []]]))).
% 2.73/3.39 ncf('1.1.1',plain,[-(element(7249 ^ [], powerset(7250 ^ []))), subset(7249 ^ [], 7250 ^ [])],extension(6256 ^ 4,bind([[_218058, _218060], [7250 ^ [], 7249 ^ []]]))).
% 2.73/3.39 ncf('1.1.1.1',plain,[-(subset(7249 ^ [], 7250 ^ []))],extension(7252 ^ 5)).
% 2.73/3.39 ncf('1.1.2',plain,[-(finite(7250 ^ []))],extension(7254 ^ 2)).
% 2.73/3.39 %-----------------------------------------------------
% 2.73/3.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------