nanoCoP---2.0.THM-Prf.s

%------------------------------------------------------------------------------
% File     : nanoCoP---2.0
% Problem  : SEU306+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : nanocop.sh %s %d

% Computer : n015.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:05 EDT 2023

% Result   : Theorem 0.47s 1.37s
% Output   : Proof 0.47s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SEU306+2 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.13  % Command  : nanocop.sh %s %d
% 0.12/0.33  % Computer : n015.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Thu May 18 13:32:22 EDT 2023
% 0.12/0.33  % CPUTime  : 
% 0.47/1.37  
% 0.47/1.37  /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.47/1.37  Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/1.37  %-----------------------------------------------------
% 0.47/1.37  ncf(matrix, plain, [(9208 ^ _51060) ^ [] : [-(one_sorted_str(9206 ^ []))], (9210 ^ _51060) ^ [] : [cast_as_carrier_subset(9206 ^ []) = the_carrier(9206 ^ [])], (676 ^ _51060) ^ [_60211, _60213, _60215, _60217, _60219, _60221] : [-(unordered_triple(_60221, _60217, _60213) = unordered_triple(_60219, _60215, _60211)), _60221 = _60219, _60217 = _60215, _60213 = _60211], (690 ^ _51060) ^ [_60432, _60434] : [_60434 = _60432, -(the_L_meet(_60434) = the_L_meet(_60432))], (696 ^ _51060) ^ [_60517, _60519] : [_60519 = _60517, -(the_L_join(_60519) = the_L_join(_60517))], (702 ^ _51060) ^ [_60602, _60604, _60606, _60608, _60610, _60612, _60614, _60616, _60618, _60620, _60622, _60624] : [-(apply_binary_as_element(_60624, _60620, _60616, _60612, _60608, _60604) = apply_binary_as_element(_60622, _60618, _60614, _60610, _60606, _60602)), _60624 = _60622, _60620 = _60618, _60616 = _60614, _60612 = _60610, _60608 = _60606, _60604 = _60602], (728 ^ _51060) ^ [_61087, _61089, _61091, _61093, _61095, _61097] : [-(apply_binary(_61097, _61093, _61089) = apply_binary(_61095, _61091, _61087)), _61097 = _61095, _61093 = _61091, _61089 = _61087], (742 ^ _51060) ^ [_61308, _61310, _61312, _61314, _61316, _61318] : [-(join_commut(_61318, _61314, _61310) = join_commut(_61316, _61312, _61308)), _61318 = _61316, _61314 = _61312, _61310 = _61308], (756 ^ _51060) ^ [_61529, _61531, _61533, _61535, _61537, _61539] : [-(join(_61539, _61535, _61531) = join(_61537, _61533, _61529)), _61539 = _61537, _61535 = _61533, _61531 = _61529], (770 ^ _51060) ^ [_61750, _61752, _61754, _61756, _61758, _61760] : [-(meet(_61760, _61756, _61752) = meet(_61758, _61754, _61750)), _61760 = _61758, _61756 = _61754, _61752 = _61750], (784 ^ _51060) ^ [_61971, _61973] : [_61973 = _61971, -(set_meet(_61973) = set_meet(_61971))], (790 ^ _51060) ^ [_62056, _62058, _62060, _62062] : [-(relation_image(_62062, _62058) = relation_image(_62060, _62056)), _62062 = _62060, _62058 = _62056], (800 ^ _51060) ^ [_62205, _62207, _62209, _62211] : [-(relation_rng_restriction(_62211, _62207) = relation_rng_restriction(_62209, _62205)), _62211 = _62209, _62207 = _62205], (810 ^ _51060) ^ [_62354, _62356, _62358, _62360] : [-(cartesian_product2(_62360, _62356) = cartesian_product2(_62358, _62354)), _62360 = _62358, _62356 = _62354], (820 ^ _51060) ^ [_62503, _62505, _62507, _62509] : [-(fiber(_62509, _62505) = fiber(_62507, _62503)), _62509 = _62507, _62505 = _62503], (830 ^ _51060) ^ [_62652, _62654, _62656, _62658, _62660, _62662] : [-(relation_dom_as_subset(_62662, _62658, _62654) = relation_dom_as_subset(_62660, _62656, _62652)), _62662 = _62660, _62658 = _62656, _62654 = _62652], (844 ^ _51060) ^ [_62873, _62875, _62877, _62879, _62881, _62883] : [-(meet_commut(_62883, _62879, _62875) = meet_commut(_62881, _62877, _62873)), _62883 = _62881, _62879 = _62877, _62875 = _62873], (858 ^ _51060) ^ [_63094, _63096, _63098, _63100, _63102, _63104] : [-(relation_rng_as_subset(_63104, _63100, _63096) = relation_rng_as_subset(_63102, _63098, _63094)), _63104 = _63102, _63100 = _63098, _63096 = _63094], (872 ^ _51060) ^ [_63315, _63317] : [_63317 = _63315, -(relation_inverse(_63317) = relation_inverse(_63315))], (878 ^ _51060) ^ [_63400, _63402, _63404, _63406] : [-(relation_restriction(_63406, _63402) = relation_restriction(_63404, _63400)), _63406 = _63404, _63402 = _63400], (888 ^ _51060) ^ [_63549, _63551] : [_63551 = _63549, -(succ(_63551) = succ(_63549))], (894 ^ _51060) ^ [_63634, _63636, _63638, _63640] : [-(relation_inverse_image(_63640, _63636) = relation_inverse_image(_63638, _63634)), _63640 = _63638, _63636 = _63634], (904 ^ _51060) ^ [_63783, _63785, _63787, _63789] : [-(union_of_subsets(_63789, _63785) = union_of_subsets(_63787, _63783)), _63789 = _63787, _63785 = _63783], (914 ^ _51060) ^ [_63932, _63934, _63936, _63938] : [-(complements_of_subsets(_63938, _63934) = complements_of_subsets(_63936, _63932)), _63938 = _63936, _63934 = _63932], (924 ^ _51060) ^ [_64081, _64083, _64085, _64087, _64089, _64091] : [-(subset_difference(_64091, _64087, _64083) = subset_difference(_64089, _64085, _64081)), _64091 = _64089, _64087 = _64085, _64083 = _64081], (938 ^ _51060) ^ [_64302, _64304] : [_64304 = _64302, -(cast_to_subset(_64304) = cast_to_subset(_64302))], (944 ^ _51060) ^ [_64387, _64389, _64391, _64393] : [-(meet_of_subsets(_64393, _64389) = meet_of_subsets(_64391, _64387)), _64393 = _64391, _64389 = _64387], (954 ^ _51060) ^ [_64536, _64538, _64540, _64542] : [-(subset_complement(_64542, _64538) = subset_complement(_64540, _64536)), _64542 = _64540, _64538 = _64536], (964 ^ _51060) ^ [_64685, _64687] : [_64687 = _64685, -(function_inverse(_64687) = function_inverse(_64685))], (970 ^ _51060) ^ [_64770, _64772] : [_64772 = _64770, -(pair_first(_64772) = pair_first(_64770))], (976 ^ _51060) ^ [_64855, _64857] : [_64857 = _64855, -(pair_second(_64857) = pair_second(_64855))], (982 ^ _51060) ^ [_64940, _64942] : [_64942 = _64940, -(inclusion_relation(_64942) = inclusion_relation(_64940))], (988 ^ _51060) ^ [_65025, _65027, _65029, _65031] : [-(set_difference(_65031, _65027) = set_difference(_65029, _65025)), _65031 = _65029, _65027 = _65025], (998 ^ _51060) ^ [_65174, _65176, _65178, _65180] : [-(ordered_pair(_65180, _65176) = ordered_pair(_65178, _65174)), _65180 = _65178, _65176 = _65174], (1008 ^ _51060) ^ [_65323, _65325, _65327, _65329] : [-(apply(_65329, _65325) = apply(_65327, _65323)), _65329 = _65327, _65325 = _65323], (1018 ^ _51060) ^ [_65472, _65474] : [_65474 = _65472, -(relation_field(_65474) = relation_field(_65472))], (1024 ^ _51060) ^ [_65557, _65559, _65561, _65563] : [-(set_union2(_65563, _65559) = set_union2(_65561, _65557)), _65563 = _65561, _65559 = _65557], (1034 ^ _51060) ^ [_65706, _65708, _65710, _65712] : [-(set_intersection2(_65712, _65708) = set_intersection2(_65710, _65706)), _65712 = _65710, _65708 = _65706], (1044 ^ _51060) ^ [_65855, _65857] : [_65857 = _65855, -(relation_dom(_65857) = relation_dom(_65855))], (1050 ^ _51060) ^ [_65940, _65942, _65944, _65946] : [-(relation_composition(_65946, _65942) = relation_composition(_65944, _65940)), _65946 = _65944, _65942 = _65940], (1060 ^ _51060) ^ [_66089, _66091] : [_66091 = _66089, -(identity_relation(_66091) = identity_relation(_66089))], (1066 ^ _51060) ^ [_66174, _66176, _66178, _66180] : [-(relation_dom_restriction(_66180, _66176) = relation_dom_restriction(_66178, _66174)), _66180 = _66178, _66176 = _66174], (1076 ^ _51060) ^ [_66323, _66325] : [_66325 = _66323, -(relation_rng(_66325) = relation_rng(_66323))], (1082 ^ _51060) ^ [_66408, _66410] : [_66410 = _66408, -(union(_66410) = union(_66408))], (1088 ^ _51060) ^ [_66493, _66495] : [_66495 = _66493, -(powerset(_66495) = powerset(_66493))], (1094 ^ _51060) ^ [_66578, _66580] : [_66580 = _66578, -(singleton(_66580) = singleton(_66578))], (1100 ^ _51060) ^ [_66663, _66665, _66667, _66669] : [-(unordered_pair(_66669, _66665) = unordered_pair(_66667, _66663)), _66669 = _66667, _66665 = _66663], (1110 ^ _51060) ^ [_66812, _66814] : [_66814 = _66812, -(cast_as_carrier_subset(_66814) = cast_as_carrier_subset(_66812))], (1116 ^ _51060) ^ [_66893, _66895] : [_66895 = _66893, -(the_carrier(_66895) = the_carrier(_66893))], (2 ^ _51060) ^ [_51090] : [-(_51090 = _51090)], (4 ^ _51060) ^ [_51113, _51115] : [_51115 = _51113, -(_51113 = _51115)], (10 ^ _51060) ^ [_51186, _51188, _51190] : [-(_51190 = _51186), _51190 = _51188, _51188 = _51186], (20 ^ _51060) ^ [_51323, _51325] : [-(v1_xcmplx_0(_51323)), _51325 = _51323, v1_xcmplx_0(_51325)], (30 ^ _51060) ^ [_51448, _51450] : [-(v1_xreal_0(_51448)), _51450 = _51448, v1_xreal_0(_51450)], (40 ^ _51060) ^ [_51573, _51575] : [-(v1_int_1(_51573)), _51575 = _51573, v1_int_1(_51575)], (50 ^ _51060) ^ [_51698, _51700] : [-(v1_rat_1(_51698)), _51700 = _51698, v1_rat_1(_51700)], (60 ^ _51060) ^ [_51823, _51825, _51827, _51829] : [-(is_antisymmetric_in(_51827, _51823)), is_antisymmetric_in(_51829, _51825), _51829 = _51827, _51825 = _51823], (74 ^ _51060) ^ [_52016, _52018, _52020, _52022] : [-(is_connected_in(_52020, _52016)), is_connected_in(_52022, _52018), _52022 = _52020, _52018 = _52016], (88 ^ _51060) ^ [_52209, _52211, _52213, _52215] : [-(is_transitive_in(_52213, _52209)), is_transitive_in(_52215, _52211), _52215 = _52213, _52211 = _52209], (102 ^ _51060) ^ [_52402, _52404, _52406, _52408] : [-(is_reflexive_in(_52406, _52402)), is_reflexive_in(_52408, _52404), _52408 = _52406, _52404 = _52402], (116 ^ _51060) ^ [_52595, _52597] : [-(cup_closed(_52595)), _52597 = _52595, cup_closed(_52597)], (126 ^ _51060) ^ [_52720, _52722] : [-(diff_closed(_52720)), _52722 = _52720, diff_closed(_52722)], (136 ^ _51060) ^ [_52845, _52847] : [-(preboolean(_52845)), _52847 = _52845, preboolean(_52847)], (146 ^ _51060) ^ [_52970, _52972] : [-(v1_membered(_52970)), _52972 = _52970, v1_membered(_52972)], (156 ^ _51060) ^ [_53095, _53097] : [-(v2_membered(_53095)), _53097 = _53095, v2_membered(_53097)], (166 ^ _51060) ^ [_53220, _53222] : [-(v3_membered(_53220)), _53222 = _53220, v3_membered(_53222)], (176 ^ _51060) ^ [_53345, _53347] : [-(v4_membered(_53345)), _53347 = _53345, v4_membered(_53347)], (186 ^ _51060) ^ [_53470, _53472] : [-(v5_membered(_53470)), _53472 = _53470, v5_membered(_53472)], (196 ^ _51060) ^ [_53595, _53597] : [-(natural(_53595)), _53597 = _53595, natural(_53597)], (206 ^ _51060) ^ [_53720, _53722] : [-(epsilon_connected(_53720)), _53722 = _53720, epsilon_connected(_53722)], (216 ^ _51060) ^ [_53845, _53847] : [-(relation_empty_yielding(_53845)), _53847 = _53845, relation_empty_yielding(_53847)], (226 ^ _51060) ^ [_53970, _53972] : [-(meet_semilatt_str(_53970)), _53972 = _53970, meet_semilatt_str(_53972)], (236 ^ _51060) ^ [_54095, _54097, _54099, _54101, _54103, _54105] : [-(relation_of2(_54103, _54099, _54095)), relation_of2(_54105, _54101, _54097), _54105 = _54103, _54101 = _54099, _54097 = _54095], (254 ^ _51060) ^ [_54364, _54366, _54368, _54370] : [-(equipotent(_54368, _54364)), equipotent(_54370, _54366), _54370 = _54368, _54366 = _54364], (268 ^ _51060) ^ [_54557, _54559] : [-(epsilon_transitive(_54557)), _54559 = _54557, epsilon_transitive(_54559)], (278 ^ _51060) ^ [_54682, _54684] : [-(meet_commutative(_54682)), _54684 = _54682, meet_commutative(_54684)], (288 ^ _51060) ^ [_54807, _54809] : [-(meet_absorbing(_54807)), _54809 = _54807, meet_absorbing(_54809)], (298 ^ _51060) ^ [_54932, _54934] : [-(latt_str(_54932)), _54934 = _54932, latt_str(_54934)], (308 ^ _51060) ^ [_55057, _55059] : [-(finite(_55057)), _55059 = _55057, finite(_55059)], (318 ^ _51060) ^ [_55182, _55184] : [-(empty_carrier(_55182)), _55184 = _55182, empty_carrier(_55184)], (328 ^ _51060) ^ [_55307, _55309] : [-(join_commutative(_55307)), _55309 = _55307, join_commutative(_55309)], (338 ^ _51060) ^ [_55432, _55434] : [-(join_semilatt_str(_55432)), _55434 = _55432, join_semilatt_str(_55434)], (348 ^ _51060) ^ [_55557, _55559, _55561, _55563, _55565, _55567] : [-(below(_55565, _55561, _55557)), below(_55567, _55563, _55559), _55567 = _55565, _55563 = _55561, _55559 = _55557], (366 ^ _51060) ^ [_55826, _55828, _55830, _55832] : [-(ordinal_subset(_55830, _55826)), ordinal_subset(_55832, _55828), _55832 = _55830, _55828 = _55826], (380 ^ _51060) ^ [_56019, _56021] : [-(being_limit_ordinal(_56019)), _56021 = _56019, being_limit_ordinal(_56021)], (390 ^ _51060) ^ [_56144, _56146] : [-(reflexive(_56144)), _56146 = _56144, reflexive(_56146)], (400 ^ _51060) ^ [_56269, _56271] : [-(transitive(_56269)), _56271 = _56269, transitive(_56271)], (410 ^ _51060) ^ [_56394, _56396] : [-(connected(_56394)), _56396 = _56394, connected(_56396)], (420 ^ _51060) ^ [_56519, _56521, _56523, _56525, _56527, _56529] : [-(relation_isomorphism(_56527, _56523, _56519)), relation_isomorphism(_56529, _56525, _56521), _56529 = _56527, _56525 = _56523, _56521 = _56519], (438 ^ _51060) ^ [_56788, _56790, _56792, _56794] : [-(element(_56792, _56788)), element(_56794, _56790), _56794 = _56792, _56790 = _56788], (452 ^ _51060) ^ [_56981, _56983, _56985, _56987] : [-(is_well_founded_in(_56985, _56981)), is_well_founded_in(_56987, _56983), _56987 = _56985, _56983 = _56981], (466 ^ _51060) ^ [_57174, _57176] : [-(antisymmetric(_57174)), _57176 = _57174, antisymmetric(_57176)], (476 ^ _51060) ^ [_57299, _57301, _57303, _57305] : [-(proper_subset(_57303, _57299)), proper_subset(_57305, _57301), _57305 = _57303, _57301 = _57299], (490 ^ _51060) ^ [_57492, _57494] : [-(one_to_one(_57492)), _57494 = _57492, one_to_one(_57494)], (500 ^ _51060) ^ [_57617, _57619] : [-(well_founded_relation(_57617)), _57619 = _57617, well_founded_relation(_57619)], (510 ^ _51060) ^ [_57742, _57744] : [-(ordinal(_57742)), _57744 = _57742, ordinal(_57744)], (520 ^ _51060) ^ [_57867, _57869, _57871, _57873] : [-(disjoint(_57871, _57867)), disjoint(_57873, _57869), _57873 = _57871, _57869 = _57867], (534 ^ _51060) ^ [_58060, _58062] : [-(empty(_58060)), _58062 = _58060, empty(_58062)], (544 ^ _51060) ^ [_58185, _58187, _58189, _58191] : [-(well_orders(_58189, _58185)), well_orders(_58191, _58187), _58191 = _58189, _58187 = _58185], (558 ^ _51060) ^ [_58378, _58380] : [-(well_ordering(_58378)), _58380 = _58378, well_ordering(_58380)], (568 ^ _51060) ^ [_58503, _58505] : [-(relation(_58503)), _58505 = _58503, relation(_58505)], (578 ^ _51060) ^ [_58628, _58630] : [-(function(_58628)), _58630 = _58628, function(_58630)], (588 ^ _51060) ^ [_58753, _58755, _58757, _58759, _58761, _58763] : [-(quasi_total(_58761, _58757, _58753)), quasi_total(_58763, _58759, _58755), _58763 = _58761, _58759 = _58757, _58755 = _58753], (606 ^ _51060) ^ [_59022, _59024, _59026, _59028, _59030, _59032] : [-(relation_of2_as_subset(_59030, _59026, _59022)), relation_of2_as_subset(_59032, _59028, _59024), _59032 = _59030, _59028 = _59026, _59024 = _59022], (624 ^ _51060) ^ [_59291, _59293, _59295, _59297] : [-(subset(_59295, _59291)), subset(_59297, _59293), _59297 = _59295, _59293 = _59291], (638 ^ _51060) ^ [_59484, _59486, _59488, _59490] : [-(are_equipotent(_59488, _59484)), are_equipotent(_59490, _59486), _59490 = _59488, _59486 = _59484], (666 ^ _51060) ^ [_59866, _59868] : [-(one_sorted_str(_59866)), _59868 = _59866, one_sorted_str(_59868)], (652 ^ _51060) ^ [_59677, _59679, _59681, _59683] : [-(in(_59681, _59677)), in(_59683, _59679), _59683 = _59681, _59679 = _59677], (1122 ^ _51060) ^ [_67128, _67130] : [in(_67130, _67128), in(_67128, _67130)], (1128 ^ _51060) ^ [_67206, _67208] : [proper_subset(_67208, _67206), proper_subset(_67206, _67208)], (1134 ^ _51060) ^ [_67284] : [v1_membered(_67284), 1137 ^ _51060 : [(1138 ^ _51060) ^ [_67342] : [element(_67342, _67284), -(v1_xcmplx_0(_67342))]]], (1144 ^ _51060) ^ [_67421] : [v2_membered(_67421), 1147 ^ _51060 : [(1148 ^ _51060) ^ [_67484] : [element(_67484, _67421), 1151 ^ _51060 : [(1152 ^ _51060) ^ [] : [-(v1_xcmplx_0(_67484))], (1154 ^ _51060) ^ [] : [-(v1_xreal_0(_67484))]]]]], (1156 ^ _51060) ^ [_67587] : [v3_membered(_67587), 1159 ^ _51060 : [(1160 ^ _51060) ^ [_67655] : [element(_67655, _67587), 1163 ^ _51060 : [(1164 ^ _51060) ^ [] : [-(v1_xcmplx_0(_67655))], (1166 ^ _51060) ^ [] : [-(v1_xreal_0(_67655))], (1168 ^ _51060) ^ [] : [-(v1_rat_1(_67655))]]]]], (1170 ^ _51060) ^ [_67780] : [v4_membered(_67780), 1173 ^ _51060 : [(1174 ^ _51060) ^ [_67853] : [element(_67853, _67780), 1177 ^ _51060 : [(1178 ^ _51060) ^ [] : [-(v1_xcmplx_0(_67853))], (1180 ^ _51060) ^ [] : [-(v1_xreal_0(_67853))], (1182 ^ _51060) ^ [] : [-(v1_int_1(_67853))], (1184 ^ _51060) ^ [] : [-(v1_rat_1(_67853))]]]]], (1186 ^ _51060) ^ [_68000] : [v5_membered(_68000), 1189 ^ _51060 : [(1190 ^ _51060) ^ [_68078] : [element(_68078, _68000), 1193 ^ _51060 : [(1194 ^ _51060) ^ [] : [-(v1_xcmplx_0(_68078))], (1196 ^ _51060) ^ [] : [-(natural(_68078))], (1198 ^ _51060) ^ [] : [-(v1_xreal_0(_68078))], (1200 ^ _51060) ^ [] : [-(v1_int_1(_68078))], (1202 ^ _51060) ^ [] : [-(v1_rat_1(_68078))]]]]], (1204 ^ _51060) ^ [_68247] : [empty(_68247), 1207 ^ _51060 : [(1208 ^ _51060) ^ [] : [-(v1_membered(_68247))], (1210 ^ _51060) ^ [] : [-(v2_membered(_68247))], (1212 ^ _51060) ^ [] : [-(v3_membered(_68247))], (1214 ^ _51060) ^ [] : [-(v4_membered(_68247))], (1216 ^ _51060) ^ [] : [-(v5_membered(_68247))]]], (1218 ^ _51060) ^ [_68408] : [v1_membered(_68408), 1221 ^ _51060 : [(1222 ^ _51060) ^ [_68468] : [element(_68468, powerset(_68408)), -(v1_membered(_68468))]]], (1228 ^ _51060) ^ [_68551] : [v2_membered(_68551), 1231 ^ _51060 : [(1232 ^ _51060) ^ [_68616] : [element(_68616, powerset(_68551)), 1235 ^ _51060 : [(1236 ^ _51060) ^ [] : [-(v1_membered(_68616))], (1238 ^ _51060) ^ [] : [-(v2_membered(_68616))]]]]], (1240 ^ _51060) ^ [_68723] : [v3_membered(_68723), 1243 ^ _51060 : [(1244 ^ _51060) ^ [_68793] : [element(_68793, powerset(_68723)), 1247 ^ _51060 : [(1248 ^ _51060) ^ [] : [-(v1_membered(_68793))], (1250 ^ _51060) ^ [] : [-(v2_membered(_68793))], (1252 ^ _51060) ^ [] : [-(v3_membered(_68793))]]]]], (1254 ^ _51060) ^ [_68922] : [v4_membered(_68922), 1257 ^ _51060 : [(1258 ^ _51060) ^ [_68997] : [element(_68997, powerset(_68922)), 1261 ^ _51060 : [(1262 ^ _51060) ^ [] : [-(v1_membered(_68997))], (1264 ^ _51060) ^ [] : [-(v2_membered(_68997))], (1266 ^ _51060) ^ [] : [-(v3_membered(_68997))], (1268 ^ _51060) ^ [] : [-(v4_membered(_68997))]]]]], (1270 ^ _51060) ^ [_69148] : [ordinal(_69148), 1273 ^ _51060 : [(1274 ^ _51060) ^ [_69216] : [element(_69216, _69148), 1277 ^ _51060 : [(1278 ^ _51060) ^ [] : [-(epsilon_transitive(_69216))], (1280 ^ _51060) ^ [] : [-(epsilon_connected(_69216))], (1282 ^ _51060) ^ [] : [-(ordinal(_69216))]]]]], (1284 ^ _51060) ^ [_69341] : [empty(_69341), -(finite(_69341))], (1290 ^ _51060) ^ [_69412] : [preboolean(_69412), 1293 ^ _51060 : [(1294 ^ _51060) ^ [] : [-(cup_closed(_69412))], (1296 ^ _51060) ^ [] : [-(diff_closed(_69412))]]], (1298 ^ _51060) ^ [_69507] : [empty(_69507), -(function(_69507))], (1304 ^ _51060) ^ [_69578] : [v5_membered(_69578), -(v4_membered(_69578))], (1310 ^ _51060) ^ [_69649] : [ordinal(_69649), 1313 ^ _51060 : [(1314 ^ _51060) ^ [] : [-(epsilon_transitive(_69649))], (1316 ^ _51060) ^ [] : [-(epsilon_connected(_69649))]]], (1318 ^ _51060) ^ [_69744] : [empty(_69744), -(relation(_69744))], (1324 ^ _51060) ^ [_69815, _69817, _69819] : [element(_69815, powerset(cartesian_product2(_69819, _69817))), -(relation(_69815))], (1330 ^ _51060) ^ [_69902] : [v5_membered(_69902), 1333 ^ _51060 : [(1334 ^ _51060) ^ [_69982] : [element(_69982, powerset(_69902)), 1337 ^ _51060 : [(1338 ^ _51060) ^ [] : [-(v1_membered(_69982))], (1340 ^ _51060) ^ [] : [-(v2_membered(_69982))], (1342 ^ _51060) ^ [] : [-(v3_membered(_69982))], (1344 ^ _51060) ^ [] : [-(v4_membered(_69982))], (1346 ^ _51060) ^ [] : [-(v5_membered(_69982))]]]]], (1348 ^ _51060) ^ [_70155] : [1355 ^ _51060 : [(1356 ^ _51060) ^ [] : [-(epsilon_transitive(_70155))], (1358 ^ _51060) ^ [] : [-(epsilon_connected(_70155))], (1360 ^ _51060) ^ [] : [-(ordinal(_70155))], (1362 ^ _51060) ^ [] : [-(natural(_70155))]], empty(_70155), ordinal(_70155)], (1364 ^ _51060) ^ [_70342] : [finite(_70342), 1367 ^ _51060 : [(1368 ^ _51060) ^ [_70402] : [element(_70402, powerset(_70342)), -(finite(_70402))]]], (1374 ^ _51060) ^ [_70485] : [-(preboolean(_70485)), cup_closed(_70485), diff_closed(_70485)], (1384 ^ _51060) ^ [_70604] : [1395 ^ _51060 : [(1396 ^ _51060) ^ [] : [-(relation(_70604))], (1398 ^ _51060) ^ [] : [-(function(_70604))], (1400 ^ _51060) ^ [] : [-(one_to_one(_70604))]], relation(_70604), empty(_70604), function(_70604)], (1402 ^ _51060) ^ [_70817] : [v4_membered(_70817), -(v3_membered(_70817))], (1408 ^ _51060) ^ [_70888] : [-(ordinal(_70888)), epsilon_transitive(_70888), epsilon_connected(_70888)], (1418 ^ _51060) ^ [_71007] : [element(_71007, omega), 1421 ^ _51060 : [(1422 ^ _51060) ^ [] : [-(epsilon_transitive(_71007))], (1424 ^ _51060) ^ [] : [-(epsilon_connected(_71007))], (1426 ^ _51060) ^ [] : [-(ordinal(_71007))], (1428 ^ _51060) ^ [] : [-(natural(_71007))]]], (1430 ^ _51060) ^ [_71148] : [v3_membered(_71148), -(v2_membered(_71148))], (1436 ^ _51060) ^ [_71219] : [empty(_71219), 1439 ^ _51060 : [(1440 ^ _51060) ^ [] : [-(epsilon_transitive(_71219))], (1442 ^ _51060) ^ [] : [-(epsilon_connected(_71219))], (1444 ^ _51060) ^ [] : [-(ordinal(_71219))]]], (1446 ^ _51060) ^ [_71336] : [v2_membered(_71336), -(v1_membered(_71336))], (1452 ^ _51060) ^ [_71407, _71409] : [-(unordered_pair(_71409, _71407) = unordered_pair(_71407, _71409))], (1454 ^ _51060) ^ [_71438, _71440] : [-(set_union2(_71440, _71438) = set_union2(_71438, _71440))], (1456 ^ _51060) ^ [_71469, _71471, _71473] : [-(join_commut(_71473, _71471, _71469) = join_commut(_71473, _71469, _71471)), -(empty_carrier(_71473)), join_commutative(_71473), join_semilatt_str(_71473), element(_71471, the_carrier(_71473)), element(_71469, the_carrier(_71473))], (1478 ^ _51060) ^ [_71785, _71787] : [-(set_intersection2(_71787, _71785) = set_intersection2(_71785, _71787))], (1480 ^ _51060) ^ [_71816, _71818, _71820] : [-(meet_commut(_71820, _71818, _71816) = meet_commut(_71820, _71816, _71818)), -(empty_carrier(_71820)), meet_commutative(_71820), meet_semilatt_str(_71820), element(_71818, the_carrier(_71820)), element(_71816, the_carrier(_71820))], (1502 ^ _51060) ^ [_72132, _72134] : [ordinal(_72134), ordinal(_72132), -(ordinal_subset(_72134, _72132)), -(ordinal_subset(_72132, _72134))], (1516 ^ _51060) ^ [_72272, _72274] : [relation(_72272), 1519 ^ _51060 : [(1542 ^ _51060) ^ [] : [-(_72272 = identity_relation(_72274)), 1555 ^ _51060 : [(1556 ^ _51060) ^ [] : [-(in(1543 ^ [_72272, _72274], _72274))], (1558 ^ _51060) ^ [] : [-(1543 ^ [_72272, _72274] = 1544 ^ [_72272, _72274])], (1560 ^ _51060) ^ [] : [in(ordered_pair(1543 ^ [_72272, _72274], 1544 ^ [_72272, _72274]), _72272)]], 1547 ^ _51060 : [(1548 ^ _51060) ^ [] : [-(in(ordered_pair(1543 ^ [_72272, _72274], 1544 ^ [_72272, _72274]), _72272))], (1550 ^ _51060) ^ [] : [in(1543 ^ [_72272, _72274], _72274), 1543 ^ [_72272, _72274] = 1544 ^ [_72272, _72274]]]], (1520 ^ _51060) ^ [] : [_72272 = identity_relation(_72274), 1523 ^ _51060 : [(1524 ^ _51060) ^ [_72425, _72427] : [in(ordered_pair(_72427, _72425), _72272), 1527 ^ _51060 : [(1528 ^ _51060) ^ [] : [-(in(_72427, _72274))], (1530 ^ _51060) ^ [] : [-(_72427 = _72425)]]], (1532 ^ _51060) ^ [_72534, _72536] : [-(in(ordered_pair(_72536, _72534), _72272)), in(_72536, _72274), _72536 = _72534]]]]], (1564 ^ _51060) ^ [_73061, _73063] : [_73063 = _73061, 1567 ^ _51060 : [(1568 ^ _51060) ^ [] : [-(subset(_73063, _73061))], (1570 ^ _51060) ^ [] : [-(subset(_73061, _73063))]]], (1572 ^ _51060) ^ [_73160, _73162] : [-(_73162 = _73160), subset(_73162, _73160), subset(_73160, _73162)], (1582 ^ _51060) ^ [_73291] : [relation(_73291), 1585 ^ _51060 : [(1586 ^ _51060) ^ [_73391, _73393] : [relation(_73391), 1589 ^ _51060 : [(1612 ^ _51060) ^ [] : [-(_73391 = relation_dom_restriction(_73291, _73393)), 1625 ^ _51060 : [(1626 ^ _51060) ^ [] : [-(in(1613 ^ [_73291, _73391, _73393], _73393))], (1628 ^ _51060) ^ [] : [-(in(ordered_pair(1613 ^ [_73291, _73391, _73393], 1614 ^ [_73291, _73391, _73393]), _73291))], (1630 ^ _51060) ^ [] : [in(ordered_pair(1613 ^ [_73291, _73391, _73393], 1614 ^ [_73291, _73391, _73393]), _73391)]], 1617 ^ _51060 : [(1618 ^ _51060) ^ [] : [-(in(ordered_pair(1613 ^ [_73291, _73391, _73393], 1614 ^ [_73291, _73391, _73393]), _73391))], (1620 ^ _51060) ^ [] : [in(1613 ^ [_73291, _73391, _73393], _73393), in(ordered_pair(1613 ^ [_73291, _73391, _73393], 1614 ^ [_73291, _73391, _73393]), _73291)]]], (1590 ^ _51060) ^ [] : [_73391 = relation_dom_restriction(_73291, _73393), 1593 ^ _51060 : [(1594 ^ _51060) ^ [_73553, _73555] : [in(ordered_pair(_73555, _73553), _73391), 1597 ^ _51060 : [(1598 ^ _51060) ^ [] : [-(in(_73555, _73393))], (1600 ^ _51060) ^ [] : [-(in(ordered_pair(_73555, _73553), _73291))]]], (1602 ^ _51060) ^ [_73670, _73672] : [-(in(ordered_pair(_73672, _73670), _73391)), in(_73672, _73393), in(ordered_pair(_73672, _73670), _73291)]]]]]]], (1634 ^ _51060) ^ [_74240] : [relation(_74240), function(_74240), 1641 ^ _51060 : [(1671 ^ _51060) ^ [_74918, _74920] : [-(_74918 = relation_image(_74240, _74920)), 1688 ^ _51060 : [(1689 ^ _51060) ^ [] : [-(in(1687 ^ [_74240, _74918, _74920], relation_dom(_74240)))], (1691 ^ _51060) ^ [] : [-(in(1687 ^ [_74240, _74918, _74920], _74920))], (1693 ^ _51060) ^ [] : [-(1672 ^ [_74240, _74918, _74920] = apply(_74240, 1687 ^ [_74240, _74918, _74920]))], (1695 ^ _51060) ^ [] : [in(1672 ^ [_74240, _74918, _74920], _74918)]], 1675 ^ _51060 : [(1676 ^ _51060) ^ [] : [-(in(1672 ^ [_74240, _74918, _74920], _74918))], (1678 ^ _51060) ^ [_75082] : [in(_75082, relation_dom(_74240)), in(_75082, _74920), 1672 ^ [_74240, _74918, _74920] = apply(_74240, _75082)]]], (1642 ^ _51060) ^ [_74403, _74405] : [_74403 = relation_image(_74240, _74405), 1645 ^ _51060 : [(1646 ^ _51060) ^ [_74508] : [in(_74508, _74403), 1650 ^ _51060 : [(1651 ^ _51060) ^ [] : [-(in(1649 ^ [_74240, _74403, _74405, _74508], relation_dom(_74240)))], (1653 ^ _51060) ^ [] : [-(in(1649 ^ [_74240, _74403, _74405, _74508], _74405))], (1655 ^ _51060) ^ [] : [-(_74508 = apply(_74240, 1649 ^ [_74240, _74403, _74405, _74508]))]]], (1657 ^ _51060) ^ [_74683] : [-(in(_74683, _74403)), 1658 ^ _51060 : [(1659 ^ _51060) ^ [_74738] : [in(_74738, relation_dom(_74240)), in(_74738, _74405), _74683 = apply(_74240, _74738)]]]]]]], (1699 ^ _51060) ^ [_75429, _75431] : [relation(_75429), 1702 ^ _51060 : [(1703 ^ _51060) ^ [_75526] : [relation(_75526), 1706 ^ _51060 : [(1729 ^ _51060) ^ [] : [-(_75526 = relation_rng_restriction(_75431, _75429)), 1742 ^ _51060 : [(1743 ^ _51060) ^ [] : [-(in(1731 ^ [_75429, _75431, _75526], _75431))], (1745 ^ _51060) ^ [] : [-(in(ordered_pair(1730 ^ [_75429, _75431, _75526], 1731 ^ [_75429, _75431, _75526]), _75429))], (1747 ^ _51060) ^ [] : [in(ordered_pair(1730 ^ [_75429, _75431, _75526], 1731 ^ [_75429, _75431, _75526]), _75526)]], 1734 ^ _51060 : [(1735 ^ _51060) ^ [] : [-(in(ordered_pair(1730 ^ [_75429, _75431, _75526], 1731 ^ [_75429, _75431, _75526]), _75526))], (1737 ^ _51060) ^ [] : [in(1731 ^ [_75429, _75431, _75526], _75431), in(ordered_pair(1730 ^ [_75429, _75431, _75526], 1731 ^ [_75429, _75431, _75526]), _75429)]]], (1707 ^ _51060) ^ [] : [_75526 = relation_rng_restriction(_75431, _75429), 1710 ^ _51060 : [(1711 ^ _51060) ^ [_75688, _75690] : [in(ordered_pair(_75690, _75688), _75526), 1714 ^ _51060 : [(1715 ^ _51060) ^ [] : [-(in(_75688, _75431))], (1717 ^ _51060) ^ [] : [-(in(ordered_pair(_75690, _75688), _75429))]]], (1719 ^ _51060) ^ [_75805, _75807] : [-(in(ordered_pair(_75807, _75805), _75526)), in(_75805, _75431), in(ordered_pair(_75807, _75805), _75429)]]]]]]], (1751 ^ _51060) ^ [_76366] : [relation(_76366), 1754 ^ _51060 : [(1755 ^ _51060) ^ [] : [antisymmetric(_76366), -(is_antisymmetric_in(_76366, relation_field(_76366)))], (1761 ^ _51060) ^ [] : [is_antisymmetric_in(_76366, relation_field(_76366)), -(antisymmetric(_76366))]]], (1767 ^ _51060) ^ [_76568] : [relation(_76568), function(_76568), 1774 ^ _51060 : [(1797 ^ _51060) ^ [_77076, _77078] : [-(_77076 = relation_inverse_image(_76568, _77078)), 1809 ^ _51060 : [(1810 ^ _51060) ^ [] : [-(in(1798 ^ [_76568, _77076, _77078], relation_dom(_76568)))], (1812 ^ _51060) ^ [] : [-(in(apply(_76568, 1798 ^ [_76568, _77076, _77078]), _77078))], (1814 ^ _51060) ^ [] : [in(1798 ^ [_76568, _77076, _77078], _77076)]], 1801 ^ _51060 : [(1802 ^ _51060) ^ [] : [-(in(1798 ^ [_76568, _77076, _77078], _77076))], (1804 ^ _51060) ^ [] : [in(1798 ^ [_76568, _77076, _77078], relation_dom(_76568)), in(apply(_76568, 1798 ^ [_76568, _77076, _77078]), _77078)]]], (1775 ^ _51060) ^ [_76720, _76722] : [_76720 = relation_inverse_image(_76568, _76722), 1778 ^ _51060 : [(1779 ^ _51060) ^ [_76814] : [in(_76814, _76720), 1782 ^ _51060 : [(1783 ^ _51060) ^ [] : [-(in(_76814, relation_dom(_76568)))], (1785 ^ _51060) ^ [] : [-(in(apply(_76568, _76814), _76722))]]], (1787 ^ _51060) ^ [_76927] : [-(in(_76927, _76720)), in(_76927, relation_dom(_76568)), in(apply(_76568, _76927), _76722)]]]]], (1818 ^ _51060) ^ [_77456] : [relation(_77456), 1821 ^ _51060 : [(1845 ^ _51060) ^ [_77961, _77963] : [-(_77961 = relation_image(_77456, _77963)), 1858 ^ _51060 : [(1859 ^ _51060) ^ [] : [-(in(ordered_pair(1857 ^ [_77456, _77961, _77963], 1846 ^ [_77456, _77961, _77963]), _77456))], (1861 ^ _51060) ^ [] : [-(in(1857 ^ [_77456, _77961, _77963], _77963))], (1863 ^ _51060) ^ [] : [in(1846 ^ [_77456, _77961, _77963], _77961)]], 1849 ^ _51060 : [(1850 ^ _51060) ^ [] : [-(in(1846 ^ [_77456, _77961, _77963], _77961))], (1852 ^ _51060) ^ [_78109] : [in(ordered_pair(_78109, 1846 ^ [_77456, _77961, _77963]), _77456), in(_78109, _77963)]]], (1822 ^ _51060) ^ [_77563, _77565] : [_77563 = relation_image(_77456, _77565), 1825 ^ _51060 : [(1826 ^ _51060) ^ [_77660] : [in(_77660, _77563), 1830 ^ _51060 : [(1831 ^ _51060) ^ [] : [-(in(ordered_pair(1829 ^ [_77456, _77563, _77565, _77660], _77660), _77456))], (1833 ^ _51060) ^ [] : [-(in(1829 ^ [_77456, _77563, _77565, _77660], _77565))]]], (1835 ^ _51060) ^ [_77796] : [-(in(_77796, _77563)), 1836 ^ _51060 : [(1837 ^ _51060) ^ [_77843] : [in(ordered_pair(_77843, _77796), _77456), in(_77843, _77565)]]]]]]], (1867 ^ _51060) ^ [_78363] : [relation(_78363), 1870 ^ _51060 : [(1894 ^ _51060) ^ [_78868, _78870] : [-(_78868 = relation_inverse_image(_78363, _78870)), 1907 ^ _51060 : [(1908 ^ _51060) ^ [] : [-(in(ordered_pair(1895 ^ [_78363, _78868, _78870], 1906 ^ [_78363, _78868, _78870]), _78363))], (1910 ^ _51060) ^ [] : [-(in(1906 ^ [_78363, _78868, _78870], _78870))], (1912 ^ _51060) ^ [] : [in(1895 ^ [_78363, _78868, _78870], _78868)]], 1898 ^ _51060 : [(1899 ^ _51060) ^ [] : [-(in(1895 ^ [_78363, _78868, _78870], _78868))], (1901 ^ _51060) ^ [_79016] : [in(ordered_pair(1895 ^ [_78363, _78868, _78870], _79016), _78363), in(_79016, _78870)]]], (1871 ^ _51060) ^ [_78470, _78472] : [_78470 = relation_inverse_image(_78363, _78472), 1874 ^ _51060 : [(1875 ^ _51060) ^ [_78567] : [in(_78567, _78470), 1879 ^ _51060 : [(1880 ^ _51060) ^ [] : [-(in(ordered_pair(_78567, 1878 ^ [_78363, _78470, _78472, _78567]), _78363))], (1882 ^ _51060) ^ [] : [-(in(1878 ^ [_78363, _78470, _78472, _78567], _78472))]]], (1884 ^ _51060) ^ [_78703] : [-(in(_78703, _78470)), 1885 ^ _51060 : [(1886 ^ _51060) ^ [_78750] : [in(ordered_pair(_78703, _78750), _78363), in(_78750, _78472)]]]]]]], (1916 ^ _51060) ^ [_79270] : [relation(_79270), 1919 ^ _51060 : [(1920 ^ _51060) ^ [] : [connected(_79270), -(is_connected_in(_79270, relation_field(_79270)))], (1926 ^ _51060) ^ [] : [is_connected_in(_79270, relation_field(_79270)), -(connected(_79270))]]], (1932 ^ _51060) ^ [_79472] : [relation(_79472), 1935 ^ _51060 : [(1936 ^ _51060) ^ [] : [transitive(_79472), -(is_transitive_in(_79472, relation_field(_79472)))], (1942 ^ _51060) ^ [] : [is_transitive_in(_79472, relation_field(_79472)), -(transitive(_79472))]]], (1976 ^ _51060) ^ [_80081, _80083, _80085, _80087] : [-(_80081 = unordered_triple(_80087, _80085, _80083)), 1980 ^ _51060 : [(1981 ^ _51060) ^ [] : [-(in(1977 ^ [_80081, _80083, _80085, _80087], _80081))], (1983 ^ _51060) ^ [] : [1977 ^ [_80081, _80083, _80085, _80087] = _80087], (1985 ^ _51060) ^ [] : [1977 ^ [_80081, _80083, _80085, _80087] = _80085], (1987 ^ _51060) ^ [] : [1977 ^ [_80081, _80083, _80085, _80087] = _80083]], 1988 ^ _51060 : [(1999 ^ _51060) ^ [] : [in(1977 ^ [_80081, _80083, _80085, _80087], _80081)], (1989 ^ _51060) ^ [] : [-(1977 ^ [_80081, _80083, _80085, _80087] = _80087), -(1977 ^ [_80081, _80083, _80085, _80087] = _80085), -(1977 ^ [_80081, _80083, _80085, _80087] = _80083)]]], (1948 ^ _51060) ^ [_79695, _79697, _79699, _79701] : [_79695 = unordered_triple(_79701, _79699, _79697), 1951 ^ _51060 : [(1966 ^ _51060) ^ [_79915] : [1967 ^ _51060 : [(1968 ^ _51060) ^ [] : [_79915 = _79701], (1970 ^ _51060) ^ [] : [_79915 = _79699], (1972 ^ _51060) ^ [] : [_79915 = _79697]], -(in(_79915, _79695))], (1952 ^ _51060) ^ [_79802] : [in(_79802, _79695), -(_79802 = _79701), -(_79802 = _79699), -(_79802 = _79697)]]], (2003 ^ _51060) ^ [_80521] : [finite(_80521), 2007 ^ _51060 : [(2008 ^ _51060) ^ [] : [-(relation(2006 ^ [_80521]))], (2010 ^ _51060) ^ [] : [-(function(2006 ^ [_80521]))], (2012 ^ _51060) ^ [] : [-(relation_rng(2006 ^ [_80521]) = _80521)], (2014 ^ _51060) ^ [] : [-(in(relation_dom(2006 ^ [_80521]), omega))]]], (2016 ^ _51060) ^ [_80693] : [-(finite(_80693)), 2017 ^ _51060 : [(2018 ^ _51060) ^ [_80744] : [relation(_80744), function(_80744), relation_rng(_80744) = _80693, in(relation_dom(_80744), omega)]]], (2048 ^ _51060) ^ [_81199] : [2052 ^ _51060 : [(2053 ^ _51060) ^ [] : [-(in(ordered_pair(2049 ^ [_81199], 2050 ^ [_81199]), _81199))], (2055 ^ _51060) ^ [] : [-(in(ordered_pair(2049 ^ [_81199], 2051 ^ [_81199]), _81199))], (2057 ^ _51060) ^ [] : [2050 ^ [_81199] = 2051 ^ [_81199]]], -(function(_81199))], (2034 ^ _51060) ^ [_80969] : [function(_80969), 2037 ^ _51060 : [(2038 ^ _51060) ^ [_81050, _81052, _81054] : [-(_81052 = _81050), in(ordered_pair(_81054, _81052), _80969), in(ordered_pair(_81054, _81050), _80969)]]], (2061 ^ _51060) ^ [_81405, _81407, _81409] : [relation_of2_as_subset(_81405, _81409, _81407), 2064 ^ _51060 : [(2065 ^ _51060) ^ [] : [2066 ^ _51060 : [(2067 ^ _51060) ^ [] : [-(_81407 = empty_set)], (2069 ^ _51060) ^ [] : [_81409 = empty_set]], 2070 ^ _51060 : [(2071 ^ _51060) ^ [] : [quasi_total(_81405, _81409, _81407), -(_81409 = relation_dom_as_subset(_81409, _81407, _81405))], (2077 ^ _51060) ^ [] : [_81409 = relation_dom_as_subset(_81409, _81407, _81405), -(quasi_total(_81405, _81409, _81407))]]], (2083 ^ _51060) ^ [] : [_81407 = empty_set, -(_81409 = empty_set), 2090 ^ _51060 : [(2091 ^ _51060) ^ [] : [quasi_total(_81405, _81409, _81407), -(_81405 = empty_set)], (2097 ^ _51060) ^ [] : [_81405 = empty_set, -(quasi_total(_81405, _81409, _81407))]]]]], (2103 ^ _51060) ^ [_82000] : [-(empty_carrier(_82000)), join_semilatt_str(_82000), 2110 ^ _51060 : [(2111 ^ _51060) ^ [_82144] : [element(_82144, the_carrier(_82000)), 2114 ^ _51060 : [(2115 ^ _51060) ^ [_82232] : [element(_82232, the_carrier(_82000)), -(join(_82000, _82144, _82232) = apply_binary_as_element(the_carrier(_82000), the_carrier(_82000), the_carrier(_82000), the_L_join(_82000), _82144, _82232))]]]]], (2121 ^ _51060) ^ [_82363] : [2122 ^ _51060 : [(2123 ^ _51060) ^ [_82443, _82445] : [_82363 = ordered_pair(_82445, _82443)]], 2124 ^ _51060 : [(2135 ^ _51060) ^ [_82646] : [2138 ^ _51060 : [(2139 ^ _51060) ^ [] : [-(_82363 = ordered_pair(2136 ^ [_82363, _82646], 2137 ^ [_82363, _82646]))], (2141 ^ _51060) ^ [] : [_82646 = 2136 ^ [_82363, _82646]]], -(_82646 = pair_first(_82363))], (2125 ^ _51060) ^ [_82484] : [_82484 = pair_first(_82363), 2128 ^ _51060 : [(2129 ^ _51060) ^ [_82559, _82561] : [_82363 = ordered_pair(_82561, _82559), -(_82484 = _82561)]]]]], (2145 ^ _51060) ^ [_82817] : [-(succ(_82817) = set_union2(_82817, singleton(_82817)))], (2159 ^ _51060) ^ [_83044] : [2161 ^ _51060 : [(2162 ^ _51060) ^ [] : [-(in(2160 ^ [_83044], _83044))], (2164 ^ _51060) ^ [_83157, _83159] : [2160 ^ [_83044] = ordered_pair(_83159, _83157)]], -(relation(_83044))], (2147 ^ _51060) ^ [_82859] : [relation(_82859), 2150 ^ _51060 : [(2151 ^ _51060) ^ [_82935] : [in(_82935, _82859), -(_82935 = ordered_pair(2154 ^ [_82859, _82935], 2155 ^ [_82859, _82935]))]]], (2168 ^ _51060) ^ [_83221] : [relation(_83221), 2171 ^ _51060 : [(2182 ^ _51060) ^ [_83457] : [2184 ^ _51060 : [(2185 ^ _51060) ^ [] : [-(in(2183 ^ [_83221, _83457], _83457))], (2187 ^ _51060) ^ [] : [in(ordered_pair(2183 ^ [_83221, _83457], 2183 ^ [_83221, _83457]), _83221)]], -(is_reflexive_in(_83221, _83457))], (2172 ^ _51060) ^ [_83306] : [is_reflexive_in(_83221, _83306), 2175 ^ _51060 : [(2176 ^ _51060) ^ [_83372] : [in(_83372, _83306), -(in(ordered_pair(_83372, _83372), _83221))]]]]], (2191 ^ _51060) ^ [_83637, _83639, _83641] : [relation_of2(_83637, _83641, _83639), -(subset(_83637, cartesian_product2(_83641, _83639)))], (2197 ^ _51060) ^ [_83720, _83722, _83724] : [subset(_83720, cartesian_product2(_83724, _83722)), -(relation_of2(_83720, _83724, _83722))], (2252 ^ _51060) ^ [_84610, _84612] : [_84612 = empty_set, 2255 ^ _51060 : [(2256 ^ _51060) ^ [] : [_84610 = set_meet(_84612), -(_84610 = empty_set)], (2262 ^ _51060) ^ [] : [_84610 = empty_set, -(_84610 = set_meet(_84612))]]], (2203 ^ _51060) ^ [_83817, _83819] : [-(_83819 = empty_set), 2206 ^ _51060 : [(2230 ^ _51060) ^ [] : [-(_83817 = set_meet(_83819)), 2234 ^ _51060 : [(2235 ^ _51060) ^ [] : [-(in(2231 ^ [_83817, _83819], _83817))], (2238 ^ _51060) ^ [] : [-(in(2236 ^ [_83817, _83819], _83819))], (2240 ^ _51060) ^ [] : [in(2231 ^ [_83817, _83819], 2236 ^ [_83817, _83819])]], 2241 ^ _51060 : [(2248 ^ _51060) ^ [] : [in(2231 ^ [_83817, _83819], _83817)], (2242 ^ _51060) ^ [_84454] : [in(_84454, _83819), -(in(2231 ^ [_83817, _83819], _84454))]]], (2207 ^ _51060) ^ [] : [_83817 = set_meet(_83819), 2210 ^ _51060 : [(2221 ^ _51060) ^ [_84110] : [2223 ^ _51060 : [(2224 ^ _51060) ^ [] : [-(in(2222 ^ [_83817, _83819, _84110], _83819))], (2226 ^ _51060) ^ [] : [in(_84110, 2222 ^ [_83817, _83819, _84110])]], -(in(_84110, _83817))], (2211 ^ _51060) ^ [_83964] : [in(_83964, _83817), 2214 ^ _51060 : [(2215 ^ _51060) ^ [_84029] : [in(_84029, _83819), -(in(_83964, _84029))]]]]]]], (2284 ^ _51060) ^ [_85075, _85077] : [-(_85075 = singleton(_85077)), 2288 ^ _51060 : [(2289 ^ _51060) ^ [] : [-(in(2285 ^ [_85075, _85077], _85075))], (2291 ^ _51060) ^ [] : [2285 ^ [_85075, _85077] = _85077]], 2292 ^ _51060 : [(2293 ^ _51060) ^ [] : [-(2285 ^ [_85075, _85077] = _85077)], (2295 ^ _51060) ^ [] : [in(2285 ^ [_85075, _85077], _85075)]]], (2268 ^ _51060) ^ [_84840, _84842] : [_84840 = singleton(_84842), 2271 ^ _51060 : [(2272 ^ _51060) ^ [_84919] : [in(_84919, _84840), -(_84919 = _84842)], (2278 ^ _51060) ^ [_84994] : [_84994 = _84842, -(in(_84994, _84840))]]], (2299 ^ _51060) ^ [_85317] : [relation(_85317), 2302 ^ _51060 : [(2325 ^ _51060) ^ [_85782, _85784] : [-(_85782 = fiber(_85317, _85784)), 2337 ^ _51060 : [(2338 ^ _51060) ^ [] : [2326 ^ [_85317, _85782, _85784] = _85784], (2340 ^ _51060) ^ [] : [-(in(ordered_pair(2326 ^ [_85317, _85782, _85784], _85784), _85317))], (2342 ^ _51060) ^ [] : [in(2326 ^ [_85317, _85782, _85784], _85782)]], 2329 ^ _51060 : [(2330 ^ _51060) ^ [] : [-(in(2326 ^ [_85317, _85782, _85784], _85782))], (2332 ^ _51060) ^ [] : [-(2326 ^ [_85317, _85782, _85784] = _85784), in(ordered_pair(2326 ^ [_85317, _85782, _85784], _85784), _85317)]]], (2303 ^ _51060) ^ [_85421, _85423] : [_85421 = fiber(_85317, _85423), 2306 ^ _51060 : [(2307 ^ _51060) ^ [_85515] : [in(_85515, _85421), 2310 ^ _51060 : [(2311 ^ _51060) ^ [] : [_85515 = _85423], (2313 ^ _51060) ^ [] : [-(in(ordered_pair(_85515, _85423), _85317))]]], (2315 ^ _51060) ^ [_85634] : [-(in(_85634, _85421)), -(_85634 = _85423), in(ordered_pair(_85634, _85423), _85317)]]]]], (2346 ^ _51060) ^ [_86166, _86168] : [relation(_86166), 2349 ^ _51060 : [(2376 ^ _51060) ^ [] : [-(_86166 = inclusion_relation(_86168)), relation_field(_86166) = _86168, 2383 ^ _51060 : [(2384 ^ _51060) ^ [] : [-(in(2381 ^ [_86166, _86168], _86168))], (2386 ^ _51060) ^ [] : [-(in(2382 ^ [_86166, _86168], _86168))], (2388 ^ _51060) ^ [] : [2389 ^ _51060 : [(2390 ^ _51060) ^ [] : [-(in(ordered_pair(2381 ^ [_86166, _86168], 2382 ^ [_86166, _86168]), _86166))], (2392 ^ _51060) ^ [] : [subset(2381 ^ [_86166, _86168], 2382 ^ [_86166, _86168])]], 2393 ^ _51060 : [(2394 ^ _51060) ^ [] : [-(subset(2381 ^ [_86166, _86168], 2382 ^ [_86166, _86168]))], (2396 ^ _51060) ^ [] : [in(ordered_pair(2381 ^ [_86166, _86168], 2382 ^ [_86166, _86168]), _86166)]]]]], (2350 ^ _51060) ^ [] : [_86166 = inclusion_relation(_86168), 2353 ^ _51060 : [(2354 ^ _51060) ^ [] : [-(relation_field(_86166) = _86168)], (2356 ^ _51060) ^ [_86341, _86343] : [in(_86343, _86168), in(_86341, _86168), 2363 ^ _51060 : [(2364 ^ _51060) ^ [] : [in(ordered_pair(_86343, _86341), _86166), -(subset(_86343, _86341))], (2370 ^ _51060) ^ [] : [subset(_86343, _86341), -(in(ordered_pair(_86343, _86341), _86166))]]]]]]], (2400 ^ _51060) ^ [_87029] : [_87029 = empty_set, 2403 ^ _51060 : [(2404 ^ _51060) ^ [_87090] : [in(_87090, _87029)]]], (2406 ^ _51060) ^ [_87111] : [-(in(2407 ^ [_87111], _87111)), -(_87111 = empty_set)], (2429 ^ _51060) ^ [_87402, _87404] : [-(_87402 = powerset(_87404)), 2433 ^ _51060 : [(2434 ^ _51060) ^ [] : [-(in(2430 ^ [_87402, _87404], _87402))], (2436 ^ _51060) ^ [] : [subset(2430 ^ [_87402, _87404], _87404)]], 2437 ^ _51060 : [(2438 ^ _51060) ^ [] : [-(subset(2430 ^ [_87402, _87404], _87404))], (2440 ^ _51060) ^ [] : [in(2430 ^ [_87402, _87404], _87402)]]], (2413 ^ _51060) ^ [_87167, _87169] : [_87167 = powerset(_87169), 2416 ^ _51060 : [(2417 ^ _51060) ^ [_87246] : [in(_87246, _87167), -(subset(_87246, _87169))], (2423 ^ _51060) ^ [_87321] : [subset(_87321, _87169), -(in(_87321, _87167))]]], (2444 ^ _51060) ^ [_87644] : [-(empty_carrier(_87644)), meet_semilatt_str(_87644), 2451 ^ _51060 : [(2452 ^ _51060) ^ [_87788] : [element(_87788, the_carrier(_87644)), 2455 ^ _51060 : [(2456 ^ _51060) ^ [_87876] : [element(_87876, the_carrier(_87644)), -(meet(_87644, _87788, _87876) = apply_binary_as_element(the_carrier(_87644), the_carrier(_87644), the_carrier(_87644), the_L_meet(_87644), _87788, _87876))]]]]], (2462 ^ _51060) ^ [_88007] : [2463 ^ _51060 : [(2464 ^ _51060) ^ [_88087, _88089] : [_88007 = ordered_pair(_88089, _88087)]], 2465 ^ _51060 : [(2476 ^ _51060) ^ [_88290] : [2479 ^ _51060 : [(2480 ^ _51060) ^ [] : [-(_88007 = ordered_pair(2477 ^ [_88007, _88290], 2478 ^ [_88007, _88290]))], (2482 ^ _51060) ^ [] : [_88290 = 2478 ^ [_88007, _88290]]], -(_88290 = pair_second(_88007))], (2466 ^ _51060) ^ [_88128] : [_88128 = pair_second(_88007), 2469 ^ _51060 : [(2470 ^ _51060) ^ [_88203, _88205] : [_88007 = ordered_pair(_88205, _88203), -(_88128 = _88203)]]]]], (2496 ^ _51060) ^ [_88609] : [2498 ^ _51060 : [(2499 ^ _51060) ^ [] : [-(in(2497 ^ [_88609], _88609))], (2501 ^ _51060) ^ [] : [subset(2497 ^ [_88609], _88609)]], -(epsilon_transitive(_88609))], (2486 ^ _51060) ^ [_88473] : [epsilon_transitive(_88473), 2489 ^ _51060 : [(2490 ^ _51060) ^ [_88532] : [in(_88532, _88473), -(subset(_88532, _88473))]]], (2505 ^ _51060) ^ [_88742] : [relation(_88742), 2508 ^ _51060 : [(2509 ^ _51060) ^ [_88828] : [relation(_88828), 2512 ^ _51060 : [(2529 ^ _51060) ^ [] : [-(_88742 = _88828), 2534 ^ _51060 : [(2535 ^ _51060) ^ [] : [-(in(ordered_pair(2530 ^ [_88742, _88828], 2531 ^ [_88742, _88828]), _88742))], (2537 ^ _51060) ^ [] : [in(ordered_pair(2530 ^ [_88742, _88828], 2531 ^ [_88742, _88828]), _88828)]], 2538 ^ _51060 : [(2539 ^ _51060) ^ [] : [-(in(ordered_pair(2530 ^ [_88742, _88828], 2531 ^ [_88742, _88828]), _88828))], (2541 ^ _51060) ^ [] : [in(ordered_pair(2530 ^ [_88742, _88828], 2531 ^ [_88742, _88828]), _88742)]]], (2513 ^ _51060) ^ [] : [_88742 = _88828, 2516 ^ _51060 : [(2517 ^ _51060) ^ [_88974, _88976] : [in(ordered_pair(_88976, _88974), _88742), -(in(ordered_pair(_88976, _88974), _88828))], (2523 ^ _51060) ^ [_89063, _89065] : [in(ordered_pair(_89065, _89063), _88828), -(in(ordered_pair(_89065, _89063), _88742))]]]]]]], (2545 ^ _51060) ^ [_89453, _89455] : [-(empty(_89455)), 2548 ^ _51060 : [(2549 ^ _51060) ^ [] : [element(_89453, _89455), -(in(_89453, _89455))], (2555 ^ _51060) ^ [] : [in(_89453, _89455), -(element(_89453, _89455))]]], (2561 ^ _51060) ^ [_89653, _89655] : [empty(_89655), 2564 ^ _51060 : [(2565 ^ _51060) ^ [] : [element(_89653, _89655), -(empty(_89653))], (2571 ^ _51060) ^ [] : [empty(_89653), -(element(_89653, _89655))]]], (2599 ^ _51060) ^ [_90175, _90177, _90179] : [-(_90175 = unordered_pair(_90179, _90177)), 2603 ^ _51060 : [(2604 ^ _51060) ^ [] : [-(in(2600 ^ [_90175, _90177, _90179], _90175))], (2606 ^ _51060) ^ [] : [2600 ^ [_90175, _90177, _90179] = _90179], (2608 ^ _51060) ^ [] : [2600 ^ [_90175, _90177, _90179] = _90177]], 2609 ^ _51060 : [(2616 ^ _51060) ^ [] : [in(2600 ^ [_90175, _90177, _90179], _90175)], (2610 ^ _51060) ^ [] : [-(2600 ^ [_90175, _90177, _90179] = _90179), -(2600 ^ [_90175, _90177, _90179] = _90177)]]], (2577 ^ _51060) ^ [_89875, _89877, _89879] : [_89875 = unordered_pair(_89879, _89877), 2580 ^ _51060 : [(2591 ^ _51060) ^ [_90054] : [2592 ^ _51060 : [(2593 ^ _51060) ^ [] : [_90054 = _89879], (2595 ^ _51060) ^ [] : [_90054 = _89877]], -(in(_90054, _89875))], (2581 ^ _51060) ^ [_89964] : [in(_89964, _89875), -(_89964 = _89879), -(_89964 = _89877)]]], (2620 ^ _51060) ^ [_90497] : [relation(_90497), 2623 ^ _51060 : [(2641 ^ _51060) ^ [] : [-(well_founded_relation(_90497)), 2643 ^ _51060 : [(2644 ^ _51060) ^ [] : [-(subset(2642 ^ [_90497], relation_field(_90497)))], (2646 ^ _51060) ^ [] : [2642 ^ [_90497] = empty_set], (2648 ^ _51060) ^ [_90918] : [in(_90918, 2642 ^ [_90497]), disjoint(fiber(_90497, _90918), 2642 ^ [_90497])]]], (2624 ^ _51060) ^ [] : [well_founded_relation(_90497), 2627 ^ _51060 : [(2628 ^ _51060) ^ [_90639] : [subset(_90639, relation_field(_90497)), -(_90639 = empty_set), 2636 ^ _51060 : [(2637 ^ _51060) ^ [] : [-(in(2635 ^ [_90497, _90639], _90639))], (2639 ^ _51060) ^ [] : [-(disjoint(fiber(_90497, 2635 ^ [_90497, _90639]), _90639))]]]]]]], (2678 ^ _51060) ^ [_91375, _91377, _91379] : [-(_91375 = set_union2(_91379, _91377)), 2682 ^ _51060 : [(2683 ^ _51060) ^ [] : [-(in(2679 ^ [_91375, _91377, _91379], _91375))], (2685 ^ _51060) ^ [] : [in(2679 ^ [_91375, _91377, _91379], _91379)], (2687 ^ _51060) ^ [] : [in(2679 ^ [_91375, _91377, _91379], _91377)]], 2688 ^ _51060 : [(2695 ^ _51060) ^ [] : [in(2679 ^ [_91375, _91377, _91379], _91375)], (2689 ^ _51060) ^ [] : [-(in(2679 ^ [_91375, _91377, _91379], _91379)), -(in(2679 ^ [_91375, _91377, _91379], _91377))]]], (2656 ^ _51060) ^ [_91075, _91077, _91079] : [_91075 = set_union2(_91079, _91077), 2659 ^ _51060 : [(2670 ^ _51060) ^ [_91254] : [2671 ^ _51060 : [(2672 ^ _51060) ^ [] : [in(_91254, _91079)], (2674 ^ _51060) ^ [] : [in(_91254, _91077)]], -(in(_91254, _91075))], (2660 ^ _51060) ^ [_91164] : [in(_91164, _91075), -(in(_91164, _91079)), -(in(_91164, _91077))]]], (2729 ^ _51060) ^ [_92248, _92250, _92252] : [-(_92248 = cartesian_product2(_92252, _92250)), 2747 ^ _51060 : [(2748 ^ _51060) ^ [] : [-(in(2745 ^ [_92248, _92250, _92252], _92252))], (2750 ^ _51060) ^ [] : [-(in(2746 ^ [_92248, _92250, _92252], _92250))], (2752 ^ _51060) ^ [] : [-(2730 ^ [_92248, _92250, _92252] = ordered_pair(2745 ^ [_92248, _92250, _92252], 2746 ^ [_92248, _92250, _92252]))], (2754 ^ _51060) ^ [] : [in(2730 ^ [_92248, _92250, _92252], _92248)]], 2733 ^ _51060 : [(2734 ^ _51060) ^ [] : [-(in(2730 ^ [_92248, _92250, _92252], _92248))], (2736 ^ _51060) ^ [_92418, _92420] : [in(_92420, _92252), in(_92418, _92250), 2730 ^ [_92248, _92250, _92252] = ordered_pair(_92420, _92418)]]], (2699 ^ _51060) ^ [_91715, _91717, _91719] : [_91715 = cartesian_product2(_91719, _91717), 2702 ^ _51060 : [(2703 ^ _51060) ^ [_91823] : [in(_91823, _91715), 2708 ^ _51060 : [(2709 ^ _51060) ^ [] : [-(in(2706 ^ [_91715, _91717, _91719, _91823], _91719))], (2711 ^ _51060) ^ [] : [-(in(2707 ^ [_91715, _91717, _91719, _91823], _91717))], (2713 ^ _51060) ^ [] : [-(_91823 = ordered_pair(2706 ^ [_91715, _91717, _91719, _91823], 2707 ^ [_91715, _91717, _91719, _91823]))]]], (2715 ^ _51060) ^ [_92010] : [-(in(_92010, _91715)), 2716 ^ _51060 : [(2717 ^ _51060) ^ [_92068, _92070] : [in(_92070, _91719), in(_92068, _91717), _92010 = ordered_pair(_92070, _92068)]]]]], (2758 ^ _51060) ^ [_92766] : [-(empty_carrier(_92766)), join_semilatt_str(_92766), 2765 ^ _51060 : [(2766 ^ _51060) ^ [_92902] : [element(_92902, the_carrier(_92766)), 2769 ^ _51060 : [(2770 ^ _51060) ^ [_92982] : [element(_92982, the_carrier(_92766)), 2773 ^ _51060 : [(2774 ^ _51060) ^ [] : [below(_92766, _92902, _92982), -(join(_92766, _92902, _92982) = _92982)], (2780 ^ _51060) ^ [] : [join(_92766, _92902, _92982) = _92982, -(below(_92766, _92902, _92982))]]]]]]], (2808 ^ _51060) ^ [_93491] : [2811 ^ _51060 : [(2812 ^ _51060) ^ [] : [-(in(2809 ^ [_93491], _93491))], (2814 ^ _51060) ^ [] : [-(in(2810 ^ [_93491], _93491))], (2816 ^ _51060) ^ [] : [in(2809 ^ [_93491], 2810 ^ [_93491])], (2818 ^ _51060) ^ [] : [2809 ^ [_93491] = 2810 ^ [_93491]], (2820 ^ _51060) ^ [] : [in(2810 ^ [_93491], 2809 ^ [_93491])]], -(epsilon_connected(_93491))], (2786 ^ _51060) ^ [_93236] : [epsilon_connected(_93236), 2789 ^ _51060 : [(2790 ^ _51060) ^ [_93326, _93328] : [in(_93328, _93236), in(_93326, _93236), -(in(_93328, _93326)), -(_93328 = _93326), -(in(_93326, _93328))]]], (2824 ^ _51060) ^ [_93805] : [one_sorted_str(_93805), -(cast_as_carrier_subset(_93805) = the_carrier(_93805))], (2830 ^ _51060) ^ [_93886] : [relation(_93886), 2833 ^ _51060 : [(2834 ^ _51060) ^ [_93972] : [relation(_93972), 2837 ^ _51060 : [(2848 ^ _51060) ^ [] : [2851 ^ _51060 : [(2852 ^ _51060) ^ [] : [-(in(ordered_pair(2849 ^ [_93886, _93972], 2850 ^ [_93886, _93972]), _93886))], (2854 ^ _51060) ^ [] : [in(ordered_pair(2849 ^ [_93886, _93972], 2850 ^ [_93886, _93972]), _93972)]], -(subset(_93886, _93972))], (2838 ^ _51060) ^ [] : [subset(_93886, _93972), 2841 ^ _51060 : [(2842 ^ _51060) ^ [_94103, _94105] : [in(ordered_pair(_94105, _94103), _93886), -(in(ordered_pair(_94105, _94103), _93972))]]]]]]], (2868 ^ _51060) ^ [_94516, _94518] : [2870 ^ _51060 : [(2871 ^ _51060) ^ [] : [-(in(2869 ^ [_94516, _94518], _94518))], (2873 ^ _51060) ^ [] : [in(2869 ^ [_94516, _94518], _94516)]], -(subset(_94518, _94516))], (2858 ^ _51060) ^ [_94374, _94376] : [subset(_94376, _94374), 2861 ^ _51060 : [(2862 ^ _51060) ^ [_94437] : [in(_94437, _94376), -(in(_94437, _94374))]]], (2877 ^ _51060) ^ [_94658] : [relation(_94658), 2880 ^ _51060 : [(2898 ^ _51060) ^ [_95023] : [-(is_well_founded_in(_94658, _95023)), 2900 ^ _51060 : [(2901 ^ _51060) ^ [] : [-(subset(2899 ^ [_94658, _95023], _95023))], (2903 ^ _51060) ^ [] : [2899 ^ [_94658, _95023] = empty_set], (2905 ^ _51060) ^ [_95186] : [in(_95186, 2899 ^ [_94658, _95023]), disjoint(fiber(_94658, _95186), 2899 ^ [_94658, _95023])]]], (2881 ^ _51060) ^ [_94766] : [is_well_founded_in(_94658, _94766), 2884 ^ _51060 : [(2885 ^ _51060) ^ [_94855] : [subset(_94855, _94766), -(_94855 = empty_set), 2893 ^ _51060 : [(2894 ^ _51060) ^ [] : [-(in(2892 ^ [_94658, _94766, _94855], _94855))], (2896 ^ _51060) ^ [] : [-(disjoint(fiber(_94658, 2892 ^ [_94658, _94766, _94855]), _94855))]]]]]]], (2935 ^ _51060) ^ [_95685, _95687, _95689] : [-(_95685 = set_intersection2(_95689, _95687)), 2947 ^ _51060 : [(2948 ^ _51060) ^ [] : [-(in(2936 ^ [_95685, _95687, _95689], _95689))], (2950 ^ _51060) ^ [] : [-(in(2936 ^ [_95685, _95687, _95689], _95687))], (2952 ^ _51060) ^ [] : [in(2936 ^ [_95685, _95687, _95689], _95685)]], 2939 ^ _51060 : [(2940 ^ _51060) ^ [] : [-(in(2936 ^ [_95685, _95687, _95689], _95685))], (2942 ^ _51060) ^ [] : [in(2936 ^ [_95685, _95687, _95689], _95689), in(2936 ^ [_95685, _95687, _95689], _95687)]]], (2913 ^ _51060) ^ [_95354, _95356, _95358] : [_95354 = set_intersection2(_95358, _95356), 2916 ^ _51060 : [(2917 ^ _51060) ^ [_95443] : [in(_95443, _95354), 2920 ^ _51060 : [(2921 ^ _51060) ^ [] : [-(in(_95443, _95358))], (2923 ^ _51060) ^ [] : [-(in(_95443, _95356))]]], (2925 ^ _51060) ^ [_95546] : [-(in(_95546, _95354)), in(_95546, _95358), in(_95546, _95356)]]], (2956 ^ _51060) ^ [_96039] : [relation(_96039), function(_96039), 2963 ^ _51060 : [(2964 ^ _51060) ^ [_96199, _96201] : [in(_96201, relation_dom(_96039)), 2967 ^ _51060 : [(2968 ^ _51060) ^ [] : [_96199 = apply(_96039, _96201), -(in(ordered_pair(_96201, _96199), _96039))], (2974 ^ _51060) ^ [] : [in(ordered_pair(_96201, _96199), _96039), -(_96199 = apply(_96039, _96201))]]], (2980 ^ _51060) ^ [_96429, _96431] : [-(in(_96431, relation_dom(_96039))), 2983 ^ _51060 : [(2984 ^ _51060) ^ [] : [_96429 = apply(_96039, _96431), -(_96429 = empty_set)], (2990 ^ _51060) ^ [] : [_96429 = empty_set, -(_96429 = apply(_96039, _96431))]]]]], (2996 ^ _51060) ^ [_96672] : [ordinal(_96672), 2999 ^ _51060 : [(3000 ^ _51060) ^ [] : [-(epsilon_transitive(_96672))], (3002 ^ _51060) ^ [] : [-(epsilon_connected(_96672))]]], (3004 ^ _51060) ^ [_96763] : [-(ordinal(_96763)), epsilon_transitive(_96763), epsilon_connected(_96763)], (3014 ^ _51060) ^ [_96884] : [relation(_96884), 3017 ^ _51060 : [(3035 ^ _51060) ^ [_97258] : [-(_97258 = relation_dom(_96884)), 3039 ^ _51060 : [(3040 ^ _51060) ^ [] : [-(in(3036 ^ [_96884, _97258], _97258))], (3042 ^ _51060) ^ [_97392] : [in(ordered_pair(3036 ^ [_96884, _97258], _97392), _96884)]], 3044 ^ _51060 : [(3045 ^ _51060) ^ [] : [-(in(ordered_pair(3036 ^ [_96884, _97258], 3043 ^ [_96884, _97258]), _96884))], (3047 ^ _51060) ^ [] : [in(3036 ^ [_96884, _97258], _97258)]]], (3018 ^ _51060) ^ [_96976] : [_96976 = relation_dom(_96884), 3021 ^ _51060 : [(3022 ^ _51060) ^ [_97063] : [in(_97063, _96976), -(in(ordered_pair(_97063, 3025 ^ [_96884, _96976, _97063]), _96884))], (3029 ^ _51060) ^ [_97158] : [3030 ^ _51060 : [(3031 ^ _51060) ^ [_97202] : [in(ordered_pair(_97158, _97202), _96884)]], -(in(_97158, _96976))]]]]], (3051 ^ _51060) ^ [_97539] : [relation(_97539), 3054 ^ _51060 : [(3077 ^ _51060) ^ [_98003] : [3080 ^ _51060 : [(3081 ^ _51060) ^ [] : [-(in(3078 ^ [_97539, _98003], _98003))], (3083 ^ _51060) ^ [] : [-(in(3079 ^ [_97539, _98003], _98003))], (3085 ^ _51060) ^ [] : [-(in(ordered_pair(3078 ^ [_97539, _98003], 3079 ^ [_97539, _98003]), _97539))], (3087 ^ _51060) ^ [] : [-(in(ordered_pair(3079 ^ [_97539, _98003], 3078 ^ [_97539, _98003]), _97539))], (3089 ^ _51060) ^ [] : [3078 ^ [_97539, _98003] = 3079 ^ [_97539, _98003]]], -(is_antisymmetric_in(_97539, _98003))], (3055 ^ _51060) ^ [_97650] : [is_antisymmetric_in(_97539, _97650), 3058 ^ _51060 : [(3059 ^ _51060) ^ [_97742, _97744] : [-(_97744 = _97742), in(_97744, _97650), in(_97742, _97650), in(ordered_pair(_97744, _97742), _97539), in(ordered_pair(_97742, _97744), _97539)]]]]], (3093 ^ _51060) ^ [_98295] : [-(cast_to_subset(_98295) = _98295)], (3118 ^ _51060) ^ [_98701, _98703] : [-(_98701 = union(_98703)), 3131 ^ _51060 : [(3132 ^ _51060) ^ [] : [-(in(3119 ^ [_98701, _98703], 3130 ^ [_98701, _98703]))], (3134 ^ _51060) ^ [] : [-(in(3130 ^ [_98701, _98703], _98703))], (3136 ^ _51060) ^ [] : [in(3119 ^ [_98701, _98703], _98701)]], 3122 ^ _51060 : [(3123 ^ _51060) ^ [] : [-(in(3119 ^ [_98701, _98703], _98701))], (3125 ^ _51060) ^ [_98834] : [in(3119 ^ [_98701, _98703], _98834), in(_98834, _98703)]]], (3095 ^ _51060) ^ [_98335, _98337] : [_98335 = union(_98337), 3098 ^ _51060 : [(3099 ^ _51060) ^ [_98425] : [in(_98425, _98335), 3103 ^ _51060 : [(3104 ^ _51060) ^ [] : [-(in(_98425, 3102 ^ [_98335, _98337, _98425]))], (3106 ^ _51060) ^ [] : [-(in(3102 ^ [_98335, _98337, _98425], _98337))]]], (3108 ^ _51060) ^ [_98549] : [-(in(_98549, _98335)), 3109 ^ _51060 : [(3110 ^ _51060) ^ [_98591] : [in(_98549, _98591), in(_98591, _98337)]]]]], (3140 ^ _51060) ^ [_99060] : [relation(_99060), 3143 ^ _51060 : [(3144 ^ _51060) ^ [] : [well_ordering(_99060), 3147 ^ _51060 : [(3148 ^ _51060) ^ [] : [-(reflexive(_99060))], (3150 ^ _51060) ^ [] : [-(transitive(_99060))], (3152 ^ _51060) ^ [] : [-(antisymmetric(_99060))], (3154 ^ _51060) ^ [] : [-(connected(_99060))], (3156 ^ _51060) ^ [] : [-(well_founded_relation(_99060))]]], (3158 ^ _51060) ^ [] : [-(well_ordering(_99060)), reflexive(_99060), transitive(_99060), antisymmetric(_99060), connected(_99060), well_founded_relation(_99060)]]], (3180 ^ _51060) ^ [_99530, _99532] : [equipotent(_99532, _99530), 3184 ^ _51060 : [(3185 ^ _51060) ^ [] : [-(relation(3183 ^ [_99530, _99532]))], (3187 ^ _51060) ^ [] : [-(function(3183 ^ [_99530, _99532]))], (3189 ^ _51060) ^ [] : [-(one_to_one(3183 ^ [_99530, _99532]))], (3191 ^ _51060) ^ [] : [-(relation_dom(3183 ^ [_99530, _99532]) = _99532)], (3193 ^ _51060) ^ [] : [-(relation_rng(3183 ^ [_99530, _99532]) = _99530)]]], (3195 ^ _51060) ^ [_99743, _99745] : [-(equipotent(_99745, _99743)), 3196 ^ _51060 : [(3197 ^ _51060) ^ [_99802] : [relation(_99802), function(_99802), one_to_one(_99802), relation_dom(_99802) = _99745, relation_rng(_99802) = _99743]]], (3239 ^ _51060) ^ [_100436, _100438, _100440] : [-(_100436 = set_difference(_100440, _100438)), 3251 ^ _51060 : [(3252 ^ _51060) ^ [] : [-(in(3240 ^ [_100436, _100438, _100440], _100440))], (3254 ^ _51060) ^ [] : [in(3240 ^ [_100436, _100438, _100440], _100438)], (3256 ^ _51060) ^ [] : [in(3240 ^ [_100436, _100438, _100440], _100436)]], 3243 ^ _51060 : [(3244 ^ _51060) ^ [] : [-(in(3240 ^ [_100436, _100438, _100440], _100436))], (3246 ^ _51060) ^ [] : [in(3240 ^ [_100436, _100438, _100440], _100440), -(in(3240 ^ [_100436, _100438, _100440], _100438))]]], (3217 ^ _51060) ^ [_100092, _100094, _100096] : [_100092 = set_difference(_100096, _100094), 3220 ^ _51060 : [(3221 ^ _51060) ^ [_100183] : [in(_100183, _100092), 3224 ^ _51060 : [(3225 ^ _51060) ^ [] : [-(in(_100183, _100096))], (3227 ^ _51060) ^ [] : [in(_100183, _100094)]]], (3229 ^ _51060) ^ [_100294] : [-(in(_100294, _100092)), in(_100294, _100096), -(in(_100294, _100094))]]], (3260 ^ _51060) ^ [_100802] : [relation(_100802), function(_100802), 3267 ^ _51060 : [(3291 ^ _51060) ^ [_101346] : [-(_101346 = relation_rng(_100802)), 3304 ^ _51060 : [(3305 ^ _51060) ^ [] : [-(in(3303 ^ [_100802, _101346], relation_dom(_100802)))], (3307 ^ _51060) ^ [] : [-(3292 ^ [_100802, _101346] = apply(_100802, 3303 ^ [_100802, _101346]))], (3309 ^ _51060) ^ [] : [in(3292 ^ [_100802, _101346], _101346)]], 3295 ^ _51060 : [(3296 ^ _51060) ^ [] : [-(in(3292 ^ [_100802, _101346], _101346))], (3298 ^ _51060) ^ [_101489] : [in(_101489, relation_dom(_100802)), 3292 ^ [_100802, _101346] = apply(_100802, _101489)]]], (3268 ^ _51060) ^ [_100950] : [_100950 = relation_rng(_100802), 3271 ^ _51060 : [(3272 ^ _51060) ^ [_101045] : [in(_101045, _100950), 3276 ^ _51060 : [(3277 ^ _51060) ^ [] : [-(in(3275 ^ [_100802, _100950, _101045], relation_dom(_100802)))], (3279 ^ _51060) ^ [] : [-(_101045 = apply(_100802, 3275 ^ [_100802, _100950, _101045]))]]], (3281 ^ _51060) ^ [_101179] : [-(in(_101179, _100950)), 3282 ^ _51060 : [(3283 ^ _51060) ^ [_101226] : [in(_101226, relation_dom(_100802)), _101179 = apply(_100802, _101226)]]]]]]], (3313 ^ _51060) ^ [_101748] : [_101748 = omega, 3316 ^ _51060 : [(3317 ^ _51060) ^ [] : [-(in(empty_set, _101748))], (3319 ^ _51060) ^ [] : [-(being_limit_ordinal(_101748))], (3321 ^ _51060) ^ [] : [-(ordinal(_101748))], (3323 ^ _51060) ^ [_101896] : [ordinal(_101896), -(subset(_101748, _101896)), in(empty_set, _101896), being_limit_ordinal(_101896)]]], (3337 ^ _51060) ^ [_102079] : [-(_102079 = omega), in(empty_set, _102079), being_limit_ordinal(_102079), ordinal(_102079), 3351 ^ _51060 : [(3352 ^ _51060) ^ [] : [-(ordinal(3350 ^ [_102079]))], (3354 ^ _51060) ^ [] : [-(in(empty_set, 3350 ^ [_102079]))], (3356 ^ _51060) ^ [] : [-(being_limit_ordinal(3350 ^ [_102079]))], (3358 ^ _51060) ^ [] : [subset(_102079, 3350 ^ [_102079])]]], (3362 ^ _51060) ^ [_102431] : [relation(_102431), 3365 ^ _51060 : [(3383 ^ _51060) ^ [_102805] : [-(_102805 = relation_rng(_102431)), 3387 ^ _51060 : [(3388 ^ _51060) ^ [] : [-(in(3384 ^ [_102431, _102805], _102805))], (3390 ^ _51060) ^ [_102939] : [in(ordered_pair(_102939, 3384 ^ [_102431, _102805]), _102431)]], 3392 ^ _51060 : [(3393 ^ _51060) ^ [] : [-(in(ordered_pair(3391 ^ [_102431, _102805], 3384 ^ [_102431, _102805]), _102431))], (3395 ^ _51060) ^ [] : [in(3384 ^ [_102431, _102805], _102805)]]], (3366 ^ _51060) ^ [_102523] : [_102523 = relation_rng(_102431), 3369 ^ _51060 : [(3370 ^ _51060) ^ [_102610] : [in(_102610, _102523), -(in(ordered_pair(3373 ^ [_102431, _102523, _102610], _102610), _102431))], (3377 ^ _51060) ^ [_102705] : [3378 ^ _51060 : [(3379 ^ _51060) ^ [_102749] : [in(ordered_pair(_102749, _102705), _102431)]], -(in(_102705, _102523))]]]]], (3399 ^ _51060) ^ [_103086, _103088] : [element(_103086, powerset(_103088)), -(subset_complement(_103088, _103086) = set_difference(_103088, _103086))], (3405 ^ _51060) ^ [_103179, _103181] : [-(ordered_pair(_103181, _103179) = unordered_pair(unordered_pair(_103181, _103179), singleton(_103181)))], (3407 ^ _51060) ^ [_103215] : [relation(_103215), 3410 ^ _51060 : [(3411 ^ _51060) ^ [_103310] : [well_orders(_103215, _103310), 3414 ^ _51060 : [(3415 ^ _51060) ^ [] : [-(is_reflexive_in(_103215, _103310))], (3417 ^ _51060) ^ [] : [-(is_transitive_in(_103215, _103310))], (3419 ^ _51060) ^ [] : [-(is_antisymmetric_in(_103215, _103310))], (3421 ^ _51060) ^ [] : [-(is_connected_in(_103215, _103310))], (3423 ^ _51060) ^ [] : [-(is_well_founded_in(_103215, _103310))]]], (3425 ^ _51060) ^ [_103481] : [-(well_orders(_103215, _103481)), is_reflexive_in(_103215, _103481), is_transitive_in(_103215, _103481), is_antisymmetric_in(_103215, _103481), is_connected_in(_103215, _103481), is_well_founded_in(_103215, _103481)]]], (3447 ^ _51060) ^ [_103784] : [being_limit_ordinal(_103784), -(_103784 = union(_103784))], (3453 ^ _51060) ^ [_103857] : [_103857 = union(_103857), -(being_limit_ordinal(_103857))], (3459 ^ _51060) ^ [_103936] : [relation(_103936), -(relation_field(_103936) = set_union2(relation_dom(_103936), relation_rng(_103936)))], (3465 ^ _51060) ^ [_104027] : [relation(_104027), 3468 ^ _51060 : [(3491 ^ _51060) ^ [_104427] : [3494 ^ _51060 : [(3495 ^ _51060) ^ [] : [-(in(3492 ^ [_104027, _104427], _104427))], (3497 ^ _51060) ^ [] : [-(in(3493 ^ [_104027, _104427], _104427))], (3499 ^ _51060) ^ [] : [3492 ^ [_104027, _104427] = 3493 ^ [_104027, _104427]], (3501 ^ _51060) ^ [] : [in(ordered_pair(3492 ^ [_104027, _104427], 3493 ^ [_104027, _104427]), _104027)], (3503 ^ _51060) ^ [] : [in(ordered_pair(3493 ^ [_104027, _104427], 3492 ^ [_104027, _104427]), _104027)]], -(is_connected_in(_104027, _104427))], (3469 ^ _51060) ^ [_104146] : [is_connected_in(_104027, _104146), 3472 ^ _51060 : [(3473 ^ _51060) ^ [_104246, _104248] : [in(_104248, _104146), in(_104246, _104146), -(_104248 = _104246), -(in(ordered_pair(_104248, _104246), _104027)), -(in(ordered_pair(_104246, _104248), _104027))]]]]], (3507 ^ _51060) ^ [_104792] : [relation(_104792), 3510 ^ _51060 : [(3511 ^ _51060) ^ [_104856] : [-(relation_restriction(_104792, _104856) = set_intersection2(_104792, cartesian_product2(_104856, _104856)))]]], (3513 ^ _51060) ^ [_104892] : [relation(_104892), 3516 ^ _51060 : [(3517 ^ _51060) ^ [_104980] : [relation(_104980), 3520 ^ _51060 : [(3537 ^ _51060) ^ [] : [-(_104980 = relation_inverse(_104892)), 3542 ^ _51060 : [(3543 ^ _51060) ^ [] : [-(in(ordered_pair(3538 ^ [_104892, _104980], 3539 ^ [_104892, _104980]), _104980))], (3545 ^ _51060) ^ [] : [in(ordered_pair(3539 ^ [_104892, _104980], 3538 ^ [_104892, _104980]), _104892)]], 3546 ^ _51060 : [(3547 ^ _51060) ^ [] : [-(in(ordered_pair(3539 ^ [_104892, _104980], 3538 ^ [_104892, _104980]), _104892))], (3549 ^ _51060) ^ [] : [in(ordered_pair(3538 ^ [_104892, _104980], 3539 ^ [_104892, _104980]), _104980)]]], (3521 ^ _51060) ^ [] : [_104980 = relation_inverse(_104892), 3524 ^ _51060 : [(3525 ^ _51060) ^ [_105130, _105132] : [in(ordered_pair(_105132, _105130), _104980), -(in(ordered_pair(_105130, _105132), _104892))], (3531 ^ _51060) ^ [_105219, _105221] : [in(ordered_pair(_105219, _105221), _104892), -(in(ordered_pair(_105221, _105219), _104980))]]]]]]], (3553 ^ _51060) ^ [_105603] : [relation(_105603), 3556 ^ _51060 : [(3557 ^ _51060) ^ [_105752] : [relation(_105752), 3560 ^ _51060 : [(3561 ^ _51060) ^ [_105893] : [relation(_105893), function(_105893), 3568 ^ _51060 : [(3603 ^ _51060) ^ [] : [-(relation_isomorphism(_105603, _105752, _105893)), relation_dom(_105893) = relation_field(_105603), relation_rng(_105893) = relation_field(_105752), one_to_one(_105893), 3632 ^ _51060 : [(3633 ^ _51060) ^ [] : [-(in(3616 ^ [_105603, _105752, _105893], relation_field(_105603)))], (3635 ^ _51060) ^ [] : [-(in(3617 ^ [_105603, _105752, _105893], relation_field(_105603)))], (3637 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_105893, 3616 ^ [_105603, _105752, _105893]), apply(_105893, 3617 ^ [_105603, _105752, _105893])), _105752))], (3639 ^ _51060) ^ [] : [in(ordered_pair(3616 ^ [_105603, _105752, _105893], 3617 ^ [_105603, _105752, _105893]), _105603)]], 3620 ^ _51060 : [(3621 ^ _51060) ^ [] : [-(in(ordered_pair(3616 ^ [_105603, _105752, _105893], 3617 ^ [_105603, _105752, _105893]), _105603))], (3623 ^ _51060) ^ [] : [in(3616 ^ [_105603, _105752, _105893], relation_field(_105603)), in(3617 ^ [_105603, _105752, _105893], relation_field(_105603)), in(ordered_pair(apply(_105893, 3616 ^ [_105603, _105752, _105893]), apply(_105893, 3617 ^ [_105603, _105752, _105893])), _105752)]]], (3569 ^ _51060) ^ [] : [relation_isomorphism(_105603, _105752, _105893), 3572 ^ _51060 : [(3573 ^ _51060) ^ [] : [-(relation_dom(_105893) = relation_field(_105603))], (3575 ^ _51060) ^ [] : [-(relation_rng(_105893) = relation_field(_105752))], (3577 ^ _51060) ^ [] : [-(one_to_one(_105893))], (3579 ^ _51060) ^ [_106215, _106217] : [in(ordered_pair(_106217, _106215), _105603), 3582 ^ _51060 : [(3583 ^ _51060) ^ [] : [-(in(_106217, relation_field(_105603)))], (3585 ^ _51060) ^ [] : [-(in(_106215, relation_field(_105603)))], (3587 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_105893, _106217), apply(_105893, _106215)), _105752))]]], (3589 ^ _51060) ^ [_106376, _106378] : [-(in(ordered_pair(_106378, _106376), _105603)), in(_106378, relation_field(_105603)), in(_106376, relation_field(_105603)), in(ordered_pair(apply(_105893, _106378), apply(_105893, _106376)), _105752)]]]]]]]]], (3643 ^ _51060) ^ [_107322, _107324] : [disjoint(_107324, _107322), -(set_intersection2(_107324, _107322) = empty_set)], (3649 ^ _51060) ^ [_107401, _107403] : [set_intersection2(_107403, _107401) = empty_set, -(disjoint(_107403, _107401))], (3655 ^ _51060) ^ [_107486] : [relation(_107486), function(_107486), 3662 ^ _51060 : [(3681 ^ _51060) ^ [] : [3684 ^ _51060 : [(3685 ^ _51060) ^ [] : [-(in(3682 ^ [_107486], relation_dom(_107486)))], (3687 ^ _51060) ^ [] : [-(in(3683 ^ [_107486], relation_dom(_107486)))], (3689 ^ _51060) ^ [] : [-(apply(_107486, 3682 ^ [_107486]) = apply(_107486, 3683 ^ [_107486]))], (3691 ^ _51060) ^ [] : [3682 ^ [_107486] = 3683 ^ [_107486]]], -(one_to_one(_107486))], (3663 ^ _51060) ^ [] : [one_to_one(_107486), 3666 ^ _51060 : [(3667 ^ _51060) ^ [_107675, _107677] : [-(_107677 = _107675), in(_107677, relation_dom(_107486)), in(_107675, relation_dom(_107486)), apply(_107486, _107677) = apply(_107486, _107675)]]]]], (3695 ^ _51060) ^ [_108078] : [-(empty_carrier(_108078)), latt_str(_108078), 3702 ^ _51060 : [(3717 ^ _51060) ^ [] : [3719 ^ _51060 : [(3720 ^ _51060) ^ [] : [-(element(3718 ^ [_108078], the_carrier(_108078)))], (3723 ^ _51060) ^ [] : [-(element(3721 ^ [_108078], the_carrier(_108078)))], (3725 ^ _51060) ^ [] : [join(_108078, meet(_108078, 3718 ^ [_108078], 3721 ^ [_108078]), 3721 ^ [_108078]) = 3721 ^ [_108078]]], -(meet_absorbing(_108078))], (3703 ^ _51060) ^ [] : [meet_absorbing(_108078), 3706 ^ _51060 : [(3707 ^ _51060) ^ [_108266] : [element(_108266, the_carrier(_108078)), 3710 ^ _51060 : [(3711 ^ _51060) ^ [_108343] : [element(_108343, the_carrier(_108078)), -(join(_108078, meet(_108078, _108266, _108343), _108343) = _108343)]]]]]]], (3729 ^ _51060) ^ [_108666] : [relation(_108666), 3732 ^ _51060 : [(3733 ^ _51060) ^ [_108779] : [relation(_108779), 3736 ^ _51060 : [(3737 ^ _51060) ^ [_108884] : [relation(_108884), 3740 ^ _51060 : [(3764 ^ _51060) ^ [] : [-(_108884 = relation_composition(_108666, _108779)), 3778 ^ _51060 : [(3779 ^ _51060) ^ [] : [-(in(ordered_pair(3765 ^ [_108666, _108779, _108884], 3777 ^ [_108666, _108779, _108884]), _108666))], (3781 ^ _51060) ^ [] : [-(in(ordered_pair(3777 ^ [_108666, _108779, _108884], 3766 ^ [_108666, _108779, _108884]), _108779))], (3783 ^ _51060) ^ [] : [in(ordered_pair(3765 ^ [_108666, _108779, _108884], 3766 ^ [_108666, _108779, _108884]), _108884)]], 3769 ^ _51060 : [(3770 ^ _51060) ^ [] : [-(in(ordered_pair(3765 ^ [_108666, _108779, _108884], 3766 ^ [_108666, _108779, _108884]), _108884))], (3772 ^ _51060) ^ [_109540] : [in(ordered_pair(3765 ^ [_108666, _108779, _108884], _109540), _108666), in(ordered_pair(_109540, 3766 ^ [_108666, _108779, _108884]), _108779)]]], (3741 ^ _51060) ^ [] : [_108884 = relation_composition(_108666, _108779), 3744 ^ _51060 : [(3745 ^ _51060) ^ [_109054, _109056] : [in(ordered_pair(_109056, _109054), _108884), 3749 ^ _51060 : [(3750 ^ _51060) ^ [] : [-(in(ordered_pair(_109056, 3748 ^ [_108666, _108779, _108884, _109054, _109056]), _108666))], (3752 ^ _51060) ^ [] : [-(in(ordered_pair(3748 ^ [_108666, _108779, _108884, _109054, _109056], _109054), _108779))]]], (3754 ^ _51060) ^ [_109208, _109210] : [-(in(ordered_pair(_109210, _109208), _108884)), 3755 ^ _51060 : [(3756 ^ _51060) ^ [_109263] : [in(ordered_pair(_109210, _109263), _108666), in(ordered_pair(_109263, _109208), _108779)]]]]]]]]]]], (3787 ^ _51060) ^ [_109850] : [relation(_109850), 3790 ^ _51060 : [(3817 ^ _51060) ^ [_110414] : [3821 ^ _51060 : [(3822 ^ _51060) ^ [] : [-(in(3818 ^ [_109850, _110414], _110414))], (3824 ^ _51060) ^ [] : [-(in(3819 ^ [_109850, _110414], _110414))], (3826 ^ _51060) ^ [] : [-(in(3820 ^ [_109850, _110414], _110414))], (3828 ^ _51060) ^ [] : [-(in(ordered_pair(3818 ^ [_109850, _110414], 3819 ^ [_109850, _110414]), _109850))], (3830 ^ _51060) ^ [] : [-(in(ordered_pair(3819 ^ [_109850, _110414], 3820 ^ [_109850, _110414]), _109850))], (3832 ^ _51060) ^ [] : [in(ordered_pair(3818 ^ [_109850, _110414], 3820 ^ [_109850, _110414]), _109850)]], -(is_transitive_in(_109850, _110414))], (3791 ^ _51060) ^ [_109975] : [is_transitive_in(_109850, _109975), 3794 ^ _51060 : [(3795 ^ _51060) ^ [_110081, _110083, _110085] : [-(in(ordered_pair(_110085, _110081), _109850)), in(_110085, _109975), in(_110083, _109975), in(_110081, _109975), in(ordered_pair(_110085, _110083), _109850), in(ordered_pair(_110083, _110081), _109850)]]]]], (3836 ^ _51060) ^ [_110753, _110755] : [element(_110753, powerset(powerset(_110755))), 3839 ^ _51060 : [(3840 ^ _51060) ^ [_110859] : [element(_110859, powerset(powerset(_110755))), 3843 ^ _51060 : [(3864 ^ _51060) ^ [] : [-(_110859 = complements_of_subsets(_110755, _110753)), 3866 ^ _51060 : [(3867 ^ _51060) ^ [] : [-(element(3865 ^ [_110753, _110755, _110859], powerset(_110755)))], (3869 ^ _51060) ^ [] : [3870 ^ _51060 : [(3871 ^ _51060) ^ [] : [-(in(3865 ^ [_110753, _110755, _110859], _110859))], (3873 ^ _51060) ^ [] : [in(subset_complement(_110755, 3865 ^ [_110753, _110755, _110859]), _110753)]], 3874 ^ _51060 : [(3875 ^ _51060) ^ [] : [-(in(subset_complement(_110755, 3865 ^ [_110753, _110755, _110859]), _110753))], (3877 ^ _51060) ^ [] : [in(3865 ^ [_110753, _110755, _110859], _110859)]]]]], (3844 ^ _51060) ^ [] : [_110859 = complements_of_subsets(_110755, _110753), 3847 ^ _51060 : [(3848 ^ _51060) ^ [_111010] : [element(_111010, powerset(_110755)), 3851 ^ _51060 : [(3852 ^ _51060) ^ [] : [in(_111010, _110859), -(in(subset_complement(_110755, _111010), _110753))], (3858 ^ _51060) ^ [] : [in(subset_complement(_110755, _111010), _110753), -(in(_111010, _110859))]]]]]]]]], (3881 ^ _51060) ^ [_111550, _111552] : [proper_subset(_111552, _111550), 3884 ^ _51060 : [(3885 ^ _51060) ^ [] : [-(subset(_111552, _111550))], (3887 ^ _51060) ^ [] : [_111552 = _111550]]], (3889 ^ _51060) ^ [_111657, _111659] : [-(proper_subset(_111659, _111657)), subset(_111659, _111657), -(_111659 = _111657)], (3899 ^ _51060) ^ [_111791] : [relation(_111791), function(_111791), one_to_one(_111791), -(function_inverse(_111791) = relation_inverse(_111791))], (3913 ^ _51060) ^ [_111970] : [relation(_111970), 3916 ^ _51060 : [(3917 ^ _51060) ^ [] : [reflexive(_111970), -(is_reflexive_in(_111970, relation_field(_111970)))], (3923 ^ _51060) ^ [] : [is_reflexive_in(_111970, relation_field(_111970)), -(reflexive(_111970))]]], (3929 ^ _51060) ^ [] : [true___, -(true___)], (3935 ^ _51060) ^ [] : [true___, -(true___)], (3941 ^ _51060) ^ [] : [true___, -(true___)], (3947 ^ _51060) ^ [] : [true___, -(true___)], (3953 ^ _51060) ^ [_112408, _112410, _112412] : [-(element(join(_112412, _112410, _112408), the_carrier(_112412))), -(empty_carrier(_112412)), join_semilatt_str(_112412), element(_112410, the_carrier(_112412)), element(_112408, the_carrier(_112412))], (3971 ^ _51060) ^ [] : [true___, -(true___)], (3977 ^ _51060) ^ [] : [true___, -(true___)], (3983 ^ _51060) ^ [] : [true___, -(true___)], (3989 ^ _51060) ^ [] : [true___, -(true___)], (3995 ^ _51060) ^ [] : [true___, -(true___)], (4001 ^ _51060) ^ [] : [true___, -(true___)], (4007 ^ _51060) ^ [_113022] : [-(relation(inclusion_relation(_113022)))], (4009 ^ _51060) ^ [] : [true___, -(true___)], (4015 ^ _51060) ^ [] : [true___, -(true___)], (4021 ^ _51060) ^ [_113164, _113166, _113168, _113170, _113172, _113174] : [-(element(apply_binary_as_element(_113174, _113172, _113170, _113168, _113166, _113164), _113170)), -(empty(_113174)), -(empty(_113172)), function(_113168), quasi_total(_113168, cartesian_product2(_113174, _113172), _113170), relation_of2(_113168, cartesian_product2(_113174, _113172), _113170), element(_113166, _113174), element(_113164, _113172)], (4051 ^ _51060) ^ [_113639] : [4058 ^ _51060 : [(4059 ^ _51060) ^ [] : [-(relation(function_inverse(_113639)))], (4061 ^ _51060) ^ [] : [-(function(function_inverse(_113639)))]], relation(_113639), function(_113639)], (4063 ^ _51060) ^ [_113790, _113792, _113794] : [-(element(meet(_113794, _113792, _113790), the_carrier(_113794))), -(empty_carrier(_113794)), meet_semilatt_str(_113794), element(_113792, the_carrier(_113794)), element(_113790, the_carrier(_113794))], (4081 ^ _51060) ^ [] : [true___, -(true___)], (4087 ^ _51060) ^ [_114109] : [one_sorted_str(_114109), -(element(cast_as_carrier_subset(_114109), powerset(the_carrier(_114109))))], (4093 ^ _51060) ^ [] : [true___, -(true___)], (4099 ^ _51060) ^ [_114253] : [-(element(cast_to_subset(_114253), powerset(_114253)))], (4101 ^ _51060) ^ [] : [true___, -(true___)], (4107 ^ _51060) ^ [_114339, _114341] : [relation(_114341), -(relation(relation_restriction(_114341, _114339)))], (4113 ^ _51060) ^ [] : [true___, -(true___)], (4119 ^ _51060) ^ [] : [true___, -(true___)], (4125 ^ _51060) ^ [_114536, _114538, _114540] : [-(element(join_commut(_114540, _114538, _114536), the_carrier(_114540))), -(empty_carrier(_114540)), join_commutative(_114540), join_semilatt_str(_114540), element(_114538, the_carrier(_114540)), element(_114536, the_carrier(_114540))], (4147 ^ _51060) ^ [] : [true___, -(true___)], (4153 ^ _51060) ^ [_114907, _114909] : [element(_114907, powerset(_114909)), -(element(subset_complement(_114909, _114907), powerset(_114909)))], (4159 ^ _51060) ^ [] : [true___, -(true___)], (4165 ^ _51060) ^ [] : [true___, -(true___)], (4171 ^ _51060) ^ [_115116, _115118, _115120] : [-(element(meet_commut(_115120, _115118, _115116), the_carrier(_115120))), -(empty_carrier(_115120)), meet_commutative(_115120), meet_semilatt_str(_115120), element(_115118, the_carrier(_115120)), element(_115116, the_carrier(_115120))], (4193 ^ _51060) ^ [_115428] : [relation(_115428), -(relation(relation_inverse(_115428)))], (4199 ^ _51060) ^ [_115503, _115505, _115507] : [relation_of2(_115503, _115507, _115505), -(element(relation_dom_as_subset(_115507, _115505, _115503), powerset(_115507)))], (4205 ^ _51060) ^ [] : [true___, -(true___)], (4211 ^ _51060) ^ [] : [true___, -(true___)], (4217 ^ _51060) ^ [] : [true___, -(true___)], (4223 ^ _51060) ^ [_115773, _115775] : [-(relation(relation_composition(_115775, _115773))), relation(_115775), relation(_115773)], (4233 ^ _51060) ^ [_115902, _115904, _115906] : [relation_of2(_115902, _115906, _115904), -(element(relation_rng_as_subset(_115906, _115904, _115902), powerset(_115904)))], (4239 ^ _51060) ^ [_115995, _115997] : [element(_115995, powerset(powerset(_115997))), -(element(union_of_subsets(_115997, _115995), powerset(_115997)))], (4245 ^ _51060) ^ [_116090] : [-(relation(identity_relation(_116090)))], (4247 ^ _51060) ^ [_116114, _116116] : [element(_116114, powerset(powerset(_116116))), -(element(meet_of_subsets(_116116, _116114), powerset(_116116)))], (4253 ^ _51060) ^ [_116209, _116211, _116213] : [-(element(subset_difference(_116213, _116211, _116209), powerset(_116213))), element(_116211, powerset(_116213)), element(_116209, powerset(_116213))], (4263 ^ _51060) ^ [_116362, _116364] : [relation(_116364), -(relation(relation_dom_restriction(_116364, _116362)))], (4269 ^ _51060) ^ [_116441, _116443] : [element(_116441, powerset(powerset(_116443))), -(element(complements_of_subsets(_116443, _116441), powerset(powerset(_116443))))], (4275 ^ _51060) ^ [_116540, _116542] : [relation(_116540), -(relation(relation_rng_restriction(_116542, _116540)))], (4281 ^ _51060) ^ [] : [true___, -(true___)], (4287 ^ _51060) ^ [_116678] : [meet_semilatt_str(_116678), -(one_sorted_str(_116678))], (4293 ^ _51060) ^ [] : [true___, -(true___)], (4299 ^ _51060) ^ [_116808] : [join_semilatt_str(_116808), -(one_sorted_str(_116808))], (4305 ^ _51060) ^ [_116879] : [latt_str(_116879), 4308 ^ _51060 : [(4309 ^ _51060) ^ [] : [-(meet_semilatt_str(_116879))], (4311 ^ _51060) ^ [] : [-(join_semilatt_str(_116879))]]], (4313 ^ _51060) ^ [] : [true___, -(true___)], (4319 ^ _51060) ^ [] : [true___, -(true___)], (4325 ^ _51060) ^ [_117092, _117094, _117096] : [relation_of2_as_subset(_117092, _117096, _117094), -(element(_117092, powerset(cartesian_product2(_117096, _117094))))], (4331 ^ _51060) ^ [_117183] : [meet_semilatt_str(_117183), 4334 ^ _51060 : [(4335 ^ _51060) ^ [] : [-(function(the_L_meet(_117183)))], (4337 ^ _51060) ^ [] : [-(quasi_total(the_L_meet(_117183), cartesian_product2(the_carrier(_117183), the_carrier(_117183)), the_carrier(_117183)))], (4339 ^ _51060) ^ [] : [-(relation_of2_as_subset(the_L_meet(_117183), cartesian_product2(the_carrier(_117183), the_carrier(_117183)), the_carrier(_117183)))]]], (4341 ^ _51060) ^ [] : [true___, -(true___)], (4347 ^ _51060) ^ [_117415] : [join_semilatt_str(_117415), 4350 ^ _51060 : [(4351 ^ _51060) ^ [] : [-(function(the_L_join(_117415)))], (4353 ^ _51060) ^ [] : [-(quasi_total(the_L_join(_117415), cartesian_product2(the_carrier(_117415), the_carrier(_117415)), the_carrier(_117415)))], (4355 ^ _51060) ^ [] : [-(relation_of2_as_subset(the_L_join(_117415), cartesian_product2(the_carrier(_117415), the_carrier(_117415)), the_carrier(_117415)))]]], (4358 ^ _51060) ^ [] : [-(meet_semilatt_str(4356 ^ []))], (4361 ^ _51060) ^ [] : [-(one_sorted_str(4359 ^ []))], (4364 ^ _51060) ^ [] : [-(join_semilatt_str(4362 ^ []))], (4367 ^ _51060) ^ [] : [-(latt_str(4365 ^ []))], (4370 ^ _51060) ^ [_117684, _117686] : [-(relation_of2(4368 ^ [_117684, _117686], _117686, _117684))], (4373 ^ _51060) ^ [_117717] : [-(element(4371 ^ [_117717], _117717))], (4376 ^ _51060) ^ [_117745, _117747] : [-(relation_of2_as_subset(4374 ^ [_117745, _117747], _117747, _117745))], (4378 ^ _51060) ^ [_117778, _117780] : [finite(_117778), -(finite(set_intersection2(_117780, _117778)))], (4384 ^ _51060) ^ [_117857, _117859] : [4391 ^ _51060 : [(4392 ^ _51060) ^ [] : [-(empty(relation_composition(_117857, _117859)))], (4394 ^ _51060) ^ [] : [-(relation(relation_composition(_117857, _117859)))]], empty(_117859), relation(_117857)], (4396 ^ _51060) ^ [_118016, _118018] : [finite(_118018), -(finite(set_intersection2(_118018, _118016)))], (4402 ^ _51060) ^ [_118095] : [empty(_118095), 4405 ^ _51060 : [(4406 ^ _51060) ^ [] : [-(empty(relation_inverse(_118095)))], (4408 ^ _51060) ^ [] : [-(relation(relation_inverse(_118095)))]]], (4410 ^ _51060) ^ [_118198, _118200] : [finite(_118200), -(finite(set_difference(_118200, _118198)))], (4416 ^ _51060) ^ [] : [-(empty(empty_set))], (4418 ^ _51060) ^ [] : [-(relation(empty_set))], (4420 ^ _51060) ^ [] : [-(relation_empty_yielding(empty_set))], (4422 ^ _51060) ^ [_118325, _118327] : [-(finite(relation_image(_118327, _118325))), relation(_118327), function(_118327), finite(_118325)], (4436 ^ _51060) ^ [_118504, _118506] : [4443 ^ _51060 : [(4444 ^ _51060) ^ [] : [-(relation(relation_dom_restriction(_118506, _118504)))], (4446 ^ _51060) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_118506, _118504)))]], relation(_118506), relation_empty_yielding(_118506)], (4448 ^ _51060) ^ [_118673] : [empty(singleton(_118673))], (4450 ^ _51060) ^ [_118695] : [-(finite(singleton(_118695)))], (4452 ^ _51060) ^ [_118731] : [empty(powerset(_118731))], (4454 ^ _51060) ^ [_118751] : [-(cup_closed(powerset(_118751)))], (4456 ^ _51060) ^ [_118770] : [-(diff_closed(powerset(_118770)))], (4458 ^ _51060) ^ [_118791] : [-(preboolean(powerset(_118791)))], (4460 ^ _51060) ^ [_118821, _118823] : [4475 ^ _51060 : [(4476 ^ _51060) ^ [] : [-(relation(relation_composition(_118823, _118821)))], (4478 ^ _51060) ^ [] : [-(function(relation_composition(_118823, _118821)))]], relation(_118823), function(_118823), relation(_118821), function(_118821)], (4480 ^ _51060) ^ [_119089] : [empty(succ(_119089))], (4482 ^ _51060) ^ [] : [-(epsilon_transitive(omega))], (4484 ^ _51060) ^ [] : [-(epsilon_connected(omega))], (4486 ^ _51060) ^ [] : [-(ordinal(omega))], (4488 ^ _51060) ^ [] : [empty(omega)], (4490 ^ _51060) ^ [_119194, _119196] : [-(relation(set_intersection2(_119196, _119194))), relation(_119196), relation(_119194)], (4500 ^ _51060) ^ [_119323] : [empty(the_carrier(_119323)), -(empty_carrier(_119323)), one_sorted_str(_119323)], (4510 ^ _51060) ^ [_119459] : [empty(powerset(_119459))], (4512 ^ _51060) ^ [] : [-(empty(empty_set))], (4514 ^ _51060) ^ [_119513, _119515] : [empty(ordered_pair(_119515, _119513))], (4516 ^ _51060) ^ [_119540] : [4523 ^ _51060 : [(4524 ^ _51060) ^ [] : [empty(succ(_119540))], (4526 ^ _51060) ^ [] : [-(epsilon_transitive(succ(_119540)))], (4528 ^ _51060) ^ [] : [-(epsilon_connected(succ(_119540)))], (4530 ^ _51060) ^ [] : [-(ordinal(succ(_119540)))], (4532 ^ _51060) ^ [] : [-(natural(succ(_119540)))]], ordinal(_119540), natural(_119540)], (4534 ^ _51060) ^ [_119777] : [-(relation(identity_relation(_119777)))], (4536 ^ _51060) ^ [_119798] : [-(function(identity_relation(_119798)))], (4538 ^ _51060) ^ [] : [-(relation(empty_set))], (4540 ^ _51060) ^ [] : [-(relation_empty_yielding(empty_set))], (4542 ^ _51060) ^ [] : [-(function(empty_set))], (4544 ^ _51060) ^ [] : [-(one_to_one(empty_set))], (4546 ^ _51060) ^ [] : [-(empty(empty_set))], (4548 ^ _51060) ^ [] : [-(epsilon_transitive(empty_set))], (4550 ^ _51060) ^ [] : [-(epsilon_connected(empty_set))], (4552 ^ _51060) ^ [] : [-(ordinal(empty_set))], (4554 ^ _51060) ^ [_119947, _119949] : [-(relation(set_union2(_119949, _119947))), relation(_119949), relation(_119947)], (4564 ^ _51060) ^ [_120085] : [empty(singleton(_120085))], (4566 ^ _51060) ^ [_120108, _120110] : [-(empty(_120110)), empty(set_union2(_120110, _120108))], (4572 ^ _51060) ^ [_120187] : [4583 ^ _51060 : [(4584 ^ _51060) ^ [] : [-(relation(relation_inverse(_120187)))], (4586 ^ _51060) ^ [] : [-(function(relation_inverse(_120187)))]], relation(_120187), function(_120187), one_to_one(_120187)], (4588 ^ _51060) ^ [_120386] : [ordinal(_120386), 4591 ^ _51060 : [(4592 ^ _51060) ^ [] : [empty(succ(_120386))], (4594 ^ _51060) ^ [] : [-(epsilon_transitive(succ(_120386)))], (4596 ^ _51060) ^ [] : [-(epsilon_connected(succ(_120386)))], (4598 ^ _51060) ^ [] : [-(ordinal(succ(_120386)))]]], (4600 ^ _51060) ^ [_120551, _120553] : [-(relation(set_difference(_120553, _120551))), relation(_120553), relation(_120551)], (4610 ^ _51060) ^ [_120692, _120694] : [empty(unordered_pair(_120694, _120692))], (4612 ^ _51060) ^ [_120718, _120720] : [-(empty(_120720)), empty(set_union2(_120718, _120720))], (4618 ^ _51060) ^ [_120797, _120799] : [4625 ^ _51060 : [(4626 ^ _51060) ^ [] : [-(relation(relation_dom_restriction(_120799, _120797)))], (4628 ^ _51060) ^ [] : [-(function(relation_dom_restriction(_120799, _120797)))]], relation(_120799), function(_120799)], (4630 ^ _51060) ^ [_120956] : [ordinal(_120956), 4633 ^ _51060 : [(4634 ^ _51060) ^ [] : [-(epsilon_transitive(union(_120956)))], (4636 ^ _51060) ^ [] : [-(epsilon_connected(union(_120956)))], (4638 ^ _51060) ^ [] : [-(ordinal(union(_120956)))]]], (4640 ^ _51060) ^ [] : [-(empty(empty_set))], (4642 ^ _51060) ^ [] : [-(relation(empty_set))], (4644 ^ _51060) ^ [_121117, _121119] : [empty(cartesian_product2(_121119, _121117)), -(empty(_121119)), -(empty(_121117))], (4654 ^ _51060) ^ [_121202, _121204] : [4661 ^ _51060 : [(4662 ^ _51060) ^ [] : [-(relation(relation_rng_restriction(_121204, _121202)))], (4664 ^ _51060) ^ [] : [-(function(relation_rng_restriction(_121204, _121202)))]], relation(_121202), function(_121202)], (4666 ^ _51060) ^ [_121361] : [empty(relation_dom(_121361)), -(empty(_121361)), relation(_121361)], (4676 ^ _51060) ^ [] : [-(empty(empty_set))], (4678 ^ _51060) ^ [] : [-(v1_membered(empty_set))], (4680 ^ _51060) ^ [] : [-(v2_membered(empty_set))], (4682 ^ _51060) ^ [] : [-(v3_membered(empty_set))], (4684 ^ _51060) ^ [] : [-(v4_membered(empty_set))], (4686 ^ _51060) ^ [] : [-(v5_membered(empty_set))], (4688 ^ _51060) ^ [_121581] : [empty(relation_rng(_121581)), -(empty(_121581)), relation(_121581)], (4698 ^ _51060) ^ [_121708] : [empty(_121708), 4701 ^ _51060 : [(4702 ^ _51060) ^ [] : [-(empty(relation_dom(_121708)))], (4704 ^ _51060) ^ [] : [-(relation(relation_dom(_121708)))]]], (4706 ^ _51060) ^ [_121811] : [empty(_121811), 4709 ^ _51060 : [(4710 ^ _51060) ^ [] : [-(empty(relation_rng(_121811)))], (4712 ^ _51060) ^ [] : [-(relation(relation_rng(_121811)))]]], (4714 ^ _51060) ^ [_121914, _121916] : [-(finite(set_union2(_121916, _121914))), finite(_121916), finite(_121914)], (4724 ^ _51060) ^ [_122043, _122045] : [4731 ^ _51060 : [(4732 ^ _51060) ^ [] : [-(empty(relation_composition(_122045, _122043)))], (4734 ^ _51060) ^ [] : [-(relation(relation_composition(_122045, _122043)))]], empty(_122045), relation(_122043)], (4736 ^ _51060) ^ [_122202, _122204] : [-(set_union2(_122204, _122204) = _122204)], (4738 ^ _51060) ^ [_122230, _122232] : [-(set_intersection2(_122232, _122232) = _122232)], (4740 ^ _51060) ^ [_122258, _122260] : [element(_122258, powerset(_122260)), -(subset_complement(_122260, subset_complement(_122260, _122258)) = _122258)], (4746 ^ _51060) ^ [_122351] : [relation(_122351), -(relation_inverse(relation_inverse(_122351)) = _122351)], (4752 ^ _51060) ^ [_122432, _122434] : [element(_122432, powerset(powerset(_122434))), -(complements_of_subsets(_122434, complements_of_subsets(_122434, _122432)) = _122432)], (4758 ^ _51060) ^ [_122541, _122543] : [proper_subset(_122543, _122543)], (4760 ^ _51060) ^ [_122566] : [relation(_122566), 4763 ^ _51060 : [(4774 ^ _51060) ^ [] : [4776 ^ _51060 : [(4777 ^ _51060) ^ [] : [-(in(4775 ^ [_122566], relation_field(_122566)))], (4779 ^ _51060) ^ [] : [in(ordered_pair(4775 ^ [_122566], 4775 ^ [_122566]), _122566)]], -(reflexive(_122566))], (4764 ^ _51060) ^ [] : [reflexive(_122566), 4767 ^ _51060 : [(4768 ^ _51060) ^ [_122685] : [in(_122685, relation_field(_122566)), -(in(ordered_pair(_122685, _122685), _122566))]]]]], (4783 ^ _51060) ^ [_122913] : [singleton(_122913) = empty_set], (4785 ^ _51060) ^ [_122938, _122940] : [in(_122940, _122938), -(set_union2(singleton(_122940), _122938) = _122938)], (4791 ^ _51060) ^ [_123025, _123027] : [disjoint(singleton(_123027), _123025), in(_123027, _123025)], (4797 ^ _51060) ^ [_123101, _123103] : [-(in(_123103, _123101)), -(disjoint(singleton(_123103), _123101))], (4803 ^ _51060) ^ [_123139, _123141] : [relation(_123139), -(subset(relation_dom(relation_rng_restriction(_123141, _123139)), relation_dom(_123139)))], (4809 ^ _51060) ^ [_123228] : [relation(_123228), 4812 ^ _51060 : [(4827 ^ _51060) ^ [] : [4831 ^ _51060 : [(4832 ^ _51060) ^ [] : [-(in(ordered_pair(4828 ^ [_123228], 4829 ^ [_123228]), _123228))], (4834 ^ _51060) ^ [] : [-(in(ordered_pair(4829 ^ [_123228], 4830 ^ [_123228]), _123228))], (4836 ^ _51060) ^ [] : [in(ordered_pair(4828 ^ [_123228], 4830 ^ [_123228]), _123228)]], -(transitive(_123228))], (4813 ^ _51060) ^ [] : [transitive(_123228), 4816 ^ _51060 : [(4817 ^ _51060) ^ [_123367, _123369, _123371] : [-(in(ordered_pair(_123371, _123367), _123228)), in(ordered_pair(_123371, _123369), _123228), in(ordered_pair(_123369, _123367), _123228)]]]]], (4840 ^ _51060) ^ [_123713, _123715] : [subset(singleton(_123715), _123713), -(in(_123715, _123713))], (4846 ^ _51060) ^ [_123790, _123792] : [in(_123792, _123790), -(subset(singleton(_123792), _123790))], (4852 ^ _51060) ^ [_123873, _123875] : [relation(_123873), well_ordering(_123873), equipotent(_123875, relation_field(_123873)), 4864 ^ _51060 : [(4865 ^ _51060) ^ [] : [-(relation(4863 ^ [_123873, _123875]))], (4867 ^ _51060) ^ [] : [-(well_orders(4863 ^ [_123873, _123875], _123875))]]], (4869 ^ _51060) ^ [_124116, _124118] : [set_difference(_124118, _124116) = empty_set, -(subset(_124118, _124116))], (4875 ^ _51060) ^ [_124195, _124197] : [subset(_124197, _124195), -(set_difference(_124197, _124195) = empty_set)], (4881 ^ _51060) ^ [_124280, _124282] : [element(_124280, powerset(_124282)), 4884 ^ _51060 : [(4885 ^ _51060) ^ [_124347] : [in(_124347, _124280), -(in(_124347, _124282))]]], (4891 ^ _51060) ^ [_124430] : [relation(_124430), 4894 ^ _51060 : [(4909 ^ _51060) ^ [] : [4912 ^ _51060 : [(4913 ^ _51060) ^ [] : [-(in(ordered_pair(4910 ^ [_124430], 4911 ^ [_124430]), _124430))], (4915 ^ _51060) ^ [] : [-(in(ordered_pair(4911 ^ [_124430], 4910 ^ [_124430]), _124430))], (4917 ^ _51060) ^ [] : [4910 ^ [_124430] = 4911 ^ [_124430]]], -(antisymmetric(_124430))], (4895 ^ _51060) ^ [] : [antisymmetric(_124430), 4898 ^ _51060 : [(4899 ^ _51060) ^ [_124561, _124563] : [-(_124563 = _124561), in(ordered_pair(_124563, _124561), _124430), in(ordered_pair(_124561, _124563), _124430)]]]]], (4921 ^ _51060) ^ [_124876, _124878, _124880] : [subset(_124880, _124878), -(in(_124876, _124880)), -(subset(_124880, set_difference(_124878, singleton(_124876))))], (4931 ^ _51060) ^ [_124978] : [relation(_124978), 4934 ^ _51060 : [(4957 ^ _51060) ^ [] : [4960 ^ _51060 : [(4961 ^ _51060) ^ [] : [-(in(4958 ^ [_124978], relation_field(_124978)))], (4963 ^ _51060) ^ [] : [-(in(4959 ^ [_124978], relation_field(_124978)))], (4965 ^ _51060) ^ [] : [4958 ^ [_124978] = 4959 ^ [_124978]], (4967 ^ _51060) ^ [] : [in(ordered_pair(4958 ^ [_124978], 4959 ^ [_124978]), _124978)], (4969 ^ _51060) ^ [] : [in(ordered_pair(4959 ^ [_124978], 4958 ^ [_124978]), _124978)]], -(connected(_124978))], (4935 ^ _51060) ^ [] : [connected(_124978), 4938 ^ _51060 : [(4939 ^ _51060) ^ [_125133, _125135] : [in(_125135, relation_field(_124978)), in(_125133, relation_field(_124978)), -(_125135 = _125133), -(in(ordered_pair(_125135, _125133), _124978)), -(in(ordered_pair(_125133, _125135), _124978))]]]]], (4983 ^ _51060) ^ [_125714, _125716] : [4984 ^ _51060 : [(4985 ^ _51060) ^ [] : [_125716 = empty_set], (4987 ^ _51060) ^ [] : [_125716 = singleton(_125714)]], -(subset(_125716, singleton(_125714)))], (4973 ^ _51060) ^ [_125620, _125622] : [subset(_125622, singleton(_125620)), -(_125622 = empty_set), -(_125622 = singleton(_125620))], (4991 ^ _51060) ^ [_125839, _125841] : [in(_125841, _125839), -(subset(_125841, union(_125839)))], (4997 ^ _51060) ^ [_125941, _125943, _125945, _125947] : [in(ordered_pair(_125947, _125945), cartesian_product2(_125943, _125941)), 5000 ^ _51060 : [(5001 ^ _51060) ^ [] : [-(in(_125947, _125943))], (5003 ^ _51060) ^ [] : [-(in(_125945, _125941))]]], (5005 ^ _51060) ^ [_126056, _126058, _126060, _126062] : [-(in(ordered_pair(_126062, _126060), cartesian_product2(_126058, _126056))), in(_126062, _126058), in(_126060, _126056)], (5015 ^ _51060) ^ [_126207, _126209] : [5017 ^ _51060 : [(5018 ^ _51060) ^ [] : [-(in(5016 ^ [_126207, _126209], _126209))], (5020 ^ _51060) ^ [] : [in(5016 ^ [_126207, _126209], _126207)]], -(element(_126209, powerset(_126207)))], (5024 ^ _51060) ^ [_126351, _126353, _126355] : [relation(_126351), function(_126351), 5031 ^ _51060 : [(5032 ^ _51060) ^ [] : [in(_126353, relation_dom(relation_dom_restriction(_126351, _126355))), 5035 ^ _51060 : [(5036 ^ _51060) ^ [] : [-(in(_126353, relation_dom(_126351)))], (5038 ^ _51060) ^ [] : [-(in(_126353, _126355))]]], (5040 ^ _51060) ^ [] : [-(in(_126353, relation_dom(relation_dom_restriction(_126351, _126355)))), in(_126353, relation_dom(_126351)), in(_126353, _126355)]]], (5051 ^ _51060) ^ [] : [empty(5049 ^ [])], (5053 ^ _51060) ^ [] : [-(epsilon_transitive(5049 ^ []))], (5055 ^ _51060) ^ [] : [-(epsilon_connected(5049 ^ []))], (5057 ^ _51060) ^ [] : [-(ordinal(5049 ^ []))], (5059 ^ _51060) ^ [] : [-(natural(5049 ^ []))], (5062 ^ _51060) ^ [] : [empty(5060 ^ [])], (5064 ^ _51060) ^ [] : [-(finite(5060 ^ []))], (5067 ^ _51060) ^ [] : [-(relation(5065 ^ []))], (5069 ^ _51060) ^ [] : [-(function(5065 ^ []))], (5072 ^ _51060) ^ [_126916, _126918] : [-(relation_of2(5070 ^ [_126916, _126918], _126918, _126916))], (5074 ^ _51060) ^ [_126944, _126946] : [-(relation(5070 ^ [_126944, _126946]))], (5076 ^ _51060) ^ [_126970, _126972] : [-(function(5070 ^ [_126970, _126972]))], (5078 ^ _51060) ^ [_126998, _127000] : [-(quasi_total(5070 ^ [_126998, _127000], _127000, _126998))], (5081 ^ _51060) ^ [] : [empty(5079 ^ [])], (5083 ^ _51060) ^ [] : [-(v1_membered(5079 ^ []))], (5085 ^ _51060) ^ [] : [-(v2_membered(5079 ^ []))], (5087 ^ _51060) ^ [] : [-(v3_membered(5079 ^ []))], (5089 ^ _51060) ^ [] : [-(v4_membered(5079 ^ []))], (5091 ^ _51060) ^ [] : [-(v5_membered(5079 ^ []))], (5094 ^ _51060) ^ [] : [-(epsilon_transitive(5092 ^ []))], (5096 ^ _51060) ^ [] : [-(epsilon_connected(5092 ^ []))], (5098 ^ _51060) ^ [] : [-(ordinal(5092 ^ []))], (5101 ^ _51060) ^ [] : [-(epsilon_transitive(5099 ^ []))], (5103 ^ _51060) ^ [] : [-(epsilon_connected(5099 ^ []))], (5105 ^ _51060) ^ [] : [-(ordinal(5099 ^ []))], (5107 ^ _51060) ^ [] : [-(being_limit_ordinal(5099 ^ []))], (5110 ^ _51060) ^ [] : [-(relation(5108 ^ []))], (5112 ^ _51060) ^ [] : [-(function(5108 ^ []))], (5114 ^ _51060) ^ [] : [-(one_to_one(5108 ^ []))], (5116 ^ _51060) ^ [] : [-(empty(5108 ^ []))], (5119 ^ _51060) ^ [] : [-(empty(5117 ^ []))], (5121 ^ _51060) ^ [] : [-(relation(5117 ^ []))], (5123 ^ _51060) ^ [_127418] : [-(empty(_127418)), 5127 ^ _51060 : [(5128 ^ _51060) ^ [] : [-(element(5126 ^ [_127418], powerset(_127418)))], (5130 ^ _51060) ^ [] : [empty(5126 ^ [_127418])]]], (5133 ^ _51060) ^ [] : [-(empty(5131 ^ []))], (5136 ^ _51060) ^ [_127573] : [-(element(5134 ^ [_127573], powerset(_127573)))], (5138 ^ _51060) ^ [_127598] : [-(empty(5134 ^ [_127598]))], (5140 ^ _51060) ^ [_127620] : [-(relation(5134 ^ [_127620]))], (5142 ^ _51060) ^ [_127642] : [-(function(5134 ^ [_127642]))], (5144 ^ _51060) ^ [_127664] : [-(one_to_one(5134 ^ [_127664]))], (5146 ^ _51060) ^ [_127686] : [-(epsilon_transitive(5134 ^ [_127686]))], (5148 ^ _51060) ^ [_127708] : [-(epsilon_connected(5134 ^ [_127708]))], (5150 ^ _51060) ^ [_127730] : [-(ordinal(5134 ^ [_127730]))], (5152 ^ _51060) ^ [_127752] : [-(natural(5134 ^ [_127752]))], (5154 ^ _51060) ^ [_127776] : [-(finite(5134 ^ [_127776]))], (5157 ^ _51060) ^ [] : [-(relation(5155 ^ []))], (5159 ^ _51060) ^ [] : [-(empty(5155 ^ []))], (5161 ^ _51060) ^ [] : [-(function(5155 ^ []))], (5164 ^ _51060) ^ [] : [-(relation(5162 ^ []))], (5166 ^ _51060) ^ [] : [-(function(5162 ^ []))], (5168 ^ _51060) ^ [] : [-(one_to_one(5162 ^ []))], (5170 ^ _51060) ^ [] : [-(empty(5162 ^ []))], (5172 ^ _51060) ^ [] : [-(epsilon_transitive(5162 ^ []))], (5174 ^ _51060) ^ [] : [-(epsilon_connected(5162 ^ []))], (5176 ^ _51060) ^ [] : [-(ordinal(5162 ^ []))], (5179 ^ _51060) ^ [_128003, _128005] : [-(relation_of2(5177 ^ [_128003, _128005], _128005, _128003))], (5181 ^ _51060) ^ [_128031, _128033] : [-(relation(5177 ^ [_128031, _128033]))], (5183 ^ _51060) ^ [_128059, _128061] : [-(function(5177 ^ [_128059, _128061]))], (5186 ^ _51060) ^ [] : [empty(5184 ^ [])], (5188 ^ _51060) ^ [] : [-(relation(5184 ^ []))], (5191 ^ _51060) ^ [_128145] : [-(element(5189 ^ [_128145], powerset(_128145)))], (5193 ^ _51060) ^ [_128172] : [-(empty(5189 ^ [_128172]))], (5196 ^ _51060) ^ [] : [empty(5194 ^ [])], (5198 ^ _51060) ^ [_128230] : [-(empty(_128230)), 5202 ^ _51060 : [(5203 ^ _51060) ^ [] : [-(element(5201 ^ [_128230], powerset(_128230)))], (5205 ^ _51060) ^ [] : [empty(5201 ^ [_128230])], (5207 ^ _51060) ^ [] : [-(finite(5201 ^ [_128230]))]]], (5210 ^ _51060) ^ [] : [-(relation(5208 ^ []))], (5212 ^ _51060) ^ [] : [-(function(5208 ^ []))], (5214 ^ _51060) ^ [] : [-(one_to_one(5208 ^ []))], (5217 ^ _51060) ^ [] : [empty(5215 ^ [])], (5219 ^ _51060) ^ [] : [-(epsilon_transitive(5215 ^ []))], (5221 ^ _51060) ^ [] : [-(epsilon_connected(5215 ^ []))], (5223 ^ _51060) ^ [] : [-(ordinal(5215 ^ []))], (5226 ^ _51060) ^ [] : [-(relation(5224 ^ []))], (5228 ^ _51060) ^ [] : [-(relation_empty_yielding(5224 ^ []))], (5231 ^ _51060) ^ [] : [-(one_sorted_str(5229 ^ []))], (5233 ^ _51060) ^ [] : [empty_carrier(5229 ^ [])], (5236 ^ _51060) ^ [] : [-(relation(5234 ^ []))], (5238 ^ _51060) ^ [] : [-(relation_empty_yielding(5234 ^ []))], (5240 ^ _51060) ^ [] : [-(function(5234 ^ []))], (5242 ^ _51060) ^ [_128704] : [5250 ^ _51060 : [(5251 ^ _51060) ^ [] : [-(element(5249 ^ [_128704], powerset(the_carrier(_128704))))], (5253 ^ _51060) ^ [] : [empty(5249 ^ [_128704])]], -(empty_carrier(_128704)), one_sorted_str(_128704)], (5255 ^ _51060) ^ [_128893, _128895, _128897, _128899, _128901, _128903] : [-(apply_binary_as_element(_128903, _128901, _128899, _128897, _128895, _128893) = apply_binary(_128897, _128895, _128893)), -(empty(_128903)), -(empty(_128901)), function(_128897), quasi_total(_128897, cartesian_product2(_128903, _128901), _128899), relation_of2(_128897, cartesian_product2(_128903, _128901), _128899), element(_128895, _128903), element(_128893, _128901)], (5285 ^ _51060) ^ [_129376, _129378, _129380] : [-(join_commut(_129380, _129378, _129376) = join(_129380, _129378, _129376)), -(empty_carrier(_129380)), join_commutative(_129380), join_semilatt_str(_129380), element(_129378, the_carrier(_129380)), element(_129376, the_carrier(_129380))], (5307 ^ _51060) ^ [_129692, _129694, _129696] : [-(meet_commut(_129696, _129694, _129692) = meet(_129696, _129694, _129692)), -(empty_carrier(_129696)), meet_commutative(_129696), meet_semilatt_str(_129696), element(_129694, the_carrier(_129696)), element(_129692, the_carrier(_129696))], (5329 ^ _51060) ^ [_130008, _130010, _130012] : [relation_of2(_130008, _130012, _130010), -(relation_dom_as_subset(_130012, _130010, _130008) = relation_dom(_130008))], (5335 ^ _51060) ^ [_130101, _130103, _130105] : [relation_of2(_130101, _130105, _130103), -(relation_rng_as_subset(_130105, _130103, _130101) = relation_rng(_130101))], (5341 ^ _51060) ^ [_130194, _130196] : [element(_130194, powerset(powerset(_130196))), -(union_of_subsets(_130196, _130194) = union(_130194))], (5347 ^ _51060) ^ [_130289, _130291] : [element(_130289, powerset(powerset(_130291))), -(meet_of_subsets(_130291, _130289) = set_meet(_130289))], (5353 ^ _51060) ^ [_130384, _130386, _130388] : [-(subset_difference(_130388, _130386, _130384) = set_difference(_130386, _130384)), element(_130386, powerset(_130388)), element(_130384, powerset(_130388))], (5363 ^ _51060) ^ [_130557, _130559, _130561] : [relation_of2_as_subset(_130557, _130561, _130559), -(relation_of2(_130557, _130561, _130559))], (5369 ^ _51060) ^ [_130636, _130638, _130640] : [relation_of2(_130636, _130640, _130638), -(relation_of2_as_subset(_130636, _130640, _130638))], (5375 ^ _51060) ^ [_130721, _130723] : [ordinal(_130723), ordinal(_130721), 5382 ^ _51060 : [(5383 ^ _51060) ^ [] : [ordinal_subset(_130723, _130721), -(subset(_130723, _130721))], (5389 ^ _51060) ^ [] : [subset(_130723, _130721), -(ordinal_subset(_130723, _130721))]]], (5395 ^ _51060) ^ [_130993, _130995] : [equipotent(_130995, _130993), -(are_equipotent(_130995, _130993))], (5401 ^ _51060) ^ [_131066, _131068] : [are_equipotent(_131068, _131066), -(equipotent(_131068, _131066))], (5407 ^ _51060) ^ [_131145, _131147] : [-(ordinal_subset(_131147, _131147)), ordinal(_131147), ordinal(_131145)], (5417 ^ _51060) ^ [_131270, _131272] : [-(subset(_131272, _131272))], (5419 ^ _51060) ^ [_131295, _131297] : [-(equipotent(_131297, _131297))], (5421 ^ _51060) ^ [_131320, _131322] : [-(empty(_131322)), relation(_131320), 5433 ^ _51060 : [(5460 ^ _51060) ^ [] : [5431 ^ [_131320, _131322] = 5432 ^ [_131320, _131322]], (5434 ^ _51060) ^ [] : [-(in(5430 ^ [_131320, _131322], _131322))], (5437 ^ _51060) ^ [] : [-(5430 ^ [_131320, _131322] = 5435 ^ [_131320, _131322])], (5439 ^ _51060) ^ [] : [-(in(5431 ^ [_131320, _131322], 5435 ^ [_131320, _131322]))], (5441 ^ _51060) ^ [_131923] : [in(_131923, 5435 ^ [_131320, _131322]), -(in(ordered_pair(5431 ^ [_131320, _131322], _131923), _131320))], (5447 ^ _51060) ^ [] : [-(in(5430 ^ [_131320, _131322], _131322))], (5450 ^ _51060) ^ [] : [-(5430 ^ [_131320, _131322] = 5448 ^ [_131320, _131322])], (5452 ^ _51060) ^ [] : [-(in(5432 ^ [_131320, _131322], 5448 ^ [_131320, _131322]))], (5454 ^ _51060) ^ [_132181] : [in(_132181, 5448 ^ [_131320, _131322]), -(in(ordered_pair(5432 ^ [_131320, _131322], _132181), _131320))]], 5462 ^ _51060 : [(5463 ^ _51060) ^ [] : [-(relation(5461 ^ [_131320, _131322]))], (5465 ^ _51060) ^ [] : [-(function(5461 ^ [_131320, _131322]))], (5467 ^ _51060) ^ [_132491, _132493] : [in(ordered_pair(_132493, _132491), 5461 ^ [_131320, _131322]), 5470 ^ _51060 : [(5471 ^ _51060) ^ [] : [-(in(_132493, _131322))], (5473 ^ _51060) ^ [] : [-(in(_132493, _131322))], (5476 ^ _51060) ^ [] : [-(_132493 = 5474 ^ [_131320, _131322, _132491, _132493])], (5478 ^ _51060) ^ [] : [-(in(_132491, 5474 ^ [_131320, _131322, _132491, _132493]))], (5480 ^ _51060) ^ [_132751] : [in(_132751, 5474 ^ [_131320, _131322, _132491, _132493]), -(in(ordered_pair(_132491, _132751), _131320))]]], (5486 ^ _51060) ^ [_132870, _132872] : [-(in(ordered_pair(_132872, _132870), 5461 ^ [_131320, _131322])), in(_132872, _131322), in(_132872, _131322), 5495 ^ _51060 : [(5496 ^ _51060) ^ [_133052] : [_132872 = _133052, in(_132870, _133052), 5504 ^ _51060 : [(5505 ^ _51060) ^ [] : [-(in(5503 ^ [_131320, _131322, _132870, _132872, _133052], _133052))], (5507 ^ _51060) ^ [] : [in(ordered_pair(_132870, 5503 ^ [_131320, _131322, _132870, _132872, _133052]), _131320)]]]]]]], (5511 ^ _51060) ^ [_133340] : [5515 ^ _51060 : [(5516 ^ _51060) ^ [] : [-(in(5512 ^ [_133340], _133340))], (5518 ^ _51060) ^ [] : [-(5513 ^ [_133340] = singleton(5512 ^ [_133340]))], (5520 ^ _51060) ^ [] : [-(in(5512 ^ [_133340], _133340))], (5522 ^ _51060) ^ [] : [-(5514 ^ [_133340] = singleton(5512 ^ [_133340]))], (5524 ^ _51060) ^ [] : [5513 ^ [_133340] = 5514 ^ [_133340]]], 5526 ^ _51060 : [(5527 ^ _51060) ^ [] : [-(relation(5525 ^ [_133340]))], (5529 ^ _51060) ^ [] : [-(function(5525 ^ [_133340]))], (5531 ^ _51060) ^ [_133738, _133740] : [in(ordered_pair(_133740, _133738), 5525 ^ [_133340]), 5534 ^ _51060 : [(5535 ^ _51060) ^ [] : [-(in(_133740, _133340))], (5537 ^ _51060) ^ [] : [-(in(_133740, _133340))], (5539 ^ _51060) ^ [] : [-(_133738 = singleton(_133740))]]], (5541 ^ _51060) ^ [_133883, _133885] : [-(in(ordered_pair(_133885, _133883), 5525 ^ [_133340])), in(_133885, _133340), in(_133885, _133340), _133883 = singleton(_133885)]]], (5555 ^ _51060) ^ [_134102] : [5556 ^ _51060 : [(5557 ^ _51060) ^ [_134171] : [ordinal(_134171), in(_134171, _134102)]], 5563 ^ _51060 : [(5564 ^ _51060) ^ [] : [-(ordinal(5562 ^ [_134102]))], (5566 ^ _51060) ^ [] : [-(in(5562 ^ [_134102], _134102))], (5568 ^ _51060) ^ [_134328] : [ordinal(_134328), in(_134328, _134102), -(ordinal_subset(5562 ^ [_134102], _134328))]]], (5578 ^ _51060) ^ [] : [5705 ^ _51060 : [(5706 ^ _51060) ^ [_136733] : [ordinal(_136733), in(_136733, omega), 5713 ^ _51060 : [(5714 ^ _51060) ^ [_136884] : [element(_136884, powerset(powerset(_136733))), -(_136884 = empty_set), 5722 ^ _51060 : [(5723 ^ _51060) ^ [] : [-(in(5721 ^ [_136733, _136884], _136884))], (5725 ^ _51060) ^ [_137086] : [-(_137086 = 5721 ^ [_136733, _136884]), in(_137086, _136884), subset(5721 ^ [_136733, _136884], _137086)]]]]]], 5581 ^ _51060 : [(5582 ^ _51060) ^ [] : [-(in(empty_set, omega))], (5585 ^ _51060) ^ [] : [-(element(5583 ^ [], powerset(powerset(empty_set))))], (5587 ^ _51060) ^ [] : [5583 ^ [] = empty_set], (5589 ^ _51060) ^ [_134619] : [in(_134619, 5583 ^ []), 5593 ^ _51060 : [(5594 ^ _51060) ^ [] : [-(in(5592 ^ [_134619], 5583 ^ []))], (5596 ^ _51060) ^ [] : [-(subset(_134619, 5592 ^ [_134619]))], (5598 ^ _51060) ^ [] : [5592 ^ [_134619] = _134619]]]], 5602 ^ _51060 : [(5603 ^ _51060) ^ [] : [-(ordinal(5601 ^ []))], (5630 ^ _51060) ^ [] : [-(in(succ(5601 ^ []), omega))], (5633 ^ _51060) ^ [] : [-(element(5631 ^ [], powerset(powerset(succ(5601 ^ [])))))], (5635 ^ _51060) ^ [] : [5631 ^ [] = empty_set], (5637 ^ _51060) ^ [_135459] : [in(_135459, 5631 ^ []), 5641 ^ _51060 : [(5642 ^ _51060) ^ [] : [-(in(5640 ^ [_135459], 5631 ^ []))], (5644 ^ _51060) ^ [] : [-(subset(_135459, 5640 ^ [_135459]))], (5646 ^ _51060) ^ [] : [5640 ^ [_135459] = _135459]]], (5605 ^ _51060) ^ [] : [in(5601 ^ [], omega), 5608 ^ _51060 : [(5609 ^ _51060) ^ [_135006] : [element(_135006, powerset(powerset(5601 ^ []))), -(_135006 = empty_set), 5617 ^ _51060 : [(5618 ^ _51060) ^ [] : [-(in(5616 ^ [_135006], _135006))], (5620 ^ _51060) ^ [_135192] : [-(_135192 = 5616 ^ [_135006]), in(_135192, _135006), subset(5616 ^ [_135006], _135192)]]]]]], 5648 ^ _51060 : [(5649 ^ _51060) ^ [] : [-(ordinal(5647 ^ []))], (5686 ^ _51060) ^ [] : [5647 ^ [] = empty_set], (5688 ^ _51060) ^ [] : [-(in(5647 ^ [], omega))], (5691 ^ _51060) ^ [] : [-(element(5689 ^ [], powerset(powerset(5647 ^ []))))], (5693 ^ _51060) ^ [] : [5689 ^ [] = empty_set], (5695 ^ _51060) ^ [_136547] : [in(_136547, 5689 ^ []), 5699 ^ _51060 : [(5700 ^ _51060) ^ [] : [-(in(5698 ^ [_136547], 5689 ^ []))], (5702 ^ _51060) ^ [] : [-(subset(_136547, 5698 ^ [_136547]))], (5704 ^ _51060) ^ [] : [5698 ^ [_136547] = _136547]]], (5651 ^ _51060) ^ [] : [-(being_limit_ordinal(5647 ^ []))], (5653 ^ _51060) ^ [_135837] : [ordinal(_135837), in(_135837, 5647 ^ []), in(_135837, omega), 5664 ^ _51060 : [(5665 ^ _51060) ^ [_136036] : [element(_136036, powerset(powerset(_135837))), -(_136036 = empty_set), 5673 ^ _51060 : [(5674 ^ _51060) ^ [] : [-(in(5672 ^ [_135837, _136036], _136036))], (5676 ^ _51060) ^ [_136238] : [-(_136238 = 5672 ^ [_135837, _136036]), in(_136238, _136036), subset(5672 ^ [_135837, _136036], _136238)]]]]]]], (5735 ^ _51060) ^ [_137265, _137267, _137269] : [relation(_137267), relation(_137265), function(_137265), 5747 ^ _51060 : [(5748 ^ _51060) ^ [] : [-(relation(5746 ^ [_137265, _137267, _137269]))], (5750 ^ _51060) ^ [_137569, _137571] : [in(ordered_pair(_137571, _137569), 5746 ^ [_137265, _137267, _137269]), 5753 ^ _51060 : [(5754 ^ _51060) ^ [] : [-(in(_137571, _137269))], (5756 ^ _51060) ^ [] : [-(in(_137569, _137269))], (5758 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_137265, _137571), apply(_137265, _137569)), _137267))]]], (5760 ^ _51060) ^ [_137740, _137742] : [-(in(ordered_pair(_137742, _137740), 5746 ^ [_137265, _137267, _137269])), in(_137742, _137269), in(_137740, _137269), in(ordered_pair(apply(_137265, _137742), apply(_137265, _137740)), _137267)]]], (5774 ^ _51060) ^ [_137993, _137995] : [-(empty(_137995)), relation(_137993), 5786 ^ _51060 : [(5813 ^ _51060) ^ [] : [5784 ^ [_137993, _137995] = 5785 ^ [_137993, _137995]], (5787 ^ _51060) ^ [] : [-(in(5783 ^ [_137993, _137995], _137995))], (5790 ^ _51060) ^ [] : [-(5783 ^ [_137993, _137995] = 5788 ^ [_137993, _137995])], (5792 ^ _51060) ^ [] : [-(in(5784 ^ [_137993, _137995], 5788 ^ [_137993, _137995]))], (5794 ^ _51060) ^ [_138583] : [in(_138583, 5788 ^ [_137993, _137995]), -(in(ordered_pair(5784 ^ [_137993, _137995], _138583), _137993))], (5800 ^ _51060) ^ [] : [-(in(5783 ^ [_137993, _137995], _137995))], (5803 ^ _51060) ^ [] : [-(5783 ^ [_137993, _137995] = 5801 ^ [_137993, _137995])], (5805 ^ _51060) ^ [] : [-(in(5785 ^ [_137993, _137995], 5801 ^ [_137993, _137995]))], (5807 ^ _51060) ^ [_138841] : [in(_138841, 5801 ^ [_137993, _137995]), -(in(ordered_pair(5785 ^ [_137993, _137995], _138841), _137993))]], 5815 ^ _51060 : [(5816 ^ _51060) ^ [_139078] : [in(_139078, 5814 ^ [_137993, _137995]), 5820 ^ _51060 : [(5821 ^ _51060) ^ [] : [-(in(5819 ^ [_137993, _137995, _139078], _137995))], (5823 ^ _51060) ^ [] : [-(in(5819 ^ [_137993, _137995, _139078], _137995))], (5826 ^ _51060) ^ [] : [-(5819 ^ [_137993, _137995, _139078] = 5824 ^ [_137993, _137995, _139078])], (5828 ^ _51060) ^ [] : [-(in(_139078, 5824 ^ [_137993, _137995, _139078]))], (5830 ^ _51060) ^ [_139409] : [in(_139409, 5824 ^ [_137993, _137995, _139078]), -(in(ordered_pair(_139078, _139409), _137993))]]], (5836 ^ _51060) ^ [_139522] : [-(in(_139522, 5814 ^ [_137993, _137995])), 5837 ^ _51060 : [(5838 ^ _51060) ^ [_139608] : [in(_139608, _137995), in(_139608, _137995), 5845 ^ _51060 : [(5846 ^ _51060) ^ [_139749] : [_139608 = _139749, in(_139522, _139749), 5854 ^ _51060 : [(5855 ^ _51060) ^ [] : [-(in(5853 ^ [_137993, _137995, _139522, _139608, _139749], _139749))], (5857 ^ _51060) ^ [] : [in(ordered_pair(_139522, 5853 ^ [_137993, _137995, _139522, _139608, _139749]), _137993)]]]]]]]]], (5861 ^ _51060) ^ [_140032, _140034] : [-(empty(_140034)), relation(_140032), 5868 ^ _51060 : [(5869 ^ _51060) ^ [_140389] : [5873 ^ _51060 : [(5912 ^ _51060) ^ [] : [5871 ^ [_140032, _140034, _140389] = 5872 ^ [_140032, _140034, _140389]], (5874 ^ _51060) ^ [] : [-(5870 ^ [_140032, _140034, _140389] = 5871 ^ [_140032, _140034, _140389])], (5878 ^ _51060) ^ [] : [-(ordered_pair(5875 ^ [_140032, _140034, _140389], 5876 ^ [_140032, _140034, _140389]) = 5871 ^ [_140032, _140034, _140389])], (5880 ^ _51060) ^ [] : [-(in(5875 ^ [_140032, _140034, _140389], _140034))], (5883 ^ _51060) ^ [] : [-(5875 ^ [_140032, _140034, _140389] = 5881 ^ [_140032, _140034, _140389])], (5885 ^ _51060) ^ [] : [-(in(5876 ^ [_140032, _140034, _140389], 5881 ^ [_140032, _140034, _140389]))], (5887 ^ _51060) ^ [_141184] : [in(_141184, 5881 ^ [_140032, _140034, _140389]), -(in(ordered_pair(5876 ^ [_140032, _140034, _140389], _141184), _140032))], (5893 ^ _51060) ^ [] : [-(5870 ^ [_140032, _140034, _140389] = 5872 ^ [_140032, _140034, _140389])], (5897 ^ _51060) ^ [] : [-(ordered_pair(5894 ^ [_140032, _140034, _140389], 5895 ^ [_140032, _140034, _140389]) = 5872 ^ [_140032, _140034, _140389])], (5899 ^ _51060) ^ [] : [-(in(5894 ^ [_140032, _140034, _140389], _140034))], (5902 ^ _51060) ^ [] : [-(5894 ^ [_140032, _140034, _140389] = 5900 ^ [_140032, _140034, _140389])], (5904 ^ _51060) ^ [] : [-(in(5895 ^ [_140032, _140034, _140389], 5900 ^ [_140032, _140034, _140389]))], (5906 ^ _51060) ^ [_141634] : [in(_141634, 5900 ^ [_140032, _140034, _140389]), -(in(ordered_pair(5895 ^ [_140032, _140034, _140389], _141634), _140032))]], 5914 ^ _51060 : [(5915 ^ _51060) ^ [_141923] : [in(_141923, 5913 ^ [_140032, _140034, _140389]), 5919 ^ _51060 : [(5920 ^ _51060) ^ [] : [-(in(5918 ^ [_140032, _140034, _140389, _141923], cartesian_product2(_140034, _140389)))], (5922 ^ _51060) ^ [] : [-(5918 ^ [_140032, _140034, _140389, _141923] = _141923)], (5926 ^ _51060) ^ [] : [-(ordered_pair(5923 ^ [_140032, _140034, _140389, _141923], 5924 ^ [_140032, _140034, _140389, _141923]) = _141923)], (5928 ^ _51060) ^ [] : [-(in(5923 ^ [_140032, _140034, _140389, _141923], _140034))], (5931 ^ _51060) ^ [] : [-(5923 ^ [_140032, _140034, _140389, _141923] = 5929 ^ [_140032, _140034, _140389, _141923])], (5933 ^ _51060) ^ [] : [-(in(5924 ^ [_140032, _140034, _140389, _141923], 5929 ^ [_140032, _140034, _140389, _141923]))], (5935 ^ _51060) ^ [_142521] : [in(_142521, 5929 ^ [_140032, _140034, _140389, _141923]), -(in(ordered_pair(5924 ^ [_140032, _140034, _140389, _141923], _142521), _140032))]]], (5941 ^ _51060) ^ [_142666] : [-(in(_142666, 5913 ^ [_140032, _140034, _140389])), 5942 ^ _51060 : [(5943 ^ _51060) ^ [_142784] : [in(_142784, cartesian_product2(_140034, _140389)), _142784 = _142666, 5950 ^ _51060 : [(5951 ^ _51060) ^ [_142960, _142962] : [ordered_pair(_142962, _142960) = _142666, in(_142962, _140034), 5958 ^ _51060 : [(5959 ^ _51060) ^ [_143119] : [_142962 = _143119, in(_142960, _143119), 5967 ^ _51060 : [(5968 ^ _51060) ^ [] : [-(in(5966 ^ [_140032, _140034, _140389, _142666, _142784, _142960, _142962, _143119], _143119))], (5970 ^ _51060) ^ [] : [in(ordered_pair(_142960, 5966 ^ [_140032, _140034, _140389, _142666, _142784, _142960, _142962, _143119]), _140032)]]]]]]]]]]]]], (5974 ^ _51060) ^ [_143442] : [5978 ^ _51060 : [(5979 ^ _51060) ^ [] : [-(in(5975 ^ [_143442], _143442))], (5981 ^ _51060) ^ [] : [-(5976 ^ [_143442] = singleton(5975 ^ [_143442]))], (5983 ^ _51060) ^ [] : [-(in(5975 ^ [_143442], _143442))], (5985 ^ _51060) ^ [] : [-(5977 ^ [_143442] = singleton(5975 ^ [_143442]))], (5987 ^ _51060) ^ [] : [5976 ^ [_143442] = 5977 ^ [_143442]]], 5989 ^ _51060 : [(5990 ^ _51060) ^ [_143758] : [in(_143758, 5988 ^ [_143442]), 5994 ^ _51060 : [(5995 ^ _51060) ^ [] : [-(in(5993 ^ [_143442, _143758], _143442))], (5997 ^ _51060) ^ [] : [-(in(5993 ^ [_143442, _143758], _143442))], (5999 ^ _51060) ^ [] : [-(_143758 = singleton(5993 ^ [_143442, _143758]))]]], (6001 ^ _51060) ^ [_143921] : [-(in(_143921, 5988 ^ [_143442])), 6002 ^ _51060 : [(6003 ^ _51060) ^ [_143974] : [in(_143974, _143442), in(_143974, _143442), _143921 = singleton(_143974)]]]]], (6015 ^ _51060) ^ [_144151, _144153] : [6019 ^ _51060 : [(6020 ^ _51060) ^ [] : [-(6016 ^ [_144151, _144153] = 6017 ^ [_144151, _144153])], (6024 ^ _51060) ^ [] : [-(ordered_pair(6021 ^ [_144151, _144153], 6022 ^ [_144151, _144153]) = 6017 ^ [_144151, _144153])], (6026 ^ _51060) ^ [] : [-(in(6021 ^ [_144151, _144153], _144153))], (6028 ^ _51060) ^ [] : [-(6022 ^ [_144151, _144153] = singleton(6021 ^ [_144151, _144153]))], (6030 ^ _51060) ^ [] : [-(6016 ^ [_144151, _144153] = 6018 ^ [_144151, _144153])], (6034 ^ _51060) ^ [] : [-(ordered_pair(6031 ^ [_144151, _144153], 6032 ^ [_144151, _144153]) = 6018 ^ [_144151, _144153])], (6036 ^ _51060) ^ [] : [-(in(6031 ^ [_144151, _144153], _144153))], (6038 ^ _51060) ^ [] : [-(6032 ^ [_144151, _144153] = singleton(6031 ^ [_144151, _144153]))], (6040 ^ _51060) ^ [] : [6017 ^ [_144151, _144153] = 6018 ^ [_144151, _144153]]], 6042 ^ _51060 : [(6043 ^ _51060) ^ [_144754] : [in(_144754, 6041 ^ [_144151, _144153]), 6047 ^ _51060 : [(6048 ^ _51060) ^ [] : [-(in(6046 ^ [_144151, _144153, _144754], cartesian_product2(_144153, _144151)))], (6050 ^ _51060) ^ [] : [-(6046 ^ [_144151, _144153, _144754] = _144754)], (6054 ^ _51060) ^ [] : [-(ordered_pair(6051 ^ [_144151, _144153, _144754], 6052 ^ [_144151, _144153, _144754]) = _144754)], (6056 ^ _51060) ^ [] : [-(in(6051 ^ [_144151, _144153, _144754], _144153))], (6058 ^ _51060) ^ [] : [-(6052 ^ [_144151, _144153, _144754] = singleton(6051 ^ [_144151, _144153, _144754]))]]], (6060 ^ _51060) ^ [_145035] : [-(in(_145035, 6041 ^ [_144151, _144153])), 6061 ^ _51060 : [(6062 ^ _51060) ^ [_145120] : [in(_145120, cartesian_product2(_144153, _144151)), _145120 = _145035, 6069 ^ _51060 : [(6070 ^ _51060) ^ [_145263, _145265] : [ordered_pair(_145265, _145263) = _145035, in(_145265, _144153), _145263 = singleton(_145265)]]]]]]], (6082 ^ _51060) ^ [_145466] : [ordinal(_145466), 6090 ^ _51060 : [(6155 ^ _51060) ^ [] : [6088 ^ [_145466] = 6089 ^ [_145466]], (6091 ^ _51060) ^ [] : [-(6087 ^ [_145466] = 6088 ^ [_145466])], (6094 ^ _51060) ^ [] : [-(ordinal(6092 ^ [_145466]))], (6096 ^ _51060) ^ [] : [-(6088 ^ [_145466] = 6092 ^ [_145466])], (6098 ^ _51060) ^ [] : [in(6092 ^ [_145466], omega), 6101 ^ _51060 : [(6102 ^ _51060) ^ [_146347] : [element(_146347, powerset(powerset(6092 ^ [_145466]))), -(_146347 = empty_set), 6110 ^ _51060 : [(6111 ^ _51060) ^ [] : [-(in(6109 ^ [_145466, _146347], _146347))], (6113 ^ _51060) ^ [_146756] : [-(_146756 = 6109 ^ [_145466, _146347]), in(_146756, _146347), subset(6109 ^ [_145466, _146347], _146756)]]]]], (6123 ^ _51060) ^ [] : [-(6087 ^ [_145466] = 6089 ^ [_145466])], (6126 ^ _51060) ^ [] : [-(ordinal(6124 ^ [_145466]))], (6128 ^ _51060) ^ [] : [-(6089 ^ [_145466] = 6124 ^ [_145466])], (6130 ^ _51060) ^ [] : [in(6124 ^ [_145466], omega), 6133 ^ _51060 : [(6134 ^ _51060) ^ [_147497] : [element(_147497, powerset(powerset(6124 ^ [_145466]))), -(_147497 = empty_set), 6142 ^ _51060 : [(6143 ^ _51060) ^ [] : [-(in(6141 ^ [_145466, _147497], _147497))], (6145 ^ _51060) ^ [_147906] : [-(_147906 = 6141 ^ [_145466, _147497]), in(_147906, _147497), subset(6141 ^ [_145466, _147497], _147906)]]]]]], 6157 ^ _51060 : [(6158 ^ _51060) ^ [_148475] : [in(_148475, 6156 ^ [_145466]), 6162 ^ _51060 : [(6163 ^ _51060) ^ [] : [-(in(6161 ^ [_145466, _148475], succ(_145466)))], (6165 ^ _51060) ^ [] : [-(6161 ^ [_145466, _148475] = _148475)], (6168 ^ _51060) ^ [] : [-(ordinal(6166 ^ [_145466, _148475]))], (6170 ^ _51060) ^ [] : [-(_148475 = 6166 ^ [_145466, _148475])], (6172 ^ _51060) ^ [] : [in(6166 ^ [_145466, _148475], omega), 6175 ^ _51060 : [(6176 ^ _51060) ^ [_149341] : [element(_149341, powerset(powerset(6166 ^ [_145466, _148475]))), -(_149341 = empty_set), 6184 ^ _51060 : [(6185 ^ _51060) ^ [] : [-(in(6183 ^ [_145466, _148475, _149341], _149341))], (6187 ^ _51060) ^ [_149772] : [-(_149772 = 6183 ^ [_145466, _148475, _149341]), in(_149772, _149341), subset(6183 ^ [_145466, _148475, _149341], _149772)]]]]]]], (6197 ^ _51060) ^ [_150114] : [-(in(_150114, 6156 ^ [_145466])), 6198 ^ _51060 : [(6199 ^ _51060) ^ [_150298] : [in(_150298, succ(_145466)), _150298 = _150114, 6206 ^ _51060 : [(6207 ^ _51060) ^ [_150602] : [ordinal(_150602), _150114 = _150602, 6214 ^ _51060 : [(6215 ^ _51060) ^ [] : [-(in(_150602, omega))], (6218 ^ _51060) ^ [] : [-(element(6216 ^ [_145466, _150114, _150298, _150602], powerset(powerset(_150602))))], (6220 ^ _51060) ^ [] : [6216 ^ [_145466, _150114, _150298, _150602] = empty_set], (6222 ^ _51060) ^ [_151232] : [in(_151232, 6216 ^ [_145466, _150114, _150298, _150602]), 6226 ^ _51060 : [(6227 ^ _51060) ^ [] : [-(in(6225 ^ [_145466, _150114, _150298, _150602, _151232], 6216 ^ [_145466, _150114, _150298, _150602]))], (6229 ^ _51060) ^ [] : [-(subset(_151232, 6225 ^ [_145466, _150114, _150298, _150602, _151232]))], (6231 ^ _51060) ^ [] : [6225 ^ [_145466, _150114, _150298, _150602, _151232] = _151232]]]]]]]]]]], (6235 ^ _51060) ^ [_151890, _151892] : [ordinal(_151892), element(_151890, powerset(powerset(succ(_151892)))), 6247 ^ _51060 : [(6248 ^ _51060) ^ [] : [-(6244 ^ [_151890, _151892] = 6245 ^ [_151890, _151892])], (6251 ^ _51060) ^ [] : [-(in(6249 ^ [_151890, _151892], _151890))], (6253 ^ _51060) ^ [] : [-(6245 ^ [_151890, _151892] = set_difference(6249 ^ [_151890, _151892], singleton(_151892)))], (6255 ^ _51060) ^ [] : [-(6244 ^ [_151890, _151892] = 6246 ^ [_151890, _151892])], (6258 ^ _51060) ^ [] : [-(in(6256 ^ [_151890, _151892], _151890))], (6260 ^ _51060) ^ [] : [-(6246 ^ [_151890, _151892] = set_difference(6256 ^ [_151890, _151892], singleton(_151892)))], (6262 ^ _51060) ^ [] : [6245 ^ [_151890, _151892] = 6246 ^ [_151890, _151892]]], 6264 ^ _51060 : [(6265 ^ _51060) ^ [_153449] : [in(_153449, 6263 ^ [_151890, _151892]), 6269 ^ _51060 : [(6270 ^ _51060) ^ [] : [-(in(6268 ^ [_151890, _151892, _153449], powerset(_151892)))], (6272 ^ _51060) ^ [] : [-(6268 ^ [_151890, _151892, _153449] = _153449)], (6275 ^ _51060) ^ [] : [-(in(6273 ^ [_151890, _151892, _153449], _151890))], (6277 ^ _51060) ^ [] : [-(_153449 = set_difference(6273 ^ [_151890, _151892, _153449], singleton(_151892)))]]], (6279 ^ _51060) ^ [_154063] : [-(in(_154063, 6263 ^ [_151890, _151892])), 6280 ^ _51060 : [(6281 ^ _51060) ^ [_154192] : [in(_154192, powerset(_151892)), _154192 = _154063, 6288 ^ _51060 : [(6289 ^ _51060) ^ [_154445] : [in(_154445, _151890), _154063 = set_difference(_154445, singleton(_151892))]]]]]]], (6297 ^ _51060) ^ [_154787, _154789, _154791] : [relation(_154789), relation(_154787), function(_154787), 6313 ^ _51060 : [(6314 ^ _51060) ^ [] : [-(6310 ^ [_154787, _154789, _154791] = 6311 ^ [_154787, _154789, _154791])], (6318 ^ _51060) ^ [] : [-(6311 ^ [_154787, _154789, _154791] = ordered_pair(6315 ^ [_154787, _154789, _154791], 6316 ^ [_154787, _154789, _154791]))], (6320 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_154787, 6315 ^ [_154787, _154789, _154791]), apply(_154787, 6316 ^ [_154787, _154789, _154791])), _154789))], (6322 ^ _51060) ^ [] : [-(6310 ^ [_154787, _154789, _154791] = 6312 ^ [_154787, _154789, _154791])], (6326 ^ _51060) ^ [] : [-(6312 ^ [_154787, _154789, _154791] = ordered_pair(6323 ^ [_154787, _154789, _154791], 6324 ^ [_154787, _154789, _154791]))], (6328 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_154787, 6323 ^ [_154787, _154789, _154791]), apply(_154787, 6324 ^ [_154787, _154789, _154791])), _154789))], (6330 ^ _51060) ^ [] : [6311 ^ [_154787, _154789, _154791] = 6312 ^ [_154787, _154789, _154791]]], 6332 ^ _51060 : [(6333 ^ _51060) ^ [_156897] : [in(_156897, 6331 ^ [_154787, _154789, _154791]), 6337 ^ _51060 : [(6338 ^ _51060) ^ [] : [-(in(6336 ^ [_154787, _154789, _154791, _156897], cartesian_product2(_154791, _154791)))], (6340 ^ _51060) ^ [] : [-(6336 ^ [_154787, _154789, _154791, _156897] = _156897)], (6344 ^ _51060) ^ [] : [-(_156897 = ordered_pair(6341 ^ [_154787, _154789, _154791, _156897], 6342 ^ [_154787, _154789, _154791, _156897]))], (6346 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_154787, 6341 ^ [_154787, _154789, _154791, _156897]), apply(_154787, 6342 ^ [_154787, _154789, _154791, _156897])), _154789))]]], (6348 ^ _51060) ^ [_157706] : [-(in(_157706, 6331 ^ [_154787, _154789, _154791])), 6349 ^ _51060 : [(6350 ^ _51060) ^ [_157854] : [in(_157854, cartesian_product2(_154791, _154791)), _157854 = _157706, 6357 ^ _51060 : [(6358 ^ _51060) ^ [_158145, _158147] : [_157706 = ordered_pair(_158147, _158145), in(ordered_pair(apply(_154787, _158147), apply(_154787, _158145)), _154789)]]]]]]], (6366 ^ _51060) ^ [_158493] : [6370 ^ _51060 : [(6371 ^ _51060) ^ [] : [-(6367 ^ [_158493] = 6368 ^ [_158493])], (6373 ^ _51060) ^ [] : [-(ordinal(6368 ^ [_158493]))], (6375 ^ _51060) ^ [] : [-(6367 ^ [_158493] = 6369 ^ [_158493])], (6377 ^ _51060) ^ [] : [-(ordinal(6369 ^ [_158493]))], (6379 ^ _51060) ^ [] : [6368 ^ [_158493] = 6369 ^ [_158493]]], 6381 ^ _51060 : [(6382 ^ _51060) ^ [_159328] : [in(_159328, 6380 ^ [_158493]), 6386 ^ _51060 : [(6387 ^ _51060) ^ [] : [-(in(6385 ^ [_158493, _159328], _158493))], (6389 ^ _51060) ^ [] : [-(6385 ^ [_158493, _159328] = _159328)], (6391 ^ _51060) ^ [] : [-(ordinal(_159328))]]], (6393 ^ _51060) ^ [_159724] : [-(in(_159724, 6380 ^ [_158493])), 6394 ^ _51060 : [(6395 ^ _51060) ^ [_159828] : [in(_159828, _158493), _159828 = _159724, ordinal(_159724)]]]]], (6407 ^ _51060) ^ [_160216, _160218, _160220] : [element(_160218, powerset(powerset(_160220))), relation(_160216), function(_160216), 6423 ^ _51060 : [(6424 ^ _51060) ^ [] : [-(6420 ^ [_160216, _160218, _160220] = 6421 ^ [_160216, _160218, _160220])], (6426 ^ _51060) ^ [] : [-(in(relation_image(_160216, 6421 ^ [_160216, _160218, _160220]), _160218))], (6428 ^ _51060) ^ [] : [-(6420 ^ [_160216, _160218, _160220] = 6422 ^ [_160216, _160218, _160220])], (6430 ^ _51060) ^ [] : [-(in(relation_image(_160216, 6422 ^ [_160216, _160218, _160220]), _160218))], (6432 ^ _51060) ^ [] : [6421 ^ [_160216, _160218, _160220] = 6422 ^ [_160216, _160218, _160220]]], 6434 ^ _51060 : [(6435 ^ _51060) ^ [_161502] : [in(_161502, 6433 ^ [_160216, _160218, _160220]), 6439 ^ _51060 : [(6440 ^ _51060) ^ [] : [-(in(6438 ^ [_160216, _160218, _160220, _161502], powerset(relation_dom(_160216))))], (6442 ^ _51060) ^ [] : [-(6438 ^ [_160216, _160218, _160220, _161502] = _161502)], (6444 ^ _51060) ^ [] : [-(in(relation_image(_160216, _161502), _160218))]]], (6446 ^ _51060) ^ [_161970] : [-(in(_161970, 6433 ^ [_160216, _160218, _160220])), 6447 ^ _51060 : [(6448 ^ _51060) ^ [_162094] : [in(_162094, powerset(relation_dom(_160216))), _162094 = _161970, in(relation_image(_160216, _161970), _160218)]]]]], (6460 ^ _51060) ^ [_162524, _162526] : [ordinal(_162524), 6468 ^ _51060 : [(6469 ^ _51060) ^ [] : [-(6465 ^ [_162524, _162526] = 6466 ^ [_162524, _162526])], (6472 ^ _51060) ^ [] : [-(ordinal(6470 ^ [_162524, _162526]))], (6474 ^ _51060) ^ [] : [-(6466 ^ [_162524, _162526] = 6470 ^ [_162524, _162526])], (6476 ^ _51060) ^ [] : [-(in(6470 ^ [_162524, _162526], _162526))], (6478 ^ _51060) ^ [] : [-(6465 ^ [_162524, _162526] = 6467 ^ [_162524, _162526])], (6481 ^ _51060) ^ [] : [-(ordinal(6479 ^ [_162524, _162526]))], (6483 ^ _51060) ^ [] : [-(6467 ^ [_162524, _162526] = 6479 ^ [_162524, _162526])], (6485 ^ _51060) ^ [] : [-(in(6479 ^ [_162524, _162526], _162526))], (6487 ^ _51060) ^ [] : [6466 ^ [_162524, _162526] = 6467 ^ [_162524, _162526]]], 6489 ^ _51060 : [(6490 ^ _51060) ^ [_164126] : [in(_164126, 6488 ^ [_162524, _162526]), 6494 ^ _51060 : [(6495 ^ _51060) ^ [] : [-(in(6493 ^ [_162524, _162526, _164126], succ(_162524)))], (6497 ^ _51060) ^ [] : [-(6493 ^ [_162524, _162526, _164126] = _164126)], (6500 ^ _51060) ^ [] : [-(ordinal(6498 ^ [_162524, _162526, _164126]))], (6502 ^ _51060) ^ [] : [-(_164126 = 6498 ^ [_162524, _162526, _164126])], (6504 ^ _51060) ^ [] : [-(in(6498 ^ [_162524, _162526, _164126], _162526))]]], (6506 ^ _51060) ^ [_164813] : [-(in(_164813, 6488 ^ [_162524, _162526])), 6507 ^ _51060 : [(6508 ^ _51060) ^ [_164942] : [in(_164942, succ(_162524)), _164942 = _164813, 6515 ^ _51060 : [(6516 ^ _51060) ^ [_165195] : [ordinal(_165195), _164813 = _165195, in(_165195, _162526)]]]]]]], (6528 ^ _51060) ^ [_165610, _165612] : [-(empty(_165612)), relation(_165610), 6536 ^ _51060 : [(6537 ^ _51060) ^ [_166076, _166078] : [in(_166076, 6535 ^ [_165610, _165612, _166078]), 6540 ^ _51060 : [(6541 ^ _51060) ^ [] : [-(in(_166076, cartesian_product2(_165612, _166078)))], (6545 ^ _51060) ^ [] : [-(ordered_pair(6542 ^ [_165610, _165612, _166076, _166078], 6543 ^ [_165610, _165612, _166076, _166078]) = _166076)], (6547 ^ _51060) ^ [] : [-(in(6542 ^ [_165610, _165612, _166076, _166078], _165612))], (6550 ^ _51060) ^ [] : [-(6542 ^ [_165610, _165612, _166076, _166078] = 6548 ^ [_165610, _165612, _166076, _166078])], (6552 ^ _51060) ^ [] : [-(in(6543 ^ [_165610, _165612, _166076, _166078], 6548 ^ [_165610, _165612, _166076, _166078]))], (6554 ^ _51060) ^ [_167078] : [in(_167078, 6548 ^ [_165610, _165612, _166076, _166078]), -(in(ordered_pair(6543 ^ [_165610, _165612, _166076, _166078], _167078), _165610))]]], (6560 ^ _51060) ^ [_167331, _167333] : [-(in(_167331, 6535 ^ [_165610, _165612, _167333])), in(_167331, cartesian_product2(_165612, _167333)), 6565 ^ _51060 : [(6566 ^ _51060) ^ [_167598, _167600] : [ordered_pair(_167600, _167598) = _167331, in(_167600, _165612), 6573 ^ _51060 : [(6574 ^ _51060) ^ [_167886] : [_167600 = _167886, in(_167598, _167886), 6582 ^ _51060 : [(6583 ^ _51060) ^ [] : [-(in(6581 ^ [_165610, _165612, _167331, _167333, _167598, _167600, _167886], _167886))], (6585 ^ _51060) ^ [] : [in(ordered_pair(_167598, 6581 ^ [_165610, _165612, _167331, _167333, _167598, _167600, _167886]), _165610)]]]]]]]]], (6590 ^ _51060) ^ [_168667, _168669, _168671] : [in(_168667, 6588 ^ [_168669, _168671]), 6593 ^ _51060 : [(6594 ^ _51060) ^ [] : [-(in(_168667, cartesian_product2(_168671, _168669)))], (6598 ^ _51060) ^ [] : [-(ordered_pair(6595 ^ [_168667, _168669, _168671], 6596 ^ [_168667, _168669, _168671]) = _168667)], (6600 ^ _51060) ^ [] : [-(in(6595 ^ [_168667, _168669, _168671], _168671))], (6602 ^ _51060) ^ [] : [-(6596 ^ [_168667, _168669, _168671] = singleton(6595 ^ [_168667, _168669, _168671]))]]], (6604 ^ _51060) ^ [_169313, _169315, _169317] : [-(in(_169313, 6588 ^ [_169315, _169317])), in(_169313, cartesian_product2(_169317, _169315)), 6609 ^ _51060 : [(6610 ^ _51060) ^ [_169539, _169541] : [ordered_pair(_169541, _169539) = _169313, in(_169541, _169317), _169539 = singleton(_169541)]]], (6622 ^ _51060) ^ [_169935] : [ordinal(_169935), 6626 ^ _51060 : [(6663 ^ _51060) ^ [_171732] : [-(in(_171732, 6625 ^ [_169935])), in(_171732, succ(_169935)), 6668 ^ _51060 : [(6669 ^ _51060) ^ [_171986] : [ordinal(_171986), _171732 = _171986, 6676 ^ _51060 : [(6677 ^ _51060) ^ [] : [-(in(_171986, omega))], (6680 ^ _51060) ^ [] : [-(element(6678 ^ [_169935, _171732, _171986], powerset(powerset(_171986))))], (6682 ^ _51060) ^ [] : [6678 ^ [_169935, _171732, _171986] = empty_set], (6684 ^ _51060) ^ [_172592] : [in(_172592, 6678 ^ [_169935, _171732, _171986]), 6688 ^ _51060 : [(6689 ^ _51060) ^ [] : [-(in(6687 ^ [_169935, _171732, _171986, _172592], 6678 ^ [_169935, _171732, _171986]))], (6691 ^ _51060) ^ [] : [-(subset(_172592, 6687 ^ [_169935, _171732, _171986, _172592]))], (6693 ^ _51060) ^ [] : [6687 ^ [_169935, _171732, _171986, _172592] = _172592]]]]]]], (6627 ^ _51060) ^ [_170322] : [in(_170322, 6625 ^ [_169935]), 6630 ^ _51060 : [(6631 ^ _51060) ^ [] : [-(in(_170322, succ(_169935)))], (6634 ^ _51060) ^ [] : [-(ordinal(6632 ^ [_169935, _170322]))], (6636 ^ _51060) ^ [] : [-(_170322 = 6632 ^ [_169935, _170322])], (6638 ^ _51060) ^ [] : [in(6632 ^ [_169935, _170322], omega), 6641 ^ _51060 : [(6642 ^ _51060) ^ [_170961] : [element(_170961, powerset(powerset(6632 ^ [_169935, _170322]))), -(_170961 = empty_set), 6650 ^ _51060 : [(6651 ^ _51060) ^ [] : [-(in(6649 ^ [_169935, _170322, _170961], _170961))], (6653 ^ _51060) ^ [_171392] : [-(_171392 = 6649 ^ [_169935, _170322, _170961]), in(_171392, _170961), subset(6649 ^ [_169935, _170322, _170961], _171392)]]]]]]]]], (6697 ^ _51060) ^ [_173208, _173210] : [ordinal(_173210), element(_173208, powerset(powerset(succ(_173210)))), 6705 ^ _51060 : [(6706 ^ _51060) ^ [_173582] : [in(_173582, 6704 ^ [_173208, _173210]), 6709 ^ _51060 : [(6710 ^ _51060) ^ [] : [-(in(_173582, powerset(_173210)))], (6713 ^ _51060) ^ [] : [-(in(6711 ^ [_173208, _173210, _173582], _173208))], (6715 ^ _51060) ^ [] : [-(_173582 = set_difference(6711 ^ [_173208, _173210, _173582], singleton(_173210)))]]], (6717 ^ _51060) ^ [_174018] : [-(in(_174018, 6704 ^ [_173208, _173210])), in(_174018, powerset(_173210)), 6722 ^ _51060 : [(6723 ^ _51060) ^ [_174221] : [in(_174221, _173208), _174018 = set_difference(_174221, singleton(_173210))]]]]], (6731 ^ _51060) ^ [_174545, _174547, _174549] : [relation(_174547), relation(_174545), function(_174545), 6743 ^ _51060 : [(6744 ^ _51060) ^ [_175034] : [in(_175034, 6742 ^ [_174545, _174547, _174549]), 6747 ^ _51060 : [(6748 ^ _51060) ^ [] : [-(in(_175034, cartesian_product2(_174549, _174549)))], (6752 ^ _51060) ^ [] : [-(_175034 = ordered_pair(6749 ^ [_174545, _174547, _174549, _175034], 6750 ^ [_174545, _174547, _174549, _175034]))], (6754 ^ _51060) ^ [] : [-(in(ordered_pair(apply(_174545, 6749 ^ [_174545, _174547, _174549, _175034]), apply(_174545, 6750 ^ [_174545, _174547, _174549, _175034])), _174547))]]], (6756 ^ _51060) ^ [_175642] : [-(in(_175642, 6742 ^ [_174545, _174547, _174549])), in(_175642, cartesian_product2(_174549, _174549)), 6761 ^ _51060 : [(6762 ^ _51060) ^ [_175883, _175885] : [_175642 = ordered_pair(_175885, _175883), in(ordered_pair(apply(_174545, _175885), apply(_174545, _175883)), _174547)]]]]], (6771 ^ _51060) ^ [_176311, _176313] : [in(_176311, 6769 ^ [_176313]), 6774 ^ _51060 : [(6775 ^ _51060) ^ [] : [-(in(_176311, _176313))], (6777 ^ _51060) ^ [] : [-(ordinal(_176311))]]], (6779 ^ _51060) ^ [_176556, _176558] : [-(in(_176556, 6769 ^ [_176558])), in(_176556, _176558), ordinal(_176556)], (6789 ^ _51060) ^ [_176879, _176881, _176883] : [element(_176881, powerset(powerset(_176883))), relation(_176879), function(_176879), 6801 ^ _51060 : [(6802 ^ _51060) ^ [_177330] : [in(_177330, 6800 ^ [_176879, _176881, _176883]), 6805 ^ _51060 : [(6806 ^ _51060) ^ [] : [-(in(_177330, powerset(relation_dom(_176879))))], (6808 ^ _51060) ^ [] : [-(in(relation_image(_176879, _177330), _176881))]]], (6810 ^ _51060) ^ [_177621] : [-(in(_177621, 6800 ^ [_176879, _176881, _176883])), in(_177621, powerset(relation_dom(_176879))), in(relation_image(_176879, _177621), _176881)]]], (6820 ^ _51060) ^ [_177989, _177991] : [ordinal(_177989), 6824 ^ _51060 : [(6825 ^ _51060) ^ [_178262] : [in(_178262, 6823 ^ [_177989, _177991]), 6828 ^ _51060 : [(6829 ^ _51060) ^ [] : [-(in(_178262, succ(_177989)))], (6832 ^ _51060) ^ [] : [-(ordinal(6830 ^ [_177989, _177991, _178262]))], (6834 ^ _51060) ^ [] : [-(_178262 = 6830 ^ [_177989, _177991, _178262])], (6836 ^ _51060) ^ [] : [-(in(6830 ^ [_177989, _177991, _178262], _177991))]]], (6838 ^ _51060) ^ [_178771] : [-(in(_178771, 6823 ^ [_177989, _177991])), in(_178771, succ(_177989)), 6843 ^ _51060 : [(6844 ^ _51060) ^ [_178974] : [ordinal(_178974), _178771 = _178974, in(_178974, _177991)]]]]], (6856 ^ _51060) ^ [_179367, _179369] : [-(empty(_179369)), relation(_179367), 6913 ^ _51060 : [(6914 ^ _51060) ^ [] : [-(relation(6912 ^ [_179367, _179369]))], (6916 ^ _51060) ^ [] : [-(function(6912 ^ [_179367, _179369]))], (6918 ^ _51060) ^ [] : [-(relation_dom(6912 ^ [_179367, _179369]) = _179369)], (6920 ^ _51060) ^ [_182457] : [in(_182457, _179369), 6924 ^ _51060 : [(6925 ^ _51060) ^ [] : [-(_182457 = 6923 ^ [_179367, _179369, _182457])], (6927 ^ _51060) ^ [] : [-(in(apply(6912 ^ [_179367, _179369], _182457), 6923 ^ [_179367, _179369, _182457]))], (6929 ^ _51060) ^ [_182901] : [in(_182901, 6923 ^ [_179367, _179369, _182457]), -(in(ordered_pair(apply(6912 ^ [_179367, _179369], _182457), _182901), _179367))]]]], 6897 ^ _51060 : [(6898 ^ _51060) ^ [] : [-(in(6896 ^ [_179367, _179369], _179369))], (6900 ^ _51060) ^ [_181643, _181645] : [6896 ^ [_179367, _179369] = _181643, in(_181645, _181643), 6908 ^ _51060 : [(6909 ^ _51060) ^ [] : [-(in(6907 ^ [_179367, _179369, _181643, _181645], _181643))], (6911 ^ _51060) ^ [] : [in(ordered_pair(_181645, 6907 ^ [_179367, _179369, _181643, _181645]), _179367)]]]], 6870 ^ _51060 : [(6895 ^ _51060) ^ [] : [6868 ^ [_179367, _179369] = 6869 ^ [_179367, _179369]], (6871 ^ _51060) ^ [] : [-(in(6867 ^ [_179367, _179369], _179369))], (6874 ^ _51060) ^ [] : [-(6867 ^ [_179367, _179369] = 6872 ^ [_179367, _179369])], (6876 ^ _51060) ^ [] : [-(in(6868 ^ [_179367, _179369], 6872 ^ [_179367, _179369]))], (6878 ^ _51060) ^ [_180696] : [in(_180696, 6872 ^ [_179367, _179369]), -(in(ordered_pair(6868 ^ [_179367, _179369], _180696), _179367))], (6885 ^ _51060) ^ [] : [-(6867 ^ [_179367, _179369] = 6883 ^ [_179367, _179369])], (6887 ^ _51060) ^ [] : [-(in(6869 ^ [_179367, _179369], 6883 ^ [_179367, _179369]))], (6889 ^ _51060) ^ [_181172] : [in(_181172, 6883 ^ [_179367, _179369]), -(in(ordered_pair(6869 ^ [_179367, _179369], _181172), _179367))]]], (6935 ^ _51060) ^ [_183185] : [6941 ^ _51060 : [(6942 ^ _51060) ^ [] : [-(in(6938 ^ [_183185], _183185))], (6944 ^ _51060) ^ [] : [-(6939 ^ [_183185] = singleton(6938 ^ [_183185]))], (6946 ^ _51060) ^ [] : [-(6940 ^ [_183185] = singleton(6938 ^ [_183185]))], (6948 ^ _51060) ^ [] : [6939 ^ [_183185] = 6940 ^ [_183185]]], 6950 ^ _51060 : [(6951 ^ _51060) ^ [] : [-(in(6949 ^ [_183185], _183185))], (6953 ^ _51060) ^ [_184039] : [_184039 = singleton(6949 ^ [_183185])]], 6955 ^ _51060 : [(6956 ^ _51060) ^ [] : [-(relation(6954 ^ [_183185]))], (6958 ^ _51060) ^ [] : [-(function(6954 ^ [_183185]))], (6960 ^ _51060) ^ [] : [-(relation_dom(6954 ^ [_183185]) = _183185)], (6962 ^ _51060) ^ [_184411] : [in(_184411, _183185), -(apply(6954 ^ [_183185], _184411) = singleton(_184411))]]], (6968 ^ _51060) ^ [] : [7023 ^ _51060 : [(7024 ^ _51060) ^ [_186644] : [ordinal(_186644), in(_186644, omega), 7031 ^ _51060 : [(7032 ^ _51060) ^ [_186900] : [element(_186900, powerset(powerset(_186644))), -(_186900 = empty_set), 7040 ^ _51060 : [(7041 ^ _51060) ^ [] : [-(in(7039 ^ [_186644, _186900], _186900))], (7043 ^ _51060) ^ [_187299] : [-(_187299 = 7039 ^ [_186644, _186900]), in(_187299, _186900), subset(7039 ^ [_186644, _186900], _187299)]]]]]], 6970 ^ _51060 : [(6971 ^ _51060) ^ [] : [-(ordinal(6969 ^ []))], (7006 ^ _51060) ^ [] : [-(in(6969 ^ [], omega))], (7009 ^ _51060) ^ [] : [-(element(7007 ^ [], powerset(powerset(6969 ^ []))))], (7011 ^ _51060) ^ [] : [7007 ^ [] = empty_set], (7013 ^ _51060) ^ [_186239] : [in(_186239, 7007 ^ []), 7017 ^ _51060 : [(7018 ^ _51060) ^ [] : [-(in(7016 ^ [_186239], 7007 ^ []))], (7020 ^ _51060) ^ [] : [-(subset(_186239, 7016 ^ [_186239]))], (7022 ^ _51060) ^ [] : [7016 ^ [_186239] = _186239]]], (6973 ^ _51060) ^ [_184931] : [ordinal(_184931), in(_184931, 6969 ^ []), in(_184931, omega), 6984 ^ _51060 : [(6985 ^ _51060) ^ [_185268] : [element(_185268, powerset(powerset(_184931))), -(_185268 = empty_set), 6993 ^ _51060 : [(6994 ^ _51060) ^ [] : [-(in(6992 ^ [_184931, _185268], _185268))], (6996 ^ _51060) ^ [_185667] : [-(_185667 = 6992 ^ [_184931, _185268]), in(_185667, _185268), subset(6992 ^ [_184931, _185268], _185667)]]]]]]], (7054 ^ _51060) ^ [_187730] : [-(relation(7052 ^ [_187730]))], (7056 ^ _51060) ^ [_187798] : [-(function(7052 ^ [_187798]))], (7058 ^ _51060) ^ [_187866] : [-(relation_dom(7052 ^ [_187866]) = _187866)], (7060 ^ _51060) ^ [_187946, _187948] : [in(_187946, _187948), -(apply(7052 ^ [_187948], _187946) = singleton(_187946))], (7066 ^ _51060) ^ [_188182, _188184] : [disjoint(_188184, _188182), -(disjoint(_188182, _188184))], (7072 ^ _51060) ^ [_188392, _188394] : [equipotent(_188394, _188392), -(equipotent(_188392, _188394))], (7078 ^ _51060) ^ [_188659, _188661, _188663, _188665] : [in(ordered_pair(_188665, _188663), cartesian_product2(_188661, _188659)), 7081 ^ _51060 : [(7082 ^ _51060) ^ [] : [-(in(_188665, _188661))], (7084 ^ _51060) ^ [] : [-(in(_188663, _188659))]]], (7086 ^ _51060) ^ [_188924, _188926, _188928, _188930] : [-(in(ordered_pair(_188930, _188928), cartesian_product2(_188926, _188924))), in(_188930, _188926), in(_188928, _188924)], (7096 ^ _51060) ^ [_189228] : [-(in(_189228, succ(_189228)))], (7098 ^ _51060) ^ [_189365, _189367, _189369, _189371] : [unordered_pair(_189371, _189369) = unordered_pair(_189367, _189365), -(_189371 = _189367), -(_189371 = _189365)], (7108 ^ _51060) ^ [_189715, _189717, _189719] : [relation(_189715), 7111 ^ _51060 : [(7112 ^ _51060) ^ [] : [in(_189719, relation_rng(relation_rng_restriction(_189717, _189715))), 7115 ^ _51060 : [(7116 ^ _51060) ^ [] : [-(in(_189719, _189717))], (7118 ^ _51060) ^ [] : [-(in(_189719, relation_rng(_189715)))]]], (7120 ^ _51060) ^ [] : [-(in(_189719, relation_rng(relation_rng_restriction(_189717, _189715)))), in(_189719, _189717), in(_189719, relation_rng(_189715))]]], (7130 ^ _51060) ^ [_190374, _190376] : [relation(_190374), -(subset(relation_rng(relation_rng_restriction(_190376, _190374)), _190376))], (7136 ^ _51060) ^ [_190592, _190594] : [relation(_190592), -(subset(relation_rng_restriction(_190594, _190592), _190592))], (7142 ^ _51060) ^ [_190806, _190808] : [relation(_190806), -(subset(relation_rng(relation_rng_restriction(_190808, _190806)), relation_rng(_190806)))], (7148 ^ _51060) ^ [_191042, _191044, _191046] : [subset(_191046, _191044), 7151 ^ _51060 : [(7152 ^ _51060) ^ [] : [-(subset(cartesian_product2(_191046, _191042), cartesian_product2(_191044, _191042)))], (7154 ^ _51060) ^ [] : [-(subset(cartesian_product2(_191042, _191046), cartesian_product2(_191042, _191044)))]]], (7156 ^ _51060) ^ [_191359, _191361] : [relation(_191359), -(relation_rng(relation_rng_restriction(_191361, _191359)) = set_intersection2(relation_rng(_191359), _191361))], (7162 ^ _51060) ^ [_191615, _191617, _191619, _191621] : [-(subset(cartesian_product2(_191621, _191617), cartesian_product2(_191619, _191615))), subset(_191621, _191619), subset(_191617, _191615)], (7172 ^ _51060) ^ [_191960, _191962, _191964] : [relation_of2_as_subset(_191960, _191964, _191962), 7175 ^ _51060 : [(7176 ^ _51060) ^ [] : [-(subset(relation_dom(_191960), _191964))], (7178 ^ _51060) ^ [] : [-(subset(relation_rng(_191960), _191962))]]], (7180 ^ _51060) ^ [_192263, _192265] : [subset(_192265, _192263), -(set_union2(_192265, _192263) = _192263)], (7187 ^ _51060) ^ [_192585] : [-(in(_192585, 7185 ^ [_192585]))], (7189 ^ _51060) ^ [_192697, _192699, _192701] : [-(in(_192697, 7185 ^ [_192701])), in(_192699, 7185 ^ [_192701]), subset(_192697, _192699)], (7199 ^ _51060) ^ [_193012, _193014] : [in(_193012, 7185 ^ [_193014]), -(in(powerset(_193012), 7185 ^ [_193014]))], (7205 ^ _51060) ^ [_193212, _193214] : [subset(_193212, 7185 ^ [_193214]), -(are_equipotent(_193212, 7185 ^ [_193214])), -(in(_193212, 7185 ^ [_193214]))], (7215 ^ _51060) ^ [_193552, _193554] : [-(finite(_193554)), subset(_193554, _193552), finite(_193552)], (7225 ^ _51060) ^ [_193861, _193863, _193865] : [relation(_193861), -(relation_dom_restriction(relation_rng_restriction(_193865, _193861), _193863) = relation_rng_restriction(_193865, relation_dom_restriction(_193861, _193863)))], (7231 ^ _51060) ^ [_194113, _194115, _194117] : [relation(_194113), 7234 ^ _51060 : [(7235 ^ _51060) ^ [] : [in(_194117, relation_image(_194113, _194115)), 7239 ^ _51060 : [(7240 ^ _51060) ^ [] : [-(in(7238 ^ [_194113, _194115, _194117], relation_dom(_194113)))], (7242 ^ _51060) ^ [] : [-(in(ordered_pair(7238 ^ [_194113, _194115, _194117], _194117), _194113))], (7244 ^ _51060) ^ [] : [-(in(7238 ^ [_194113, _194115, _194117], _194115))]]], (7246 ^ _51060) ^ [] : [-(in(_194117, relation_image(_194113, _194115))), 7247 ^ _51060 : [(7248 ^ _51060) ^ [_194714] : [in(_194714, relation_dom(_194113)), in(ordered_pair(_194714, _194117), _194113), in(_194714, _194115)]]]]], (7260 ^ _51060) ^ [_195111, _195113] : [relation(_195111), -(subset(relation_image(_195111, _195113), relation_rng(_195111)))], (7266 ^ _51060) ^ [_195329, _195331] : [-(subset(relation_image(_195329, relation_inverse_image(_195329, _195331)), _195331)), relation(_195329), function(_195329)], (7276 ^ _51060) ^ [_195636, _195638] : [relation(_195636), -(relation_image(_195636, _195638) = relation_image(_195636, set_intersection2(relation_dom(_195636), _195638)))], (7282 ^ _51060) ^ [_195866, _195868] : [relation(_195866), subset(_195868, relation_dom(_195866)), -(subset(_195868, relation_inverse_image(_195866, relation_image(_195866, _195868))))], (7292 ^ _51060) ^ [_196165] : [relation(_196165), -(relation_image(_196165, relation_dom(_196165)) = relation_rng(_196165))], (7298 ^ _51060) ^ [_196381, _196383] : [relation(_196381), function(_196381), subset(_196383, relation_rng(_196381)), -(relation_image(_196381, relation_inverse_image(_196381, _196383)) = _196383)], (7312 ^ _51060) ^ [_196811, _196813, _196815, _196817] : [relation_of2_as_subset(_196811, _196813, _196817), subset(relation_rng(_196811), _196815), -(relation_of2_as_subset(_196811, _196813, _196815))], (7322 ^ _51060) ^ [_197138, _197140] : [finite(_197140), -(finite(set_intersection2(_197140, _197138)))], (7328 ^ _51060) ^ [_197336] : [relation(_197336), 7331 ^ _51060 : [(7332 ^ _51060) ^ [_197476] : [relation(_197476), -(relation_rng(relation_composition(_197336, _197476)) = relation_image(_197476, relation_rng(_197336)))]]], (7338 ^ _51060) ^ [_197725, _197727, _197729] : [relation(_197725), 7341 ^ _51060 : [(7342 ^ _51060) ^ [] : [in(_197729, relation_inverse_image(_197725, _197727)), 7346 ^ _51060 : [(7347 ^ _51060) ^ [] : [-(in(7345 ^ [_197725, _197727, _197729], relation_rng(_197725)))], (7349 ^ _51060) ^ [] : [-(in(ordered_pair(_197729, 7345 ^ [_197725, _197727, _197729]), _197725))], (7351 ^ _51060) ^ [] : [-(in(7345 ^ [_197725, _197727, _197729], _197727))]]], (7353 ^ _51060) ^ [] : [-(in(_197729, relation_inverse_image(_197725, _197727))), 7354 ^ _51060 : [(7355 ^ _51060) ^ [_198326] : [in(_198326, relation_rng(_197725)), in(ordered_pair(_197729, _198326), _197725), in(_198326, _197727)]]]]], (7367 ^ _51060) ^ [_198723, _198725] : [relation(_198723), -(subset(relation_inverse_image(_198723, _198725), relation_dom(_198723)))], (7373 ^ _51060) ^ [_198969, _198971, _198973, _198975] : [relation_of2_as_subset(_198969, _198971, _198975), subset(_198975, _198973), -(relation_of2_as_subset(_198969, _198971, _198973))], (7383 ^ _51060) ^ [_199306, _199308, _199310] : [relation(_199306), 7386 ^ _51060 : [(7387 ^ _51060) ^ [] : [in(_199310, relation_restriction(_199306, _199308)), 7390 ^ _51060 : [(7391 ^ _51060) ^ [] : [-(in(_199310, _199306))], (7393 ^ _51060) ^ [] : [-(in(_199310, cartesian_product2(_199308, _199308)))]]], (7395 ^ _51060) ^ [] : [-(in(_199310, relation_restriction(_199306, _199308))), in(_199310, _199306), in(_199310, cartesian_product2(_199308, _199308))]]], (7405 ^ _51060) ^ [_199962, _199964] : [relation(_199962), -(_199964 = empty_set), subset(_199964, relation_rng(_199962)), relation_inverse_image(_199962, _199964) = empty_set], (7419 ^ _51060) ^ [_200376, _200378, _200380] : [relation(_200376), subset(_200380, _200378), -(subset(relation_inverse_image(_200376, _200380), relation_inverse_image(_200376, _200378)))], (7429 ^ _51060) ^ [_200695, _200697] : [relation(_200695), function(_200695), finite(_200697), -(finite(relation_image(_200695, _200697)))], (7443 ^ _51060) ^ [_201083, _201085] : [relation(_201083), -(relation_restriction(_201083, _201085) = relation_dom_restriction(relation_rng_restriction(_201085, _201083), _201085))], (7449 ^ _51060) ^ [_201294, _201296] : [-(subset(set_intersection2(_201296, _201294), _201296))], (7451 ^ _51060) ^ [_201392] : [finite(_201392), 7454 ^ _51060 : [(7455 ^ _51060) ^ [_201567] : [element(_201567, powerset(powerset(_201392))), -(_201567 = empty_set), 7463 ^ _51060 : [(7464 ^ _51060) ^ [] : [-(in(7462 ^ [_201392, _201567], _201567))], (7466 ^ _51060) ^ [_201966] : [-(_201966 = 7462 ^ [_201392, _201567]), in(_201966, _201567), subset(7462 ^ [_201392, _201567], _201966)]]]]], (7476 ^ _51060) ^ [_202323, _202325] : [relation(_202323), -(relation_restriction(_202323, _202325) = relation_rng_restriction(_202325, relation_dom_restriction(_202323, _202325)))], (7482 ^ _51060) ^ [_202563, _202565, _202567] : [relation(_202563), in(_202567, relation_field(relation_restriction(_202563, _202565))), 7489 ^ _51060 : [(7490 ^ _51060) ^ [] : [-(in(_202567, relation_field(_202563)))], (7492 ^ _51060) ^ [] : [-(in(_202567, _202565))]]], (7494 ^ _51060) ^ [_202975, _202977, _202979] : [-(subset(_202979, set_intersection2(_202977, _202975))), subset(_202979, _202977), subset(_202979, _202975)], (7504 ^ _51060) ^ [_203261] : [-(set_union2(_203261, empty_set) = _203261)], (7506 ^ _51060) ^ [_203371, _203373] : [in(_203373, _203371), -(element(_203373, _203371))], (7512 ^ _51060) ^ [_203595, _203597, _203599] : [-(subset(_203599, _203595)), subset(_203599, _203597), subset(_203597, _203595)], (7522 ^ _51060) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (7524 ^ _51060) ^ [_203971, _203973, _203975] : [relation(_203971), in(ordered_pair(_203975, _203973), _203971), 7531 ^ _51060 : [(7532 ^ _51060) ^ [] : [-(in(_203975, relation_dom(_203971)))], (7534 ^ _51060) ^ [] : [-(in(_203973, relation_rng(_203971)))]]], (7536 ^ _51060) ^ [_204369, _204371] : [relation(_204369), 7539 ^ _51060 : [(7540 ^ _51060) ^ [] : [-(subset(relation_field(relation_restriction(_204369, _204371)), relation_field(_204369)))], (7542 ^ _51060) ^ [] : [-(subset(relation_field(relation_restriction(_204369, _204371)), _204371))]]], (7544 ^ _51060) ^ [_204676, _204678] : [relation(_204676), function(_204676), 7551 ^ _51060 : [(7552 ^ _51060) ^ [_204926] : [relation(_204926), function(_204926), 7559 ^ _51060 : [(7560 ^ _51060) ^ [] : [in(_204678, relation_dom(relation_composition(_204926, _204676))), 7563 ^ _51060 : [(7564 ^ _51060) ^ [] : [-(in(_204678, relation_dom(_204926)))], (7566 ^ _51060) ^ [] : [-(in(apply(_204926, _204678), relation_dom(_204676)))]]], (7568 ^ _51060) ^ [] : [-(in(_204678, relation_dom(relation_composition(_204926, _204676)))), in(_204678, relation_dom(_204926)), in(apply(_204926, _204678), relation_dom(_204676))]]]]], (7578 ^ _51060) ^ [_205732, _205734, _205736, _205738] : [function(_205732), quasi_total(_205732, _205738, _205736), relation_of2_as_subset(_205732, _205738, _205736), 7589 ^ _51060 : [(7590 ^ _51060) ^ [_206101] : [relation(_206101), function(_206101), in(_205734, _205738), -(_205736 = empty_set), -(apply(relation_composition(_205732, _206101), _205734) = apply(_206101, apply(_205732, _205734)))]]], (7608 ^ _51060) ^ [_206658] : [epsilon_transitive(_206658), 7611 ^ _51060 : [(7612 ^ _51060) ^ [_206794] : [ordinal(_206794), proper_subset(_206658, _206794), -(in(_206658, _206794))]]], (7622 ^ _51060) ^ [_207084] : [relation(_207084), -(subset(_207084, cartesian_product2(relation_dom(_207084), relation_rng(_207084))))], (7628 ^ _51060) ^ [_207314, _207316, _207318] : [relation(_207314), -(subset(fiber(relation_restriction(_207314, _207318), _207316), fiber(_207314, _207316)))], (7634 ^ _51060) ^ [_207546, _207548] : [relation(_207546), function(_207546), 7641 ^ _51060 : [(7642 ^ _51060) ^ [_207795] : [relation(_207795), function(_207795), in(_207548, relation_dom(relation_composition(_207795, _207546))), -(apply(relation_composition(_207795, _207546), _207548) = apply(_207546, apply(_207795, _207548)))]]], (7656 ^ _51060) ^ [_208254, _208256, _208258] : [relation_of2_as_subset(_208254, _208256, _208258), 7659 ^ _51060 : [(7660 ^ _51060) ^ [] : [7662 ^ _51060 : [(7663 ^ _51060) ^ [] : [-(in(7661 ^ [_208254, _208256, _208258], _208256))], (7665 ^ _51060) ^ [_208612] : [in(ordered_pair(7661 ^ [_208254, _208256, _208258], _208612), _208254)]], -(relation_dom_as_subset(_208256, _208258, _208254) = _208256)], (7669 ^ _51060) ^ [] : [relation_dom_as_subset(_208256, _208258, _208254) = _208256, 7672 ^ _51060 : [(7673 ^ _51060) ^ [_208849] : [in(_208849, _208256), -(in(ordered_pair(_208849, 7676 ^ [_208254, _208256, _208258, _208849]), _208254))]]]]], (7680 ^ _51060) ^ [_209171, _209173] : [relation(_209171), reflexive(_209171), -(reflexive(relation_restriction(_209171, _209173)))], (7690 ^ _51060) ^ [_209470, _209472] : [relation(_209470), function(_209470), 7697 ^ _51060 : [(7698 ^ _51060) ^ [_209716] : [relation(_209716), function(_209716), in(_209472, relation_dom(_209470)), -(apply(relation_composition(_209470, _209716), _209472) = apply(_209716, apply(_209470, _209472)))]]], (7712 ^ _51060) ^ [_210141] : [7727 ^ _51060 : [(7728 ^ _51060) ^ [_210544] : [element(_210544, the_carrier(_210141)), 7731 ^ _51060 : [(7732 ^ _51060) ^ [_210694] : [element(_210694, the_carrier(_210141)), -(below(_210141, meet_commut(_210141, _210544, _210694), _210544))]]]], -(empty_carrier(_210141)), meet_commutative(_210141), meet_absorbing(_210141), latt_str(_210141)], (7738 ^ _51060) ^ [_210938, _210940] : [ordinal(_210938), in(_210940, _210938), -(ordinal(_210940))], (7748 ^ _51060) ^ [_211247, _211249, _211251] : [relation_of2_as_subset(_211247, _211251, _211249), 7751 ^ _51060 : [(7752 ^ _51060) ^ [] : [7754 ^ _51060 : [(7755 ^ _51060) ^ [] : [-(in(7753 ^ [_211247, _211249, _211251], _211249))], (7757 ^ _51060) ^ [_211605] : [in(ordered_pair(_211605, 7753 ^ [_211247, _211249, _211251]), _211247)]], -(relation_rng_as_subset(_211251, _211249, _211247) = _211249)], (7761 ^ _51060) ^ [] : [relation_rng_as_subset(_211251, _211249, _211247) = _211249, 7764 ^ _51060 : [(7765 ^ _51060) ^ [_211842] : [in(_211842, _211249), -(in(ordered_pair(7768 ^ [_211247, _211249, _211251, _211842], _211842), _211247))]]]]], (7772 ^ _51060) ^ [_212164, _212166] : [relation(_212164), connected(_212164), -(connected(relation_restriction(_212164, _212166)))], (7782 ^ _51060) ^ [_212449] : [ordinal(_212449), 7785 ^ _51060 : [(7786 ^ _51060) ^ [_212599] : [ordinal(_212599), -(in(_212449, _212599)), -(_212449 = _212599), -(in(_212599, _212449))]]], (7800 ^ _51060) ^ [_213002, _213004] : [relation(_213002), transitive(_213002), -(transitive(relation_restriction(_213002, _213004)))], (7810 ^ _51060) ^ [_213287] : [relation(_213287), 7813 ^ _51060 : [(7814 ^ _51060) ^ [_213437] : [relation(_213437), subset(_213287, _213437), 7821 ^ _51060 : [(7822 ^ _51060) ^ [] : [-(subset(relation_dom(_213287), relation_dom(_213437)))], (7824 ^ _51060) ^ [] : [-(subset(relation_rng(_213287), relation_rng(_213437)))]]]]], (7826 ^ _51060) ^ [_213832, _213834] : [relation(_213832), antisymmetric(_213832), -(antisymmetric(relation_restriction(_213832, _213834)))], (7836 ^ _51060) ^ [_214131, _214133] : [relation(_214131), well_orders(_214131, _214133), 7843 ^ _51060 : [(7844 ^ _51060) ^ [] : [-(relation_field(relation_restriction(_214131, _214133)) = _214133)], (7846 ^ _51060) ^ [] : [-(well_ordering(relation_restriction(_214131, _214133)))]]], (7848 ^ _51060) ^ [_214503] : [relation(_214503), function(_214503), finite(relation_dom(_214503)), -(finite(relation_rng(_214503)))], (7862 ^ _51060) ^ [_214865] : [-(empty_carrier(_214865)), join_commutative(_214865), join_semilatt_str(_214865), 7873 ^ _51060 : [(7874 ^ _51060) ^ [_215194] : [element(_215194, the_carrier(_214865)), 7877 ^ _51060 : [(7878 ^ _51060) ^ [_215353] : [element(_215353, the_carrier(_214865)), -(_215194 = _215353), below(_214865, _215194, _215353), below(_214865, _215353, _215194)]]]]], (7893 ^ _51060) ^ [_215816] : [-(relation(7891 ^ [_215816]))], (7895 ^ _51060) ^ [_215864] : [-(well_orders(7891 ^ [_215864], _215864))], (7897 ^ _51060) ^ [_215992, _215994, _215996] : [subset(_215996, _215994), -(subset(set_intersection2(_215996, _215992), set_intersection2(_215994, _215992)))], (7903 ^ _51060) ^ [_216206] : [-(empty(_216206)), 7909 ^ _51060 : [(7910 ^ _51060) ^ [] : [-(in(7908 ^ [_216206], _216206))], (7912 ^ _51060) ^ [] : [-(7908 ^ [_216206] = empty_set)]], 7914 ^ _51060 : [(7915 ^ _51060) ^ [] : [-(relation(7913 ^ [_216206]))], (7917 ^ _51060) ^ [] : [-(function(7913 ^ [_216206]))], (7919 ^ _51060) ^ [] : [-(relation_dom(7913 ^ [_216206]) = _216206)], (7921 ^ _51060) ^ [_216874] : [in(_216874, _216206), -(in(apply(7913 ^ [_216206], _216874), _216874))]]], (7927 ^ _51060) ^ [_217118, _217120] : [subset(_217120, _217118), -(set_intersection2(_217120, _217118) = _217120)], (7933 ^ _51060) ^ [_217305] : [-(set_intersection2(_217305, empty_set) = empty_set)], (7935 ^ _51060) ^ [_217415, _217417] : [element(_217417, _217415), -(empty(_217415)), -(in(_217417, _217415))], (7945 ^ _51060) ^ [_217713, _217715] : [-(_217715 = _217713), 7949 ^ _51060 : [(7950 ^ _51060) ^ [] : [-(in(7946 ^ [_217713, _217715], _217715))], (7952 ^ _51060) ^ [] : [in(7946 ^ [_217713, _217715], _217713)]], 7953 ^ _51060 : [(7954 ^ _51060) ^ [] : [-(in(7946 ^ [_217713, _217715], _217713))], (7956 ^ _51060) ^ [] : [in(7946 ^ [_217713, _217715], _217715)]]], (7960 ^ _51060) ^ [_218214] : [-(reflexive(inclusion_relation(_218214)))], (7962 ^ _51060) ^ [_218293] : [-(subset(empty_set, _218293))], (7964 ^ _51060) ^ [_218414, _218416, _218418] : [relation(_218414), in(ordered_pair(_218418, _218416), _218414), 7971 ^ _51060 : [(7972 ^ _51060) ^ [] : [-(in(_218418, relation_field(_218414)))], (7974 ^ _51060) ^ [] : [-(in(_218416, relation_field(_218414)))]]], (7976 ^ _51060) ^ [_218798] : [-(ordinal(_218798)), 7978 ^ _51060 : [(7979 ^ _51060) ^ [] : [-(in(7977 ^ [_218798], _218798))], (7981 ^ _51060) ^ [] : [ordinal(7977 ^ [_218798]), subset(7977 ^ [_218798], _218798)]]], (7989 ^ _51060) ^ [_219228, _219230] : [relation(_219228), well_founded_relation(_219228), -(well_founded_relation(relation_restriction(_219228, _219230)))], (7999 ^ _51060) ^ [_219527, _219529] : [ordinal(_219527), subset(_219529, _219527), -(_219529 = empty_set), 8011 ^ _51060 : [(8012 ^ _51060) ^ [] : [-(ordinal(8010 ^ [_219527, _219529]))], (8014 ^ _51060) ^ [] : [-(in(8010 ^ [_219527, _219529], _219529))], (8016 ^ _51060) ^ [_220079] : [ordinal(_220079), in(_220079, _219529), -(ordinal_subset(8010 ^ [_219527, _219529], _220079))]]], (8026 ^ _51060) ^ [_220421, _220423] : [relation(_220421), well_ordering(_220421), -(well_ordering(relation_restriction(_220421, _220423)))], (8036 ^ _51060) ^ [_220706] : [ordinal(_220706), 8039 ^ _51060 : [(8040 ^ _51060) ^ [_220844] : [ordinal(_220844), 8043 ^ _51060 : [(8044 ^ _51060) ^ [] : [in(_220706, _220844), -(ordinal_subset(succ(_220706), _220844))], (8050 ^ _51060) ^ [] : [ordinal_subset(succ(_220706), _220844), -(in(_220706, _220844))]]]]], (8056 ^ _51060) ^ [_221329, _221331, _221333] : [subset(_221333, _221331), -(subset(set_difference(_221333, _221329), set_difference(_221331, _221329)))], (8062 ^ _51060) ^ [_221585, _221587, _221589, _221591] : [ordered_pair(_221591, _221589) = ordered_pair(_221587, _221585), 8065 ^ _51060 : [(8066 ^ _51060) ^ [] : [-(_221591 = _221587)], (8068 ^ _51060) ^ [] : [-(_221589 = _221585)]]], (8070 ^ _51060) ^ [_221898, _221900] : [relation(_221898), function(_221898), 8077 ^ _51060 : [(8078 ^ _51060) ^ [] : [_221898 = identity_relation(_221900), 8081 ^ _51060 : [(8082 ^ _51060) ^ [] : [-(relation_dom(_221898) = _221900)], (8084 ^ _51060) ^ [_222317] : [in(_222317, _221900), -(apply(_221898, _222317) = _222317)]]], (8090 ^ _51060) ^ [] : [-(_221898 = identity_relation(_221900)), relation_dom(_221898) = _221900, 8096 ^ _51060 : [(8097 ^ _51060) ^ [] : [-(in(8095 ^ [_221898, _221900], _221900))], (8099 ^ _51060) ^ [] : [apply(_221898, 8095 ^ [_221898, _221900]) = 8095 ^ [_221898, _221900]]]]]], (8103 ^ _51060) ^ [_222922, _222924] : [in(_222922, _222924), -(apply(identity_relation(_222924), _222922) = _222922)], (8109 ^ _51060) ^ [_223127, _223129] : [-(subset(set_difference(_223129, _223127), _223129))], (8111 ^ _51060) ^ [_223225] : [relation(_223225), 8114 ^ _51060 : [(8115 ^ _51060) ^ [] : [-(relation_rng(_223225) = relation_dom(relation_inverse(_223225)))], (8117 ^ _51060) ^ [] : [-(relation_dom(_223225) = relation_rng(relation_inverse(_223225)))]]], (8119 ^ _51060) ^ [_223553, _223555] : [set_difference(_223555, _223553) = empty_set, -(subset(_223555, _223553))], (8125 ^ _51060) ^ [_223721, _223723] : [subset(_223723, _223721), -(set_difference(_223723, _223721) = empty_set)], (8131 ^ _51060) ^ [_223968, _223970] : [subset(singleton(_223970), _223968), -(in(_223970, _223968))], (8137 ^ _51060) ^ [_224134, _224136] : [in(_224136, _224134), -(subset(singleton(_224136), _224134))], (8143 ^ _51060) ^ [_224393, _224395, _224397] : [subset(unordered_pair(_224397, _224395), _224393), 8146 ^ _51060 : [(8147 ^ _51060) ^ [] : [-(in(_224397, _224393))], (8149 ^ _51060) ^ [] : [-(in(_224395, _224393))]]], (8151 ^ _51060) ^ [_224644, _224646, _224648] : [-(subset(unordered_pair(_224648, _224646), _224644)), in(_224648, _224644), in(_224646, _224644)], (8161 ^ _51060) ^ [_224961, _224963] : [relation(_224961), -(relation_field(relation_restriction(_224961, _224963)) = _224963), well_ordering(_224961), subset(_224963, relation_field(_224961))], (8175 ^ _51060) ^ [_225344, _225346] : [-(set_union2(_225346, set_difference(_225344, _225346)) = set_union2(_225346, _225344))], (8187 ^ _51060) ^ [_225751, _225753] : [8188 ^ _51060 : [(8189 ^ _51060) ^ [] : [_225753 = empty_set], (8191 ^ _51060) ^ [] : [_225753 = singleton(_225751)]], -(subset(_225753, singleton(_225751)))], (8177 ^ _51060) ^ [_225491, _225493] : [subset(_225493, singleton(_225491)), -(_225493 = empty_set), -(_225493 = singleton(_225491))], (8195 ^ _51060) ^ [_226016] : [-(set_difference(_226016, empty_set) = _226016)], (8197 ^ _51060) ^ [_226140, _226142, _226144] : [in(_226144, _226142), in(_226142, _226140), in(_226140, _226144)], (8207 ^ _51060) ^ [_226477, _226479] : [element(_226479, powerset(_226477)), -(subset(_226479, _226477))], (8213 ^ _51060) ^ [_226643, _226645] : [subset(_226645, _226643), -(element(_226645, powerset(_226643)))], (8219 ^ _51060) ^ [_226830] : [-(transitive(inclusion_relation(_226830)))], (8221 ^ _51060) ^ [_226958, _226960] : [-(disjoint(_226960, _226958)), 8225 ^ _51060 : [(8226 ^ _51060) ^ [] : [-(in(8224 ^ [_226958, _226960], _226960))], (8228 ^ _51060) ^ [] : [-(in(8224 ^ [_226958, _226960], _226958))]]], (8230 ^ _51060) ^ [_227272, _227274] : [disjoint(_227274, _227272), 8231 ^ _51060 : [(8232 ^ _51060) ^ [_227364] : [in(_227364, _227274), in(_227364, _227272)]]], (8240 ^ _51060) ^ [_227621] : [subset(_227621, empty_set), -(_227621 = empty_set)], (8246 ^ _51060) ^ [_227810, _227812] : [-(set_difference(set_union2(_227812, _227810), _227810) = set_difference(_227812, _227810))], (8248 ^ _51060) ^ [_227914] : [ordinal(_227914), 8251 ^ _51060 : [(8266 ^ _51060) ^ [] : [8268 ^ _51060 : [(8269 ^ _51060) ^ [] : [-(ordinal(8267 ^ [_227914]))], (8271 ^ _51060) ^ [] : [-(in(8267 ^ [_227914], _227914))], (8273 ^ _51060) ^ [] : [in(succ(8267 ^ [_227914]), _227914)]], -(being_limit_ordinal(_227914))], (8252 ^ _51060) ^ [] : [being_limit_ordinal(_227914), 8255 ^ _51060 : [(8256 ^ _51060) ^ [_228160] : [ordinal(_228160), in(_228160, _227914), -(in(succ(_228160), _227914))]]]]], (8277 ^ _51060) ^ [_228786] : [ordinal(_228786), 8280 ^ _51060 : [(8281 ^ _51060) ^ [] : [-(being_limit_ordinal(_228786)), 8285 ^ _51060 : [(8286 ^ _51060) ^ [] : [-(ordinal(8284 ^ [_228786]))], (8288 ^ _51060) ^ [] : [-(_228786 = succ(8284 ^ [_228786]))]]], (8290 ^ _51060) ^ [] : [being_limit_ordinal(_228786), 8291 ^ _51060 : [(8292 ^ _51060) ^ [_229257] : [ordinal(_229257), _228786 = succ(_229257)]]]]], (8300 ^ _51060) ^ [_229524, _229526] : [element(_229524, powerset(_229526)), 8303 ^ _51060 : [(8304 ^ _51060) ^ [_229676] : [element(_229676, powerset(_229526)), 8307 ^ _51060 : [(8308 ^ _51060) ^ [] : [disjoint(_229524, _229676), -(subset(_229524, subset_complement(_229526, _229676)))], (8314 ^ _51060) ^ [] : [subset(_229524, subset_complement(_229526, _229676)), -(disjoint(_229524, _229676))]]]]], (8320 ^ _51060) ^ [_230160] : [relation(_230160), 8323 ^ _51060 : [(8324 ^ _51060) ^ [_230297] : [relation(_230297), -(subset(relation_dom(relation_composition(_230160, _230297)), relation_dom(_230160)))]]], (8330 ^ _51060) ^ [_230512] : [relation(_230512), 8333 ^ _51060 : [(8334 ^ _51060) ^ [_230649] : [relation(_230649), -(subset(relation_rng(relation_composition(_230512, _230649)), relation_rng(_230649)))]]], (8340 ^ _51060) ^ [_230878, _230880] : [subset(_230880, _230878), -(_230878 = set_union2(_230880, set_difference(_230878, _230880)))], (8346 ^ _51060) ^ [_231128, _231130, _231132, _231134] : [function(_231128), quasi_total(_231128, _231134, _231132), relation_of2_as_subset(_231128, _231134, _231132), -(_231132 = empty_set), 8361 ^ _51060 : [(8362 ^ _51060) ^ [_231606] : [in(_231606, relation_inverse_image(_231128, _231130)), 8365 ^ _51060 : [(8366 ^ _51060) ^ [] : [-(in(_231606, _231134))], (8368 ^ _51060) ^ [] : [-(in(apply(_231128, _231606), _231130))]]], (8370 ^ _51060) ^ [_231887] : [-(in(_231887, relation_inverse_image(_231128, _231130))), in(_231887, _231134), in(apply(_231128, _231887), _231130)]]], (8380 ^ _51060) ^ [_232237] : [relation(_232237), 8383 ^ _51060 : [(8384 ^ _51060) ^ [_232384] : [relation(_232384), subset(relation_rng(_232237), relation_dom(_232384)), -(relation_dom(relation_composition(_232237, _232384)) = relation_dom(_232237))]]], (8394 ^ _51060) ^ [_232710, _232712] : [element(_232710, powerset(powerset(_232712))), -(_232710 = empty_set), complements_of_subsets(_232712, _232710) = empty_set], (8404 ^ _51060) ^ [_233027, _233029] : [in(_233029, _233027), -(set_union2(singleton(_233029), _233027) = _233027)], (8410 ^ _51060) ^ [_233233] : [relation(_233233), 8413 ^ _51060 : [(8414 ^ _51060) ^ [_233380] : [relation(_233380), subset(relation_dom(_233233), relation_rng(_233380)), -(relation_rng(relation_composition(_233380, _233233)) = relation_rng(_233233))]]], (8424 ^ _51060) ^ [_233706, _233708] : [element(_233706, powerset(powerset(_233708))), -(_233706 = empty_set), -(subset_difference(_233708, cast_to_subset(_233708), union_of_subsets(_233708, _233706)) = meet_of_subsets(_233708, complements_of_subsets(_233708, _233706)))], (8434 ^ _51060) ^ [_234046, _234048] : [element(_234046, powerset(powerset(_234048))), -(_234046 = empty_set), -(union_of_subsets(_234048, complements_of_subsets(_234048, _234046)) = subset_difference(_234048, cast_to_subset(_234048), meet_of_subsets(_234048, _234046)))], (8444 ^ _51060) ^ [_234371, _234373] : [-(set_difference(_234373, set_difference(_234373, _234371)) = set_intersection2(_234373, _234371))], (8446 ^ _51060) ^ [_234475] : [relation(_234475), 8449 ^ _51060 : [(8450 ^ _51060) ^ [_234630] : [relation(_234630), 8453 ^ _51060 : [(8454 ^ _51060) ^ [_234781] : [relation(_234781), function(_234781), relation_isomorphism(_234475, _234630, _234781), -(relation_isomorphism(_234630, _234475, function_inverse(_234781)))]]]]], (8468 ^ _51060) ^ [_235174] : [-(set_difference(empty_set, _235174) = empty_set)], (8470 ^ _51060) ^ [_235298, _235300, _235302] : [-(element(_235302, _235298)), in(_235302, _235300), element(_235300, powerset(_235298))], (8480 ^ _51060) ^ [_235597] : [ordinal(_235597), -(connected(inclusion_relation(_235597)))], (8486 ^ _51060) ^ [_235821, _235823] : [-(disjoint(_235823, _235821)), -(in(8489 ^ [_235821, _235823], set_intersection2(_235823, _235821)))], (8493 ^ _51060) ^ [_236056, _236058] : [8494 ^ _51060 : [(8495 ^ _51060) ^ [_236129] : [in(_236129, set_intersection2(_236058, _236056))]], disjoint(_236058, _236056)], (8499 ^ _51060) ^ [_236281] : [-(_236281 = empty_set), 8502 ^ _51060 : [(8503 ^ _51060) ^ [_236441] : [element(_236441, powerset(_236281)), 8506 ^ _51060 : [(8507 ^ _51060) ^ [_236595] : [element(_236595, _236281), -(in(_236595, _236441)), -(in(_236595, subset_complement(_236281, _236441)))]]]]], (8517 ^ _51060) ^ [_236913] : [relation(_236913), 8520 ^ _51060 : [(8521 ^ _51060) ^ [_237109] : [relation(_237109), 8524 ^ _51060 : [(8525 ^ _51060) ^ [_237301] : [relation(_237301), function(_237301), relation_isomorphism(_236913, _237109, _237301), 8536 ^ _51060 : [(8537 ^ _51060) ^ [] : [reflexive(_236913), -(reflexive(_237109))], (8543 ^ _51060) ^ [] : [transitive(_236913), -(transitive(_237109))], (8549 ^ _51060) ^ [] : [connected(_236913), -(connected(_237109))], (8555 ^ _51060) ^ [] : [antisymmetric(_236913), -(antisymmetric(_237109))], (8561 ^ _51060) ^ [] : [well_founded_relation(_236913), -(well_founded_relation(_237109))]]]]]]], (8567 ^ _51060) ^ [_238453] : [relation(_238453), function(_238453), one_to_one(_238453), 8578 ^ _51060 : [(8579 ^ _51060) ^ [_238840] : [relation(_238840), function(_238840), 8586 ^ _51060 : [(8617 ^ _51060) ^ [] : [-(_238840 = function_inverse(_238453)), relation_dom(_238840) = relation_rng(_238453), 8626 ^ _51060 : [(8627 ^ _51060) ^ [] : [-(in(8622 ^ [_238453, _238840], relation_rng(_238453)))], (8629 ^ _51060) ^ [] : [-(8623 ^ [_238453, _238840] = apply(_238840, 8622 ^ [_238453, _238840]))], (8631 ^ _51060) ^ [] : [in(8623 ^ [_238453, _238840], relation_dom(_238453)), 8622 ^ [_238453, _238840] = apply(_238453, 8623 ^ [_238453, _238840])]], 8636 ^ _51060 : [(8637 ^ _51060) ^ [] : [-(in(8623 ^ [_238453, _238840], relation_dom(_238453)))], (8639 ^ _51060) ^ [] : [-(8622 ^ [_238453, _238840] = apply(_238453, 8623 ^ [_238453, _238840]))], (8641 ^ _51060) ^ [] : [in(8622 ^ [_238453, _238840], relation_rng(_238453)), 8623 ^ [_238453, _238840] = apply(_238840, 8622 ^ [_238453, _238840])]]], (8587 ^ _51060) ^ [] : [_238840 = function_inverse(_238453), 8590 ^ _51060 : [(8591 ^ _51060) ^ [] : [-(relation_dom(_238840) = relation_rng(_238453))], (8593 ^ _51060) ^ [_239357, _239359] : [8600 ^ _51060 : [(8601 ^ _51060) ^ [] : [-(in(_239357, relation_dom(_238453)))], (8603 ^ _51060) ^ [] : [-(_239359 = apply(_238453, _239357))]], in(_239359, relation_rng(_238453)), _239357 = apply(_238840, _239359)], (8605 ^ _51060) ^ [_239731, _239733] : [8612 ^ _51060 : [(8613 ^ _51060) ^ [] : [-(in(_239733, relation_rng(_238453)))], (8615 ^ _51060) ^ [] : [-(_239731 = apply(_238840, _239733))]], in(_239731, relation_dom(_238453)), _239733 = apply(_238453, _239731)]]]]]]], (8649 ^ _51060) ^ [_241306, _241308, _241310] : [element(_241306, powerset(_241310)), in(_241308, subset_complement(_241310, _241306)), in(_241308, _241306)], (8659 ^ _51060) ^ [_241612] : [relation(_241612), 8662 ^ _51060 : [(8663 ^ _51060) ^ [_241768] : [relation(_241768), 8666 ^ _51060 : [(8667 ^ _51060) ^ [_241920] : [relation(_241920), function(_241920), -(well_ordering(_241768)), well_ordering(_241612), relation_isomorphism(_241612, _241768, _241920)]]]]], (8685 ^ _51060) ^ [_242411] : [relation(_242411), function(_242411), one_to_one(_242411), 8696 ^ _51060 : [(8697 ^ _51060) ^ [] : [-(relation_rng(_242411) = relation_dom(function_inverse(_242411)))], (8699 ^ _51060) ^ [] : [-(relation_dom(_242411) = relation_rng(function_inverse(_242411)))]]], (8701 ^ _51060) ^ [_242864] : [relation(_242864), -(in(ordered_pair(8706 ^ [_242864], 8707 ^ [_242864]), _242864)), -(_242864 = empty_set)], (8713 ^ _51060) ^ [_243282, _243284] : [relation(_243282), function(_243282), 8728 ^ _51060 : [(8729 ^ _51060) ^ [] : [-(_243284 = apply(_243282, apply(function_inverse(_243282), _243284)))], (8731 ^ _51060) ^ [] : [-(_243284 = apply(relation_composition(function_inverse(_243282), _243282), _243284))]], one_to_one(_243282), in(_243284, relation_rng(_243282))], (8733 ^ _51060) ^ [_243880, _243882, _243884] : [in(_243884, _243882), element(_243882, powerset(_243880)), empty(_243880)], (8743 ^ _51060) ^ [_244176] : [relation(_244176), 8746 ^ _51060 : [(8747 ^ _51060) ^ [] : [well_founded_relation(_244176), -(is_well_founded_in(_244176, relation_field(_244176)))], (8753 ^ _51060) ^ [] : [is_well_founded_in(_244176, relation_field(_244176)), -(well_founded_relation(_244176))]]], (8759 ^ _51060) ^ [_244592] : [-(antisymmetric(inclusion_relation(_244592)))], (8761 ^ _51060) ^ [] : [-(relation_dom(empty_set) = empty_set)], (8763 ^ _51060) ^ [] : [-(relation_rng(empty_set) = empty_set)], (8765 ^ _51060) ^ [_244808, _244810] : [subset(_244810, _244808), proper_subset(_244808, _244810)], (8771 ^ _51060) ^ [_245003] : [relation(_245003), function(_245003), one_to_one(_245003), -(one_to_one(function_inverse(_245003)))], (8785 ^ _51060) ^ [_245389, _245391, _245393] : [-(disjoint(_245393, _245389)), subset(_245393, _245391), disjoint(_245391, _245389)], (8795 ^ _51060) ^ [_245684] : [relation(_245684), 8800 ^ _51060 : [(8801 ^ _51060) ^ [] : [relation_dom(_245684) = empty_set], (8803 ^ _51060) ^ [] : [relation_rng(_245684) = empty_set]], -(_245684 = empty_set)], (8807 ^ _51060) ^ [_246037] : [relation(_246037), 8810 ^ _51060 : [(8811 ^ _51060) ^ [] : [relation_dom(_246037) = empty_set, -(relation_rng(_246037) = empty_set)], (8817 ^ _51060) ^ [] : [relation_rng(_246037) = empty_set, -(relation_dom(_246037) = empty_set)]]], (8823 ^ _51060) ^ [_246520, _246522] : [set_difference(_246522, singleton(_246520)) = _246522, in(_246520, _246522)], (8829 ^ _51060) ^ [_246693, _246695] : [-(in(_246693, _246695)), -(set_difference(_246695, singleton(_246693)) = _246695)], (8835 ^ _51060) ^ [_246918, _246920] : [relation(_246918), function(_246918), 8842 ^ _51060 : [(8843 ^ _51060) ^ [_247185] : [relation(_247185), function(_247185), 8850 ^ _51060 : [(8851 ^ _51060) ^ [] : [_246918 = relation_dom_restriction(_247185, _246920), 8854 ^ _51060 : [(8855 ^ _51060) ^ [] : [-(relation_dom(_246918) = set_intersection2(relation_dom(_247185), _246920))], (8857 ^ _51060) ^ [_247639] : [in(_247639, relation_dom(_246918)), -(apply(_246918, _247639) = apply(_247185, _247639))]]], (8863 ^ _51060) ^ [] : [-(_246918 = relation_dom_restriction(_247185, _246920)), relation_dom(_246918) = set_intersection2(relation_dom(_247185), _246920), 8869 ^ _51060 : [(8870 ^ _51060) ^ [] : [-(in(8868 ^ [_246918, _246920, _247185], relation_dom(_246918)))], (8872 ^ _51060) ^ [] : [apply(_246918, 8868 ^ [_246918, _246920, _247185]) = apply(_247185, 8868 ^ [_246918, _246920, _247185])]]]]]]], (8876 ^ _51060) ^ [_248278] : [-(unordered_pair(_248278, _248278) = singleton(_248278))], (8878 ^ _51060) ^ [_248376] : [empty(_248376), -(_248376 = empty_set)], (8884 ^ _51060) ^ [_248606, _248608, _248610, _248612] : [function(_248606), quasi_total(_248606, _248612, _248610), relation_of2_as_subset(_248606, _248612, _248610), in(_248608, _248612), -(_248610 = empty_set), -(in(apply(_248606, _248608), relation_rng(_248606)))], (8906 ^ _51060) ^ [_249219] : [ordinal(_249219), -(well_founded_relation(inclusion_relation(_249219)))], (8912 ^ _51060) ^ [_249423, _249425] : [subset(singleton(_249425), singleton(_249423)), -(_249425 = _249423)], (8918 ^ _51060) ^ [_249655, _249657, _249659] : [relation(_249655), function(_249655), in(_249657, relation_dom(relation_dom_restriction(_249655, _249659))), -(apply(relation_dom_restriction(_249655, _249659), _249657) = apply(_249655, _249657))], (8932 ^ _51060) ^ [_250074] : [-(relation_dom(identity_relation(_250074)) = _250074)], (8934 ^ _51060) ^ [_250122] : [-(relation_rng(identity_relation(_250122)) = _250122)], (8936 ^ _51060) ^ [_250249, _250251, _250253] : [relation(_250249), function(_250249), in(_250251, _250253), -(apply(relation_dom_restriction(_250249, _250253), _250251) = apply(_250249, _250251))], (8950 ^ _51060) ^ [_250695, _250697, _250699, _250701] : [relation(_250695), 8953 ^ _51060 : [(8954 ^ _51060) ^ [] : [in(ordered_pair(_250701, _250699), relation_composition(identity_relation(_250697), _250695)), 8957 ^ _51060 : [(8958 ^ _51060) ^ [] : [-(in(_250701, _250697))], (8960 ^ _51060) ^ [] : [-(in(ordered_pair(_250701, _250699), _250695))]]], (8962 ^ _51060) ^ [] : [-(in(ordered_pair(_250701, _250699), relation_composition(identity_relation(_250697), _250695))), in(_250701, _250697), in(ordered_pair(_250701, _250699), _250695)]]], (8972 ^ _51060) ^ [_251388, _251390] : [in(_251390, _251388), empty(_251388)], (8978 ^ _51060) ^ [_251600, _251602] : [-(pair_first(ordered_pair(_251602, _251600)) = _251602)], (8980 ^ _51060) ^ [_251651, _251653] : [-(pair_second(ordered_pair(_251653, _251651)) = _251651)], (8982 ^ _51060) ^ [_251767, _251769] : [in(_251769, _251767), 8986 ^ _51060 : [(8987 ^ _51060) ^ [] : [-(in(8985 ^ [_251767, _251769], _251767))], (8989 ^ _51060) ^ [_252058] : [in(_252058, _251767), in(_252058, 8985 ^ [_251767, _251769])]]], (8995 ^ _51060) ^ [_252284] : [ordinal(_252284), -(well_ordering(inclusion_relation(_252284)))], (9001 ^ _51060) ^ [_252473, _252475] : [-(subset(_252475, set_union2(_252475, _252473)))], (9003 ^ _51060) ^ [_252614, _252616] : [disjoint(_252616, _252614), -(set_difference(_252616, _252614) = _252616)], (9009 ^ _51060) ^ [_252782, _252784] : [set_difference(_252784, _252782) = _252784, -(disjoint(_252784, _252782))], (9015 ^ _51060) ^ [_253014, _253016, _253018] : [relation(_253014), 9018 ^ _51060 : [(9019 ^ _51060) ^ [] : [in(_253018, relation_dom(relation_dom_restriction(_253014, _253016))), 9022 ^ _51060 : [(9023 ^ _51060) ^ [] : [-(in(_253018, _253016))], (9025 ^ _51060) ^ [] : [-(in(_253018, relation_dom(_253014)))]]], (9027 ^ _51060) ^ [] : [-(in(_253018, relation_dom(relation_dom_restriction(_253014, _253016)))), in(_253018, _253016), in(_253018, relation_dom(_253014))]]], (9037 ^ _51060) ^ [_253673, _253675] : [relation(_253673), -(subset(relation_dom_restriction(_253673, _253675), _253673))], (9043 ^ _51060) ^ [_253887, _253889] : [empty(_253889), -(_253889 = _253887), empty(_253887)], (9053 ^ _51060) ^ [_254198, _254200, _254202] : [relation(_254198), function(_254198), 9060 ^ _51060 : [(9061 ^ _51060) ^ [] : [in(ordered_pair(_254202, _254200), _254198), 9064 ^ _51060 : [(9065 ^ _51060) ^ [] : [-(in(_254202, relation_dom(_254198)))], (9067 ^ _51060) ^ [] : [-(_254200 = apply(_254198, _254202))]]], (9069 ^ _51060) ^ [] : [-(in(ordered_pair(_254202, _254200), _254198)), in(_254202, relation_dom(_254198)), _254200 = apply(_254198, _254202)]]], (9079 ^ _51060) ^ [_254939] : [relation(_254939), 9082 ^ _51060 : [(9083 ^ _51060) ^ [] : [well_orders(_254939, relation_field(_254939)), -(well_ordering(_254939))], (9089 ^ _51060) ^ [] : [well_ordering(_254939), -(well_orders(_254939, relation_field(_254939)))]]], (9095 ^ _51060) ^ [_255398, _255400, _255402] : [-(subset(set_union2(_255402, _255398), _255400)), subset(_255402, _255400), subset(_255398, _255400)], (9105 ^ _51060) ^ [_255727, _255729, _255731] : [singleton(_255731) = unordered_pair(_255729, _255727), -(_255731 = _255729)], (9111 ^ _51060) ^ [_255953, _255955] : [relation(_255953), -(relation_dom(relation_dom_restriction(_255953, _255955)) = set_intersection2(relation_dom(_255953), _255955))], (9117 ^ _51060) ^ [_256181, _256183] : [in(_256183, _256181), -(subset(_256183, union(_256181)))], (9123 ^ _51060) ^ [_256395, _256397] : [relation(_256395), -(relation_dom_restriction(_256395, _256397) = relation_composition(identity_relation(_256397), _256395))], (9129 ^ _51060) ^ [_256619, _256621] : [relation(_256619), -(subset(relation_rng(relation_dom_restriction(_256619, _256621)), relation_rng(_256619)))], (9135 ^ _51060) ^ [_256812] : [-(union(powerset(_256812)) = _256812)], (9137 ^ _51060) ^ [_256951, _256953, _256955, _256957] : [function(_256951), quasi_total(_256951, _256957, _256955), relation_of2_as_subset(_256951, _256957, _256955), subset(_256955, _256953), 9154 ^ _51060 : [(9155 ^ _51060) ^ [] : [-(_256955 = empty_set)], (9157 ^ _51060) ^ [] : [_256957 = empty_set]], 9158 ^ _51060 : [(9159 ^ _51060) ^ [] : [-(function(_256951))], (9161 ^ _51060) ^ [] : [-(quasi_total(_256951, _256957, _256953))], (9163 ^ _51060) ^ [] : [-(relation_of2_as_subset(_256951, _256957, _256953))]]], (9201 ^ _51060) ^ [_259217, _259219, _259221] : [singleton(_259221) = unordered_pair(_259219, _259217), -(_259219 = _259217)], (9166 ^ _51060) ^ [_257937] : [-(in(_257937, 9164 ^ [_257937]))], (9168 ^ _51060) ^ [_258049, _258051, _258053] : [-(in(_258049, 9164 ^ [_258053])), in(_258051, 9164 ^ [_258053]), subset(_258049, _258051)], (9178 ^ _51060) ^ [_258364, _258366] : [in(_258364, 9164 ^ [_258366]), 9182 ^ _51060 : [(9183 ^ _51060) ^ [] : [-(in(9181 ^ [_258364, _258366], 9164 ^ [_258366]))], (9185 ^ _51060) ^ [_258676] : [subset(_258676, _258364), -(in(_258676, 9181 ^ [_258364, _258366]))]]], (9191 ^ _51060) ^ [_258883, _258885] : [subset(_258883, 9164 ^ [_258885]), -(are_equipotent(_258883, 9164 ^ [_258885])), -(in(_258883, 9164 ^ [_258885]))]], input).
% 0.47/1.37  ncf('1',plain,[cast_as_carrier_subset(9206 ^ []) = the_carrier(9206 ^ [])],start(9210 ^ 0)).
% 0.47/1.37  ncf('1.1',plain,[-(cast_as_carrier_subset(9206 ^ []) = the_carrier(9206 ^ [])), one_sorted_str(9206 ^ [])],extension(2824 ^ 1,bind([[_93805], [9206 ^ []]]))).
% 0.47/1.37  ncf('1.1.1',plain,[-(one_sorted_str(9206 ^ []))],extension(9208 ^ 2)).
% 0.47/1.37  %-----------------------------------------------------
% 0.47/1.37  End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------