%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU275+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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:02:58 EDT 2023
% Result : Theorem 1.61s 2.45s
% Output : Proof 1.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU275+2 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n026.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 12:59:05 EDT 2023
% 0.13/0.35 % CPUTime :
% 1.61/2.45
% 1.61/2.45 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 1.61/2.45 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.61/2.45 %-----------------------------------------------------
% 1.61/2.45 ncf(matrix, plain, [(5908 ^ _341635) ^ [] : [-(ordinal(5906 ^ []))], (5910 ^ _341635) ^ [] : [well_ordering(inclusion_relation(5906 ^ []))], (406 ^ _341635) ^ [_354621, _354623, _354625, _354627, _354629, _354631] : [-(unordered_triple(_354631, _354627, _354623) = unordered_triple(_354629, _354625, _354621)), _354631 = _354629, _354627 = _354625, _354623 = _354621], (420 ^ _341635) ^ [_355081, _355083] : [_355083 = _355081, -(set_meet(_355083) = set_meet(_355081))], (426 ^ _341635) ^ [_355327, _355329, _355331, _355333] : [-(relation_image(_355333, _355329) = relation_image(_355331, _355327)), _355333 = _355331, _355329 = _355327], (436 ^ _341635) ^ [_355686, _355688, _355690, _355692] : [-(relation_inverse_image(_355692, _355688) = relation_inverse_image(_355690, _355686)), _355692 = _355690, _355688 = _355686], (446 ^ _341635) ^ [_356045, _356047, _356049, _356051] : [-(relation_rng_restriction(_356051, _356047) = relation_rng_restriction(_356049, _356045)), _356051 = _356049, _356047 = _356045], (456 ^ _341635) ^ [_356404, _356406, _356408, _356410] : [-(cartesian_product2(_356410, _356406) = cartesian_product2(_356408, _356404)), _356410 = _356408, _356406 = _356404], (466 ^ _341635) ^ [_356763, _356765, _356767, _356769] : [-(fiber(_356769, _356765) = fiber(_356767, _356763)), _356769 = _356767, _356765 = _356763], (476 ^ _341635) ^ [_357150, _357152, _357154, _357156, _357158, _357160] : [-(relation_dom_as_subset(_357160, _357156, _357152) = relation_dom_as_subset(_357158, _357154, _357150)), _357160 = _357158, _357156 = _357154, _357152 = _357150], (490 ^ _341635) ^ [_357666, _357668, _357670, _357672, _357674, _357676] : [-(relation_rng_as_subset(_357676, _357672, _357668) = relation_rng_as_subset(_357674, _357670, _357666)), _357676 = _357674, _357672 = _357670, _357668 = _357666], (504 ^ _341635) ^ [_358126, _358128] : [_358128 = _358126, -(relation_inverse(_358128) = relation_inverse(_358126))], (510 ^ _341635) ^ [_358372, _358374, _358376, _358378] : [-(relation_restriction(_358378, _358374) = relation_restriction(_358376, _358372)), _358378 = _358376, _358374 = _358372], (520 ^ _341635) ^ [_358703, _358705] : [_358705 = _358703, -(succ(_358705) = succ(_358703))], (526 ^ _341635) ^ [_358949, _358951, _358953, _358955] : [-(union_of_subsets(_358955, _358951) = union_of_subsets(_358953, _358949)), _358955 = _358953, _358951 = _358949], (536 ^ _341635) ^ [_359308, _359310, _359312, _359314] : [-(complements_of_subsets(_359314, _359310) = complements_of_subsets(_359312, _359308)), _359314 = _359312, _359310 = _359308], (546 ^ _341635) ^ [_359695, _359697, _359699, _359701, _359703, _359705] : [-(subset_difference(_359705, _359701, _359697) = subset_difference(_359703, _359699, _359695)), _359705 = _359703, _359701 = _359699, _359697 = _359695], (560 ^ _341635) ^ [_360155, _360157] : [_360157 = _360155, -(cast_to_subset(_360157) = cast_to_subset(_360155))], (566 ^ _341635) ^ [_360401, _360403, _360405, _360407] : [-(meet_of_subsets(_360407, _360403) = meet_of_subsets(_360405, _360401)), _360407 = _360405, _360403 = _360401], (576 ^ _341635) ^ [_360760, _360762, _360764, _360766] : [-(subset_complement(_360766, _360762) = subset_complement(_360764, _360760)), _360766 = _360764, _360762 = _360760], (586 ^ _341635) ^ [_361091, _361093] : [_361093 = _361091, -(function_inverse(_361093) = function_inverse(_361091))], (592 ^ _341635) ^ [_361309, _361311] : [_361311 = _361309, -(pair_first(_361311) = pair_first(_361309))], (598 ^ _341635) ^ [_361527, _361529] : [_361529 = _361527, -(pair_second(_361529) = pair_second(_361527))], (604 ^ _341635) ^ [_361773, _361775, _361777, _361779] : [-(set_difference(_361779, _361775) = set_difference(_361777, _361773)), _361779 = _361777, _361775 = _361773], (614 ^ _341635) ^ [_362132, _362134, _362136, _362138] : [-(ordered_pair(_362138, _362134) = ordered_pair(_362136, _362132)), _362138 = _362136, _362134 = _362132], (624 ^ _341635) ^ [_362491, _362493, _362495, _362497] : [-(apply(_362497, _362493) = apply(_362495, _362491)), _362497 = _362495, _362493 = _362491], (634 ^ _341635) ^ [_362822, _362824] : [_362824 = _362822, -(relation_field(_362824) = relation_field(_362822))], (640 ^ _341635) ^ [_363068, _363070, _363072, _363074] : [-(set_union2(_363074, _363070) = set_union2(_363072, _363068)), _363074 = _363072, _363070 = _363068], (650 ^ _341635) ^ [_363427, _363429, _363431, _363433] : [-(set_intersection2(_363433, _363429) = set_intersection2(_363431, _363427)), _363433 = _363431, _363429 = _363427], (660 ^ _341635) ^ [_363758, _363760] : [_363760 = _363758, -(relation_dom(_363760) = relation_dom(_363758))], (666 ^ _341635) ^ [_364004, _364006, _364008, _364010] : [-(relation_composition(_364010, _364006) = relation_composition(_364008, _364004)), _364010 = _364008, _364006 = _364004], (676 ^ _341635) ^ [_364335, _364337] : [_364337 = _364335, -(identity_relation(_364337) = identity_relation(_364335))], (682 ^ _341635) ^ [_364581, _364583, _364585, _364587] : [-(relation_dom_restriction(_364587, _364583) = relation_dom_restriction(_364585, _364581)), _364587 = _364585, _364583 = _364581], (692 ^ _341635) ^ [_364912, _364914] : [_364914 = _364912, -(relation_rng(_364914) = relation_rng(_364912))], (698 ^ _341635) ^ [_365130, _365132] : [_365132 = _365130, -(union(_365132) = union(_365130))], (704 ^ _341635) ^ [_365348, _365350] : [_365350 = _365348, -(powerset(_365350) = powerset(_365348))], (710 ^ _341635) ^ [_365566, _365568] : [_365568 = _365566, -(singleton(_365568) = singleton(_365566))], (726 ^ _341635) ^ [_366123, _366125] : [_366125 = _366123, -(inclusion_relation(_366125) = inclusion_relation(_366123))], (716 ^ _341635) ^ [_365812, _365814, _365816, _365818] : [-(unordered_pair(_365818, _365814) = unordered_pair(_365816, _365812)), _365818 = _365816, _365814 = _365812], (2 ^ _341635) ^ [_341779] : [-(_341779 = _341779)], (4 ^ _341635) ^ [_341886, _341888] : [_341888 = _341886, -(_341886 = _341888)], (10 ^ _341635) ^ [_342090, _342092, _342094] : [-(_342094 = _342090), _342094 = _342092, _342092 = _342090], (20 ^ _341635) ^ [_342431, _342433, _342435, _342437] : [-(is_antisymmetric_in(_342435, _342431)), is_antisymmetric_in(_342437, _342433), _342437 = _342435, _342433 = _342431], (34 ^ _341635) ^ [_342875, _342877, _342879, _342881] : [-(is_connected_in(_342879, _342875)), is_connected_in(_342881, _342877), _342881 = _342879, _342877 = _342875], (48 ^ _341635) ^ [_343319, _343321, _343323, _343325] : [-(is_transitive_in(_343323, _343319)), is_transitive_in(_343325, _343321), _343325 = _343323, _343321 = _343319], (62 ^ _341635) ^ [_343763, _343765, _343767, _343769] : [-(is_reflexive_in(_343767, _343763)), is_reflexive_in(_343769, _343765), _343769 = _343767, _343765 = _343763], (76 ^ _341635) ^ [_344179, _344181] : [-(epsilon_connected(_344179)), _344181 = _344179, epsilon_connected(_344181)], (86 ^ _341635) ^ [_344474, _344476] : [-(relation_empty_yielding(_344474)), _344476 = _344474, relation_empty_yielding(_344476)], (96 ^ _341635) ^ [_344825, _344827, _344829, _344831, _344833, _344835] : [-(relation_of2(_344833, _344829, _344825)), relation_of2(_344835, _344831, _344827), _344835 = _344833, _344831 = _344829, _344827 = _344825], (114 ^ _341635) ^ [_345378, _345380] : [-(epsilon_transitive(_345378)), _345380 = _345378, epsilon_transitive(_345380)], (124 ^ _341635) ^ [_345729, _345731, _345733, _345735, _345737, _345739] : [-(relation_of2_as_subset(_345737, _345733, _345729)), relation_of2_as_subset(_345739, _345735, _345731), _345739 = _345737, _345735 = _345733, _345731 = _345729], (142 ^ _341635) ^ [_346310, _346312, _346314, _346316] : [-(ordinal_subset(_346314, _346310)), ordinal_subset(_346316, _346312), _346316 = _346314, _346312 = _346310], (156 ^ _341635) ^ [_346726, _346728] : [-(being_limit_ordinal(_346726)), _346728 = _346726, being_limit_ordinal(_346728)], (166 ^ _341635) ^ [_347021, _347023] : [-(reflexive(_347021)), _347023 = _347021, reflexive(_347023)], (176 ^ _341635) ^ [_347316, _347318] : [-(transitive(_347316)), _347318 = _347316, transitive(_347318)], (186 ^ _341635) ^ [_347611, _347613] : [-(connected(_347611)), _347613 = _347611, connected(_347613)], (196 ^ _341635) ^ [_347962, _347964, _347966, _347968, _347970, _347972] : [-(relation_isomorphism(_347970, _347966, _347962)), relation_isomorphism(_347972, _347968, _347964), _347972 = _347970, _347968 = _347966, _347964 = _347962], (214 ^ _341635) ^ [_348543, _348545, _348547, _348549] : [-(element(_348547, _348543)), element(_348549, _348545), _348549 = _348547, _348545 = _348543], (228 ^ _341635) ^ [_348987, _348989, _348991, _348993] : [-(is_well_founded_in(_348991, _348987)), is_well_founded_in(_348993, _348989), _348993 = _348991, _348989 = _348987], (242 ^ _341635) ^ [_349403, _349405] : [-(antisymmetric(_349403)), _349405 = _349403, antisymmetric(_349405)], (252 ^ _341635) ^ [_349726, _349728, _349730, _349732] : [-(proper_subset(_349730, _349726)), proper_subset(_349732, _349728), _349732 = _349730, _349728 = _349726], (266 ^ _341635) ^ [_350142, _350144] : [-(one_to_one(_350142)), _350144 = _350142, one_to_one(_350144)], (276 ^ _341635) ^ [_350437, _350439] : [-(well_founded_relation(_350437)), _350439 = _350437, well_founded_relation(_350439)], (286 ^ _341635) ^ [_350760, _350762, _350764, _350766] : [-(disjoint(_350764, _350760)), disjoint(_350766, _350762), _350766 = _350764, _350762 = _350760], (300 ^ _341635) ^ [_351176, _351178] : [-(empty(_351176)), _351178 = _351176, empty(_351178)], (310 ^ _341635) ^ [_351471, _351473] : [-(function(_351471)), _351473 = _351471, function(_351473)], (320 ^ _341635) ^ [_351794, _351796, _351798, _351800] : [-(well_orders(_351798, _351794)), well_orders(_351800, _351796), _351800 = _351798, _351796 = _351794], (334 ^ _341635) ^ [_352210, _352212] : [-(relation(_352210)), _352212 = _352210, relation(_352212)], (344 ^ _341635) ^ [_352533, _352535, _352537, _352539] : [-(subset(_352537, _352533)), subset(_352539, _352535), _352539 = _352537, _352535 = _352533], (358 ^ _341635) ^ [_352977, _352979, _352981, _352983] : [-(are_equipotent(_352981, _352977)), are_equipotent(_352983, _352979), _352983 = _352981, _352979 = _352977], (372 ^ _341635) ^ [_353421, _353423, _353425, _353427] : [-(in(_353425, _353421)), in(_353427, _353423), _353427 = _353425, _353423 = _353421], (386 ^ _341635) ^ [_353837, _353839] : [-(ordinal(_353837)), _353839 = _353837, ordinal(_353839)], (396 ^ _341635) ^ [_354112, _354114] : [-(well_ordering(_354112)), _354114 = _354112, well_ordering(_354114)], (732 ^ _341635) ^ [_366574, _366576] : [in(_366576, _366574), in(_366574, _366576)], (738 ^ _341635) ^ [_366785, _366787] : [proper_subset(_366787, _366785), proper_subset(_366785, _366787)], (744 ^ _341635) ^ [_366982] : [empty(_366982), -(function(_366982))], (750 ^ _341635) ^ [_367168] : [ordinal(_367168), 753 ^ _341635 : [(754 ^ _341635) ^ [] : [-(epsilon_transitive(_367168))], (756 ^ _341635) ^ [] : [-(epsilon_connected(_367168))]]], (758 ^ _341635) ^ [_367425] : [empty(_367425), -(relation(_367425))], (764 ^ _341635) ^ [_367639, _367641, _367643] : [element(_367639, powerset(cartesian_product2(_367643, _367641))), -(relation(_367639))], (770 ^ _341635) ^ [_367849] : [781 ^ _341635 : [(782 ^ _341635) ^ [] : [-(relation(_367849))], (784 ^ _341635) ^ [] : [-(function(_367849))], (786 ^ _341635) ^ [] : [-(one_to_one(_367849))]], relation(_367849), empty(_367849), function(_367849)], (788 ^ _341635) ^ [_368342] : [-(ordinal(_368342)), epsilon_transitive(_368342), epsilon_connected(_368342)], (798 ^ _341635) ^ [_368611] : [empty(_368611), 801 ^ _341635 : [(802 ^ _341635) ^ [] : [-(epsilon_transitive(_368611))], (804 ^ _341635) ^ [] : [-(epsilon_connected(_368611))], (806 ^ _341635) ^ [] : [-(ordinal(_368611))]]], (808 ^ _341635) ^ [_368937, _368939] : [-(unordered_pair(_368939, _368937) = unordered_pair(_368937, _368939))], (810 ^ _341635) ^ [_369037, _369039] : [-(set_union2(_369039, _369037) = set_union2(_369037, _369039))], (812 ^ _341635) ^ [_369137, _369139] : [-(set_intersection2(_369139, _369137) = set_intersection2(_369137, _369139))], (814 ^ _341635) ^ [_369252, _369254] : [ordinal(_369254), ordinal(_369252), -(ordinal_subset(_369254, _369252)), -(ordinal_subset(_369252, _369254))], (828 ^ _341635) ^ [_369639, _369641] : [relation(_369639), 831 ^ _341635 : [(854 ^ _341635) ^ [] : [-(_369639 = identity_relation(_369641)), 867 ^ _341635 : [(868 ^ _341635) ^ [] : [-(in(855 ^ [_369639, _369641], _369641))], (870 ^ _341635) ^ [] : [-(855 ^ [_369639, _369641] = 856 ^ [_369639, _369641])], (872 ^ _341635) ^ [] : [in(ordered_pair(855 ^ [_369639, _369641], 856 ^ [_369639, _369641]), _369639)]], 859 ^ _341635 : [(860 ^ _341635) ^ [] : [-(in(ordered_pair(855 ^ [_369639, _369641], 856 ^ [_369639, _369641]), _369639))], (862 ^ _341635) ^ [] : [in(855 ^ [_369639, _369641], _369641), 855 ^ [_369639, _369641] = 856 ^ [_369639, _369641]]]], (832 ^ _341635) ^ [] : [_369639 = identity_relation(_369641), 835 ^ _341635 : [(836 ^ _341635) ^ [_369949, _369951] : [in(ordered_pair(_369951, _369949), _369639), 839 ^ _341635 : [(840 ^ _341635) ^ [] : [-(in(_369951, _369641))], (842 ^ _341635) ^ [] : [-(_369951 = _369949)]]], (844 ^ _341635) ^ [_370212, _370214] : [-(in(ordered_pair(_370214, _370212), _369639)), in(_370214, _369641), _370214 = _370212]]]]], (876 ^ _341635) ^ [_371320, _371322] : [_371322 = _371320, 879 ^ _341635 : [(880 ^ _341635) ^ [] : [-(subset(_371322, _371320))], (882 ^ _341635) ^ [] : [-(subset(_371320, _371322))]]], (884 ^ _341635) ^ [_371557, _371559] : [-(_371559 = _371557), subset(_371559, _371557), subset(_371557, _371559)], (894 ^ _341635) ^ [_371844] : [relation(_371844), 897 ^ _341635 : [(898 ^ _341635) ^ [_372030, _372032] : [relation(_372030), 901 ^ _341635 : [(924 ^ _341635) ^ [] : [-(_372030 = relation_dom_restriction(_371844, _372032)), 937 ^ _341635 : [(938 ^ _341635) ^ [] : [-(in(925 ^ [_371844, _372030, _372032], _372032))], (940 ^ _341635) ^ [] : [-(in(ordered_pair(925 ^ [_371844, _372030, _372032], 926 ^ [_371844, _372030, _372032]), _371844))], (942 ^ _341635) ^ [] : [in(ordered_pair(925 ^ [_371844, _372030, _372032], 926 ^ [_371844, _372030, _372032]), _372030)]], 929 ^ _341635 : [(930 ^ _341635) ^ [] : [-(in(ordered_pair(925 ^ [_371844, _372030, _372032], 926 ^ [_371844, _372030, _372032]), _372030))], (932 ^ _341635) ^ [] : [in(925 ^ [_371844, _372030, _372032], _372032), in(ordered_pair(925 ^ [_371844, _372030, _372032], 926 ^ [_371844, _372030, _372032]), _371844)]]], (902 ^ _341635) ^ [] : [_372030 = relation_dom_restriction(_371844, _372032), 905 ^ _341635 : [(906 ^ _341635) ^ [_372355, _372357] : [in(ordered_pair(_372357, _372355), _372030), 909 ^ _341635 : [(910 ^ _341635) ^ [] : [-(in(_372357, _372032))], (912 ^ _341635) ^ [] : [-(in(ordered_pair(_372357, _372355), _371844))]]], (914 ^ _341635) ^ [_372634, _372636] : [-(in(ordered_pair(_372636, _372634), _372030)), in(_372636, _372032), in(ordered_pair(_372636, _372634), _371844)]]]]]]], (946 ^ _341635) ^ [_373789] : [relation(_373789), function(_373789), 953 ^ _341635 : [(983 ^ _341635) ^ [_375215, _375217] : [-(_375215 = relation_image(_373789, _375217)), 1000 ^ _341635 : [(1001 ^ _341635) ^ [] : [-(in(999 ^ [_373789, _375215, _375217], relation_dom(_373789)))], (1003 ^ _341635) ^ [] : [-(in(999 ^ [_373789, _375215, _375217], _375217))], (1005 ^ _341635) ^ [] : [-(984 ^ [_373789, _375215, _375217] = apply(_373789, 999 ^ [_373789, _375215, _375217]))], (1007 ^ _341635) ^ [] : [in(984 ^ [_373789, _375215, _375217], _375215)]], 987 ^ _341635 : [(988 ^ _341635) ^ [] : [-(in(984 ^ [_373789, _375215, _375217], _375215))], (990 ^ _341635) ^ [_375535] : [in(_375535, relation_dom(_373789)), in(_375535, _375217), 984 ^ [_373789, _375215, _375217] = apply(_373789, _375535)]]], (954 ^ _341635) ^ [_374087, _374089] : [_374087 = relation_image(_373789, _374089), 957 ^ _341635 : [(958 ^ _341635) ^ [_374287] : [in(_374287, _374087), 962 ^ _341635 : [(963 ^ _341635) ^ [] : [-(in(961 ^ [_373789, _374087, _374089, _374287], relation_dom(_373789)))], (965 ^ _341635) ^ [] : [-(in(961 ^ [_373789, _374087, _374089, _374287], _374089))], (967 ^ _341635) ^ [] : [-(_374287 = apply(_373789, 961 ^ [_373789, _374087, _374089, _374287]))]]], (969 ^ _341635) ^ [_374742] : [-(in(_374742, _374087)), 970 ^ _341635 : [(971 ^ _341635) ^ [_374855] : [in(_374855, relation_dom(_373789)), in(_374855, _374089), _374742 = apply(_373789, _374855)]]]]]]], (1011 ^ _341635) ^ [_376345, _376347] : [relation(_376345), 1014 ^ _341635 : [(1015 ^ _341635) ^ [_376516] : [relation(_376516), 1018 ^ _341635 : [(1041 ^ _341635) ^ [] : [-(_376516 = relation_rng_restriction(_376347, _376345)), 1054 ^ _341635 : [(1055 ^ _341635) ^ [] : [-(in(1043 ^ [_376345, _376347, _376516], _376347))], (1057 ^ _341635) ^ [] : [-(in(ordered_pair(1042 ^ [_376345, _376347, _376516], 1043 ^ [_376345, _376347, _376516]), _376345))], (1059 ^ _341635) ^ [] : [in(ordered_pair(1042 ^ [_376345, _376347, _376516], 1043 ^ [_376345, _376347, _376516]), _376516)]], 1046 ^ _341635 : [(1047 ^ _341635) ^ [] : [-(in(ordered_pair(1042 ^ [_376345, _376347, _376516], 1043 ^ [_376345, _376347, _376516]), _376516))], (1049 ^ _341635) ^ [] : [in(1043 ^ [_376345, _376347, _376516], _376347), in(ordered_pair(1042 ^ [_376345, _376347, _376516], 1043 ^ [_376345, _376347, _376516]), _376345)]]], (1019 ^ _341635) ^ [] : [_376516 = relation_rng_restriction(_376347, _376345), 1022 ^ _341635 : [(1023 ^ _341635) ^ [_376843, _376845] : [in(ordered_pair(_376845, _376843), _376516), 1026 ^ _341635 : [(1027 ^ _341635) ^ [] : [-(in(_376843, _376347))], (1029 ^ _341635) ^ [] : [-(in(ordered_pair(_376845, _376843), _376345))]]], (1031 ^ _341635) ^ [_377122, _377124] : [-(in(ordered_pair(_377124, _377122), _376516)), in(_377122, _376347), in(ordered_pair(_377124, _377122), _376345)]]]]]]], (1063 ^ _341635) ^ [_378268] : [relation(_378268), 1066 ^ _341635 : [(1067 ^ _341635) ^ [] : [antisymmetric(_378268), -(is_antisymmetric_in(_378268, relation_field(_378268)))], (1073 ^ _341635) ^ [] : [is_antisymmetric_in(_378268, relation_field(_378268)), -(antisymmetric(_378268))]]], (1079 ^ _341635) ^ [_378699] : [relation(_378699), function(_378699), 1086 ^ _341635 : [(1109 ^ _341635) ^ [_379738, _379740] : [-(_379738 = relation_inverse_image(_378699, _379740)), 1121 ^ _341635 : [(1122 ^ _341635) ^ [] : [-(in(1110 ^ [_378699, _379738, _379740], relation_dom(_378699)))], (1124 ^ _341635) ^ [] : [-(in(apply(_378699, 1110 ^ [_378699, _379738, _379740]), _379740))], (1126 ^ _341635) ^ [] : [in(1110 ^ [_378699, _379738, _379740], _379738)]], 1113 ^ _341635 : [(1114 ^ _341635) ^ [] : [-(in(1110 ^ [_378699, _379738, _379740], _379738))], (1116 ^ _341635) ^ [] : [in(1110 ^ [_378699, _379738, _379740], relation_dom(_378699)), in(apply(_378699, 1110 ^ [_378699, _379738, _379740]), _379740)]]], (1087 ^ _341635) ^ [_378986, _378988] : [_378986 = relation_inverse_image(_378699, _378988), 1090 ^ _341635 : [(1091 ^ _341635) ^ [_379175] : [in(_379175, _378986), 1094 ^ _341635 : [(1095 ^ _341635) ^ [] : [-(in(_379175, relation_dom(_378699)))], (1097 ^ _341635) ^ [] : [-(in(apply(_378699, _379175), _378988))]]], (1099 ^ _341635) ^ [_379444] : [-(in(_379444, _378986)), in(_379444, relation_dom(_378699)), in(apply(_378699, _379444), _378988)]]]]], (1130 ^ _341635) ^ [_380506] : [relation(_380506), 1133 ^ _341635 : [(1157 ^ _341635) ^ [_381619, _381621] : [-(_381619 = relation_image(_380506, _381621)), 1170 ^ _341635 : [(1171 ^ _341635) ^ [] : [-(in(ordered_pair(1169 ^ [_380506, _381619, _381621], 1158 ^ [_380506, _381619, _381621]), _380506))], (1173 ^ _341635) ^ [] : [-(in(1169 ^ [_380506, _381619, _381621], _381621))], (1175 ^ _341635) ^ [] : [in(1158 ^ [_380506, _381619, _381621], _381619)]], 1161 ^ _341635 : [(1162 ^ _341635) ^ [] : [-(in(1158 ^ [_380506, _381619, _381621], _381619))], (1164 ^ _341635) ^ [_381923] : [in(ordered_pair(_381923, 1158 ^ [_380506, _381619, _381621]), _380506), in(_381923, _381621)]]], (1134 ^ _341635) ^ [_380713, _380715] : [_380713 = relation_image(_380506, _380715), 1137 ^ _341635 : [(1138 ^ _341635) ^ [_380905] : [in(_380905, _380713), 1142 ^ _341635 : [(1143 ^ _341635) ^ [] : [-(in(ordered_pair(1141 ^ [_380506, _380713, _380715, _380905], _380905), _380506))], (1145 ^ _341635) ^ [] : [-(in(1141 ^ [_380506, _380713, _380715, _380905], _380715))]]], (1147 ^ _341635) ^ [_381259] : [-(in(_381259, _380713)), 1148 ^ _341635 : [(1149 ^ _341635) ^ [_381364] : [in(ordered_pair(_381364, _381259), _380506), in(_381364, _380715)]]]]]]], (1179 ^ _341635) ^ [_382525] : [relation(_382525), 1182 ^ _341635 : [(1206 ^ _341635) ^ [_383638, _383640] : [-(_383638 = relation_inverse_image(_382525, _383640)), 1219 ^ _341635 : [(1220 ^ _341635) ^ [] : [-(in(ordered_pair(1207 ^ [_382525, _383638, _383640], 1218 ^ [_382525, _383638, _383640]), _382525))], (1222 ^ _341635) ^ [] : [-(in(1218 ^ [_382525, _383638, _383640], _383640))], (1224 ^ _341635) ^ [] : [in(1207 ^ [_382525, _383638, _383640], _383638)]], 1210 ^ _341635 : [(1211 ^ _341635) ^ [] : [-(in(1207 ^ [_382525, _383638, _383640], _383638))], (1213 ^ _341635) ^ [_383942] : [in(ordered_pair(1207 ^ [_382525, _383638, _383640], _383942), _382525), in(_383942, _383640)]]], (1183 ^ _341635) ^ [_382732, _382734] : [_382732 = relation_inverse_image(_382525, _382734), 1186 ^ _341635 : [(1187 ^ _341635) ^ [_382924] : [in(_382924, _382732), 1191 ^ _341635 : [(1192 ^ _341635) ^ [] : [-(in(ordered_pair(_382924, 1190 ^ [_382525, _382732, _382734, _382924]), _382525))], (1194 ^ _341635) ^ [] : [-(in(1190 ^ [_382525, _382732, _382734, _382924], _382734))]]], (1196 ^ _341635) ^ [_383278] : [-(in(_383278, _382732)), 1197 ^ _341635 : [(1198 ^ _341635) ^ [_383383] : [in(ordered_pair(_383278, _383383), _382525), in(_383383, _382734)]]]]]]], (1228 ^ _341635) ^ [_384544] : [relation(_384544), 1231 ^ _341635 : [(1232 ^ _341635) ^ [] : [connected(_384544), -(is_connected_in(_384544, relation_field(_384544)))], (1238 ^ _341635) ^ [] : [is_connected_in(_384544, relation_field(_384544)), -(connected(_384544))]]], (1244 ^ _341635) ^ [_384975] : [relation(_384975), 1247 ^ _341635 : [(1248 ^ _341635) ^ [] : [transitive(_384975), -(is_transitive_in(_384975, relation_field(_384975)))], (1254 ^ _341635) ^ [] : [is_transitive_in(_384975, relation_field(_384975)), -(transitive(_384975))]]], (1288 ^ _341635) ^ [_386441, _386443, _386445, _386447] : [-(_386441 = unordered_triple(_386447, _386445, _386443)), 1292 ^ _341635 : [(1293 ^ _341635) ^ [] : [-(in(1289 ^ [_386441, _386443, _386445, _386447], _386441))], (1295 ^ _341635) ^ [] : [1289 ^ [_386441, _386443, _386445, _386447] = _386447], (1297 ^ _341635) ^ [] : [1289 ^ [_386441, _386443, _386445, _386447] = _386445], (1299 ^ _341635) ^ [] : [1289 ^ [_386441, _386443, _386445, _386447] = _386443]], 1300 ^ _341635 : [(1311 ^ _341635) ^ [] : [in(1289 ^ [_386441, _386443, _386445, _386447], _386441)], (1301 ^ _341635) ^ [] : [-(1289 ^ [_386441, _386443, _386445, _386447] = _386447), -(1289 ^ [_386441, _386443, _386445, _386447] = _386445), -(1289 ^ [_386441, _386443, _386445, _386447] = _386443)]]], (1260 ^ _341635) ^ [_385477, _385479, _385481, _385483] : [_385477 = unordered_triple(_385483, _385481, _385479), 1263 ^ _341635 : [(1278 ^ _341635) ^ [_386079] : [1279 ^ _341635 : [(1280 ^ _341635) ^ [] : [_386079 = _385483], (1282 ^ _341635) ^ [] : [_386079 = _385481], (1284 ^ _341635) ^ [] : [_386079 = _385479]], -(in(_386079, _385477))], (1264 ^ _341635) ^ [_385679] : [in(_385679, _385477), -(_385679 = _385483), -(_385679 = _385481), -(_385679 = _385479)]]], (1315 ^ _341635) ^ [_387429] : [1316 ^ _341635 : [(1317 ^ _341635) ^ [_387551, _387553] : [_387429 = ordered_pair(_387553, _387551)]], 1318 ^ _341635 : [(1329 ^ _341635) ^ [_388014] : [1332 ^ _341635 : [(1333 ^ _341635) ^ [] : [-(_387429 = ordered_pair(1330 ^ [_387429, _388014], 1331 ^ [_387429, _388014]))], (1335 ^ _341635) ^ [] : [_388014 = 1330 ^ [_387429, _388014]]], -(_388014 = pair_first(_387429))], (1319 ^ _341635) ^ [_387660] : [_387660 = pair_first(_387429), 1322 ^ _341635 : [(1323 ^ _341635) ^ [_387825, _387827] : [_387429 = ordered_pair(_387827, _387825), -(_387660 = _387827)]]]]], (1339 ^ _341635) ^ [_388448] : [-(succ(_388448) = set_union2(_388448, singleton(_388448)))], (1353 ^ _341635) ^ [_389038] : [1355 ^ _341635 : [(1356 ^ _341635) ^ [] : [-(in(1354 ^ [_389038], _389038))], (1358 ^ _341635) ^ [_389275, _389277] : [1354 ^ [_389038] = ordered_pair(_389277, _389275)]], -(relation(_389038))], (1341 ^ _341635) ^ [_388577] : [relation(_388577), 1344 ^ _341635 : [(1345 ^ _341635) ^ [_388725] : [in(_388725, _388577), -(_388725 = ordered_pair(1348 ^ [_388577, _388725], 1349 ^ [_388577, _388725]))]]], (1362 ^ _341635) ^ [_389432] : [relation(_389432), 1365 ^ _341635 : [(1376 ^ _341635) ^ [_389931] : [1378 ^ _341635 : [(1379 ^ _341635) ^ [] : [-(in(1377 ^ [_389432, _389931], _389931))], (1381 ^ _341635) ^ [] : [in(ordered_pair(1377 ^ [_389432, _389931], 1377 ^ [_389432, _389931]), _389432)]], -(is_reflexive_in(_389432, _389931))], (1366 ^ _341635) ^ [_389606] : [is_reflexive_in(_389432, _389606), 1369 ^ _341635 : [(1370 ^ _341635) ^ [_389748] : [in(_389748, _389606), -(in(ordered_pair(_389748, _389748), _389432))]]]]], (1385 ^ _341635) ^ [_390354, _390356, _390358] : [relation_of2(_390354, _390358, _390356), -(subset(_390354, cartesian_product2(_390358, _390356)))], (1391 ^ _341635) ^ [_390530, _390532, _390534] : [subset(_390530, cartesian_product2(_390534, _390532)), -(relation_of2(_390530, _390534, _390532))], (1446 ^ _341635) ^ [_392483, _392485] : [_392485 = empty_set, 1449 ^ _341635 : [(1450 ^ _341635) ^ [] : [_392483 = set_meet(_392485), -(_392483 = empty_set)], (1456 ^ _341635) ^ [] : [_392483 = empty_set, -(_392483 = set_meet(_392485))]]], (1397 ^ _341635) ^ [_390776, _390778] : [-(_390778 = empty_set), 1400 ^ _341635 : [(1424 ^ _341635) ^ [] : [-(_390776 = set_meet(_390778)), 1428 ^ _341635 : [(1429 ^ _341635) ^ [] : [-(in(1425 ^ [_390776, _390778], _390776))], (1432 ^ _341635) ^ [] : [-(in(1430 ^ [_390776, _390778], _390778))], (1434 ^ _341635) ^ [] : [in(1425 ^ [_390776, _390778], 1430 ^ [_390776, _390778])]], 1435 ^ _341635 : [(1442 ^ _341635) ^ [] : [in(1425 ^ [_390776, _390778], _390776)], (1436 ^ _341635) ^ [_392178] : [in(_392178, _390778), -(in(1425 ^ [_390776, _390778], _392178))]]], (1401 ^ _341635) ^ [] : [_390776 = set_meet(_390778), 1404 ^ _341635 : [(1415 ^ _341635) ^ [_391404] : [1417 ^ _341635 : [(1418 ^ _341635) ^ [] : [-(in(1416 ^ [_390776, _390778, _391404], _390778))], (1420 ^ _341635) ^ [] : [in(_391404, 1416 ^ [_390776, _390778, _391404])]], -(in(_391404, _390776))], (1405 ^ _341635) ^ [_391074] : [in(_391074, _390776), 1408 ^ _341635 : [(1409 ^ _341635) ^ [_391219] : [in(_391219, _390778), -(in(_391074, _391219))]]]]]]], (1478 ^ _341635) ^ [_393501, _393503] : [-(_393501 = singleton(_393503)), 1482 ^ _341635 : [(1483 ^ _341635) ^ [] : [-(in(1479 ^ [_393501, _393503], _393501))], (1485 ^ _341635) ^ [] : [1479 ^ [_393501, _393503] = _393503]], 1486 ^ _341635 : [(1487 ^ _341635) ^ [] : [-(1479 ^ [_393501, _393503] = _393503)], (1489 ^ _341635) ^ [] : [in(1479 ^ [_393501, _393503], _393501)]]], (1462 ^ _341635) ^ [_392980, _392982] : [_392980 = singleton(_392982), 1465 ^ _341635 : [(1466 ^ _341635) ^ [_393150] : [in(_393150, _392980), -(_393150 = _392982)], (1472 ^ _341635) ^ [_393322] : [_393322 = _392982, -(in(_393322, _392980))]]], (1493 ^ _341635) ^ [_394023] : [relation(_394023), 1496 ^ _341635 : [(1519 ^ _341635) ^ [_394975, _394977] : [-(_394975 = fiber(_394023, _394977)), 1531 ^ _341635 : [(1532 ^ _341635) ^ [] : [1520 ^ [_394023, _394975, _394977] = _394977], (1534 ^ _341635) ^ [] : [-(in(ordered_pair(1520 ^ [_394023, _394975, _394977], _394977), _394023))], (1536 ^ _341635) ^ [] : [in(1520 ^ [_394023, _394975, _394977], _394975)]], 1523 ^ _341635 : [(1524 ^ _341635) ^ [] : [-(in(1520 ^ [_394023, _394975, _394977], _394975))], (1526 ^ _341635) ^ [] : [-(1520 ^ [_394023, _394975, _394977] = _394977), in(ordered_pair(1520 ^ [_394023, _394975, _394977], _394977), _394023)]]], (1497 ^ _341635) ^ [_394227, _394229] : [_394227 = fiber(_394023, _394229), 1500 ^ _341635 : [(1501 ^ _341635) ^ [_394416] : [in(_394416, _394227), 1504 ^ _341635 : [(1505 ^ _341635) ^ [] : [_394416 = _394229], (1507 ^ _341635) ^ [] : [-(in(ordered_pair(_394416, _394229), _394023))]]], (1509 ^ _341635) ^ [_394682] : [-(in(_394682, _394227)), -(_394682 = _394229), in(ordered_pair(_394682, _394229), _394023)]]]]], (1540 ^ _341635) ^ [_395751, _395753] : [relation(_395751), 1543 ^ _341635 : [(1570 ^ _341635) ^ [] : [-(_395751 = inclusion_relation(_395753)), relation_field(_395751) = _395753, 1577 ^ _341635 : [(1578 ^ _341635) ^ [] : [-(in(1575 ^ [_395751, _395753], _395753))], (1580 ^ _341635) ^ [] : [-(in(1576 ^ [_395751, _395753], _395753))], (1582 ^ _341635) ^ [] : [1583 ^ _341635 : [(1584 ^ _341635) ^ [] : [-(in(ordered_pair(1575 ^ [_395751, _395753], 1576 ^ [_395751, _395753]), _395751))], (1586 ^ _341635) ^ [] : [subset(1575 ^ [_395751, _395753], 1576 ^ [_395751, _395753])]], 1587 ^ _341635 : [(1588 ^ _341635) ^ [] : [-(subset(1575 ^ [_395751, _395753], 1576 ^ [_395751, _395753]))], (1590 ^ _341635) ^ [] : [in(ordered_pair(1575 ^ [_395751, _395753], 1576 ^ [_395751, _395753]), _395751)]]]]], (1544 ^ _341635) ^ [] : [_395751 = inclusion_relation(_395753), 1547 ^ _341635 : [(1548 ^ _341635) ^ [] : [-(relation_field(_395751) = _395753)], (1550 ^ _341635) ^ [_396114, _396116] : [in(_396116, _395753), in(_396114, _395753), 1557 ^ _341635 : [(1558 ^ _341635) ^ [] : [in(ordered_pair(_396116, _396114), _395751), -(subset(_396116, _396114))], (1564 ^ _341635) ^ [] : [subset(_396116, _396114), -(in(ordered_pair(_396116, _396114), _395751))]]]]]]], (1594 ^ _341635) ^ [_397566] : [_397566 = empty_set, 1597 ^ _341635 : [(1598 ^ _341635) ^ [_397679] : [in(_397679, _397566)]]], (1600 ^ _341635) ^ [_397745] : [-(in(1601 ^ [_397745], _397745)), -(_397745 = empty_set)], (1623 ^ _341635) ^ [_398557, _398559] : [-(_398557 = powerset(_398559)), 1627 ^ _341635 : [(1628 ^ _341635) ^ [] : [-(in(1624 ^ [_398557, _398559], _398557))], (1630 ^ _341635) ^ [] : [subset(1624 ^ [_398557, _398559], _398559)]], 1631 ^ _341635 : [(1632 ^ _341635) ^ [] : [-(subset(1624 ^ [_398557, _398559], _398559))], (1634 ^ _341635) ^ [] : [in(1624 ^ [_398557, _398559], _398557)]]], (1607 ^ _341635) ^ [_398036, _398038] : [_398036 = powerset(_398038), 1610 ^ _341635 : [(1611 ^ _341635) ^ [_398206] : [in(_398206, _398036), -(subset(_398206, _398038))], (1617 ^ _341635) ^ [_398378] : [subset(_398378, _398038), -(in(_398378, _398036))]]], (1638 ^ _341635) ^ [_399079] : [1639 ^ _341635 : [(1640 ^ _341635) ^ [_399201, _399203] : [_399079 = ordered_pair(_399203, _399201)]], 1641 ^ _341635 : [(1652 ^ _341635) ^ [_399664] : [1655 ^ _341635 : [(1656 ^ _341635) ^ [] : [-(_399079 = ordered_pair(1653 ^ [_399079, _399664], 1654 ^ [_399079, _399664]))], (1658 ^ _341635) ^ [] : [_399664 = 1654 ^ [_399079, _399664]]], -(_399664 = pair_second(_399079))], (1642 ^ _341635) ^ [_399310] : [_399310 = pair_second(_399079), 1645 ^ _341635 : [(1646 ^ _341635) ^ [_399475, _399477] : [_399079 = ordered_pair(_399477, _399475), -(_399310 = _399475)]]]]], (1672 ^ _341635) ^ [_400435] : [1674 ^ _341635 : [(1675 ^ _341635) ^ [] : [-(in(1673 ^ [_400435], _400435))], (1677 ^ _341635) ^ [] : [subset(1673 ^ [_400435], _400435)]], -(epsilon_transitive(_400435))], (1662 ^ _341635) ^ [_400135] : [epsilon_transitive(_400135), 1665 ^ _341635 : [(1666 ^ _341635) ^ [_400266] : [in(_400266, _400135), -(subset(_400266, _400135))]]], (1681 ^ _341635) ^ [_400760] : [relation(_400760), 1684 ^ _341635 : [(1685 ^ _341635) ^ [_400918] : [relation(_400918), 1688 ^ _341635 : [(1705 ^ _341635) ^ [] : [-(_400760 = _400918), 1710 ^ _341635 : [(1711 ^ _341635) ^ [] : [-(in(ordered_pair(1706 ^ [_400760, _400918], 1707 ^ [_400760, _400918]), _400760))], (1713 ^ _341635) ^ [] : [in(ordered_pair(1706 ^ [_400760, _400918], 1707 ^ [_400760, _400918]), _400918)]], 1714 ^ _341635 : [(1715 ^ _341635) ^ [] : [-(in(ordered_pair(1706 ^ [_400760, _400918], 1707 ^ [_400760, _400918]), _400918))], (1717 ^ _341635) ^ [] : [in(ordered_pair(1706 ^ [_400760, _400918], 1707 ^ [_400760, _400918]), _400760)]]], (1689 ^ _341635) ^ [] : [_400760 = _400918, 1692 ^ _341635 : [(1693 ^ _341635) ^ [_401223, _401225] : [in(ordered_pair(_401225, _401223), _400760), -(in(ordered_pair(_401225, _401223), _400918))], (1699 ^ _341635) ^ [_401413, _401415] : [in(ordered_pair(_401415, _401413), _400918), -(in(ordered_pair(_401415, _401413), _400760))]]]]]]], (1721 ^ _341635) ^ [_402250, _402252] : [-(empty(_402252)), 1724 ^ _341635 : [(1725 ^ _341635) ^ [] : [element(_402250, _402252), -(in(_402250, _402252))], (1731 ^ _341635) ^ [] : [in(_402250, _402252), -(element(_402250, _402252))]]], (1737 ^ _341635) ^ [_402663, _402665] : [empty(_402665), 1740 ^ _341635 : [(1741 ^ _341635) ^ [] : [element(_402663, _402665), -(empty(_402663))], (1747 ^ _341635) ^ [] : [empty(_402663), -(element(_402663, _402665))]]], (1775 ^ _341635) ^ [_403888, _403890, _403892] : [-(_403888 = unordered_pair(_403892, _403890)), 1779 ^ _341635 : [(1780 ^ _341635) ^ [] : [-(in(1776 ^ [_403888, _403890, _403892], _403888))], (1782 ^ _341635) ^ [] : [1776 ^ [_403888, _403890, _403892] = _403892], (1784 ^ _341635) ^ [] : [1776 ^ [_403888, _403890, _403892] = _403890]], 1785 ^ _341635 : [(1792 ^ _341635) ^ [] : [in(1776 ^ [_403888, _403890, _403892], _403888)], (1786 ^ _341635) ^ [] : [-(1776 ^ [_403888, _403890, _403892] = _403892), -(1776 ^ [_403888, _403890, _403892] = _403890)]]], (1753 ^ _341635) ^ [_403163, _403165, _403167] : [_403163 = unordered_pair(_403167, _403165), 1756 ^ _341635 : [(1767 ^ _341635) ^ [_403623] : [1768 ^ _341635 : [(1769 ^ _341635) ^ [] : [_403623 = _403167], (1771 ^ _341635) ^ [] : [_403623 = _403165]], -(in(_403623, _403163))], (1757 ^ _341635) ^ [_403345] : [in(_403345, _403163), -(_403345 = _403167), -(_403345 = _403165)]]], (1796 ^ _341635) ^ [_404625] : [relation(_404625), 1799 ^ _341635 : [(1817 ^ _341635) ^ [] : [-(well_founded_relation(_404625)), 1819 ^ _341635 : [(1820 ^ _341635) ^ [] : [-(subset(1818 ^ [_404625], relation_field(_404625)))], (1822 ^ _341635) ^ [] : [1818 ^ [_404625] = empty_set], (1824 ^ _341635) ^ [_405575] : [in(_405575, 1818 ^ [_404625]), disjoint(fiber(_404625, _405575), 1818 ^ [_404625])]]], (1800 ^ _341635) ^ [] : [well_founded_relation(_404625), 1803 ^ _341635 : [(1804 ^ _341635) ^ [_404892] : [subset(_404892, relation_field(_404625)), -(_404892 = empty_set), 1812 ^ _341635 : [(1813 ^ _341635) ^ [] : [-(in(1811 ^ [_404625, _404892], _404892))], (1815 ^ _341635) ^ [] : [-(disjoint(fiber(_404625, 1811 ^ [_404625, _404892]), _404892))]]]]]]], (1854 ^ _341635) ^ [_406639, _406641, _406643] : [-(_406639 = set_union2(_406643, _406641)), 1858 ^ _341635 : [(1859 ^ _341635) ^ [] : [-(in(1855 ^ [_406639, _406641, _406643], _406639))], (1861 ^ _341635) ^ [] : [in(1855 ^ [_406639, _406641, _406643], _406643)], (1863 ^ _341635) ^ [] : [in(1855 ^ [_406639, _406641, _406643], _406641)]], 1864 ^ _341635 : [(1871 ^ _341635) ^ [] : [in(1855 ^ [_406639, _406641, _406643], _406639)], (1865 ^ _341635) ^ [] : [-(in(1855 ^ [_406639, _406641, _406643], _406643)), -(in(1855 ^ [_406639, _406641, _406643], _406641))]]], (1832 ^ _341635) ^ [_405914, _405916, _405918] : [_405914 = set_union2(_405918, _405916), 1835 ^ _341635 : [(1846 ^ _341635) ^ [_406374] : [1847 ^ _341635 : [(1848 ^ _341635) ^ [] : [in(_406374, _405918)], (1850 ^ _341635) ^ [] : [in(_406374, _405916)]], -(in(_406374, _405914))], (1836 ^ _341635) ^ [_406096] : [in(_406096, _405914), -(in(_406096, _405918)), -(in(_406096, _405916))]]], (1905 ^ _341635) ^ [_408690, _408692, _408694] : [-(_408690 = cartesian_product2(_408694, _408692)), 1923 ^ _341635 : [(1924 ^ _341635) ^ [] : [-(in(1921 ^ [_408690, _408692, _408694], _408694))], (1926 ^ _341635) ^ [] : [-(in(1922 ^ [_408690, _408692, _408694], _408692))], (1928 ^ _341635) ^ [] : [-(1906 ^ [_408690, _408692, _408694] = ordered_pair(1921 ^ [_408690, _408692, _408694], 1922 ^ [_408690, _408692, _408694]))], (1930 ^ _341635) ^ [] : [in(1906 ^ [_408690, _408692, _408694], _408690)]], 1909 ^ _341635 : [(1910 ^ _341635) ^ [] : [-(in(1906 ^ [_408690, _408692, _408694], _408690))], (1912 ^ _341635) ^ [_409028, _409030] : [in(_409030, _408694), in(_409028, _408692), 1906 ^ [_408690, _408692, _408694] = ordered_pair(_409030, _409028)]]], (1875 ^ _341635) ^ [_407433, _407435, _407437] : [_407433 = cartesian_product2(_407437, _407435), 1878 ^ _341635 : [(1879 ^ _341635) ^ [_407634] : [in(_407634, _407433), 1884 ^ _341635 : [(1885 ^ _341635) ^ [] : [-(in(1882 ^ [_407433, _407435, _407437, _407634], _407437))], (1887 ^ _341635) ^ [] : [-(in(1883 ^ [_407433, _407435, _407437, _407634], _407435))], (1889 ^ _341635) ^ [] : [-(_407634 = ordered_pair(1882 ^ [_407433, _407435, _407437, _407634], 1883 ^ [_407433, _407435, _407437, _407634]))]]], (1891 ^ _341635) ^ [_408194] : [-(in(_408194, _407433)), 1892 ^ _341635 : [(1893 ^ _341635) ^ [_408324, _408326] : [in(_408326, _407437), in(_408324, _407435), _408194 = ordered_pair(_408326, _408324)]]]]], (1956 ^ _341635) ^ [_410591] : [1959 ^ _341635 : [(1960 ^ _341635) ^ [] : [-(in(1957 ^ [_410591], _410591))], (1962 ^ _341635) ^ [] : [-(in(1958 ^ [_410591], _410591))], (1964 ^ _341635) ^ [] : [in(1957 ^ [_410591], 1958 ^ [_410591])], (1966 ^ _341635) ^ [] : [1957 ^ [_410591] = 1958 ^ [_410591]], (1968 ^ _341635) ^ [] : [in(1958 ^ [_410591], 1957 ^ [_410591])]], -(epsilon_connected(_410591))], (1934 ^ _341635) ^ [_409953] : [epsilon_connected(_409953), 1937 ^ _341635 : [(1938 ^ _341635) ^ [_410129, _410131] : [in(_410131, _409953), in(_410129, _409953), -(in(_410131, _410129)), -(_410131 = _410129), -(in(_410129, _410131))]]], (1972 ^ _341635) ^ [_411297] : [relation(_411297), 1975 ^ _341635 : [(1976 ^ _341635) ^ [_411455] : [relation(_411455), 1979 ^ _341635 : [(1990 ^ _341635) ^ [] : [1993 ^ _341635 : [(1994 ^ _341635) ^ [] : [-(in(ordered_pair(1991 ^ [_411297, _411455], 1992 ^ [_411297, _411455]), _411297))], (1996 ^ _341635) ^ [] : [in(ordered_pair(1991 ^ [_411297, _411455], 1992 ^ [_411297, _411455]), _411455)]], -(subset(_411297, _411455))], (1980 ^ _341635) ^ [] : [subset(_411297, _411455), 1983 ^ _341635 : [(1984 ^ _341635) ^ [_411731, _411733] : [in(ordered_pair(_411733, _411731), _411297), -(in(ordered_pair(_411733, _411731), _411455))]]]]]]], (2010 ^ _341635) ^ [_412694, _412696] : [2012 ^ _341635 : [(2013 ^ _341635) ^ [] : [-(in(2011 ^ [_412694, _412696], _412696))], (2015 ^ _341635) ^ [] : [in(2011 ^ [_412694, _412696], _412694)]], -(subset(_412696, _412694))], (2000 ^ _341635) ^ [_412380, _412382] : [subset(_412382, _412380), 2003 ^ _341635 : [(2004 ^ _341635) ^ [_412517] : [in(_412517, _412382), -(in(_412517, _412380))]]], (2019 ^ _341635) ^ [_413037] : [relation(_413037), 2022 ^ _341635 : [(2040 ^ _341635) ^ [_413840] : [-(is_well_founded_in(_413037, _413840)), 2042 ^ _341635 : [(2043 ^ _341635) ^ [] : [-(subset(2041 ^ [_413037, _413840], _413840))], (2045 ^ _341635) ^ [] : [2041 ^ [_413037, _413840] = empty_set], (2047 ^ _341635) ^ [_414182] : [in(_414182, 2041 ^ [_413037, _413840]), disjoint(fiber(_413037, _414182), 2041 ^ [_413037, _413840])]]], (2023 ^ _341635) ^ [_413234] : [is_well_founded_in(_413037, _413234), 2026 ^ _341635 : [(2027 ^ _341635) ^ [_413399] : [subset(_413399, _413234), -(_413399 = empty_set), 2035 ^ _341635 : [(2036 ^ _341635) ^ [] : [-(in(2034 ^ [_413037, _413234, _413399], _413399))], (2038 ^ _341635) ^ [] : [-(disjoint(fiber(_413037, 2034 ^ [_413037, _413234, _413399]), _413399))]]]]]]], (2077 ^ _341635) ^ [_415265, _415267, _415269] : [-(_415265 = set_intersection2(_415269, _415267)), 2089 ^ _341635 : [(2090 ^ _341635) ^ [] : [-(in(2078 ^ [_415265, _415267, _415269], _415269))], (2092 ^ _341635) ^ [] : [-(in(2078 ^ [_415265, _415267, _415269], _415267))], (2094 ^ _341635) ^ [] : [in(2078 ^ [_415265, _415267, _415269], _415265)]], 2081 ^ _341635 : [(2082 ^ _341635) ^ [] : [-(in(2078 ^ [_415265, _415267, _415269], _415265))], (2084 ^ _341635) ^ [] : [in(2078 ^ [_415265, _415267, _415269], _415269), in(2078 ^ [_415265, _415267, _415269], _415267)]]], (2055 ^ _341635) ^ [_414540, _414542, _414544] : [_414540 = set_intersection2(_414544, _414542), 2058 ^ _341635 : [(2059 ^ _341635) ^ [_414722] : [in(_414722, _414540), 2062 ^ _341635 : [(2063 ^ _341635) ^ [] : [-(in(_414722, _414544))], (2065 ^ _341635) ^ [] : [-(in(_414722, _414542))]]], (2067 ^ _341635) ^ [_414981] : [-(in(_414981, _414540)), in(_414981, _414544), in(_414981, _414542)]]], (2098 ^ _341635) ^ [_416004] : [relation(_416004), function(_416004), 2105 ^ _341635 : [(2106 ^ _341635) ^ [_416296, _416298] : [in(_416298, relation_dom(_416004)), 2109 ^ _341635 : [(2110 ^ _341635) ^ [] : [_416296 = apply(_416004, _416298), -(in(ordered_pair(_416298, _416296), _416004))], (2116 ^ _341635) ^ [] : [in(ordered_pair(_416298, _416296), _416004), -(_416296 = apply(_416004, _416298))]]], (2122 ^ _341635) ^ [_416748, _416750] : [-(in(_416750, relation_dom(_416004))), 2125 ^ _341635 : [(2126 ^ _341635) ^ [] : [_416748 = apply(_416004, _416750), -(_416748 = empty_set)], (2132 ^ _341635) ^ [] : [_416748 = empty_set, -(_416748 = apply(_416004, _416750))]]]]], (2138 ^ _341635) ^ [_417266] : [ordinal(_417266), 2141 ^ _341635 : [(2142 ^ _341635) ^ [] : [-(epsilon_transitive(_417266))], (2144 ^ _341635) ^ [] : [-(epsilon_connected(_417266))]]], (2146 ^ _341635) ^ [_417489] : [-(ordinal(_417489)), epsilon_transitive(_417489), epsilon_connected(_417489)], (2156 ^ _341635) ^ [_417760] : [relation(_417760), 2159 ^ _341635 : [(2177 ^ _341635) ^ [_418572] : [-(_418572 = relation_dom(_417760)), 2181 ^ _341635 : [(2182 ^ _341635) ^ [] : [-(in(2178 ^ [_417760, _418572], _418572))], (2184 ^ _341635) ^ [_418835] : [in(ordered_pair(2178 ^ [_417760, _418572], _418835), _417760)]], 2186 ^ _341635 : [(2187 ^ _341635) ^ [] : [-(in(ordered_pair(2178 ^ [_417760, _418572], 2185 ^ [_417760, _418572]), _417760))], (2189 ^ _341635) ^ [] : [in(2178 ^ [_417760, _418572], _418572)]]], (2160 ^ _341635) ^ [_417941] : [_417941 = relation_dom(_417760), 2163 ^ _341635 : [(2164 ^ _341635) ^ [_418121] : [in(_418121, _417941), -(in(ordered_pair(_418121, 2167 ^ [_417760, _417941, _418121]), _417760))], (2171 ^ _341635) ^ [_418365] : [2172 ^ _341635 : [(2173 ^ _341635) ^ [_418444] : [in(ordered_pair(_418365, _418444), _417760)]], -(in(_418365, _417941))]]]]], (2193 ^ _341635) ^ [_419201] : [relation(_419201), 2196 ^ _341635 : [(2219 ^ _341635) ^ [_420069] : [2222 ^ _341635 : [(2223 ^ _341635) ^ [] : [-(in(2220 ^ [_419201, _420069], _420069))], (2225 ^ _341635) ^ [] : [-(in(2221 ^ [_419201, _420069], _420069))], (2227 ^ _341635) ^ [] : [-(in(ordered_pair(2220 ^ [_419201, _420069], 2221 ^ [_419201, _420069]), _419201))], (2229 ^ _341635) ^ [] : [-(in(ordered_pair(2221 ^ [_419201, _420069], 2220 ^ [_419201, _420069]), _419201))], (2231 ^ _341635) ^ [] : [2220 ^ [_419201, _420069] = 2221 ^ [_419201, _420069]]], -(is_antisymmetric_in(_419201, _420069))], (2197 ^ _341635) ^ [_419401] : [is_antisymmetric_in(_419201, _419401), 2200 ^ _341635 : [(2201 ^ _341635) ^ [_419583, _419585] : [-(_419585 = _419583), in(_419585, _419401), in(_419583, _419401), in(ordered_pair(_419585, _419583), _419201), in(ordered_pair(_419583, _419585), _419201)]]]]], (2235 ^ _341635) ^ [_420823] : [-(cast_to_subset(_420823) = _420823)], (2260 ^ _341635) ^ [_421806, _421808] : [-(_421806 = union(_421808)), 2273 ^ _341635 : [(2274 ^ _341635) ^ [] : [-(in(2261 ^ [_421806, _421808], 2272 ^ [_421806, _421808]))], (2276 ^ _341635) ^ [] : [-(in(2272 ^ [_421806, _421808], _421808))], (2278 ^ _341635) ^ [] : [in(2261 ^ [_421806, _421808], _421806)]], 2264 ^ _341635 : [(2265 ^ _341635) ^ [] : [-(in(2261 ^ [_421806, _421808], _421806))], (2267 ^ _341635) ^ [_422089] : [in(2261 ^ [_421806, _421808], _422089), in(_422089, _421808)]]], (2237 ^ _341635) ^ [_420961, _420963] : [_420961 = union(_420963), 2240 ^ _341635 : [(2241 ^ _341635) ^ [_421142] : [in(_421142, _420961), 2245 ^ _341635 : [(2246 ^ _341635) ^ [] : [-(in(_421142, 2244 ^ [_420961, _420963, _421142]))], (2248 ^ _341635) ^ [] : [-(in(2244 ^ [_420961, _420963, _421142], _420963))]]], (2250 ^ _341635) ^ [_421469] : [-(in(_421469, _420961)), 2251 ^ _341635 : [(2252 ^ _341635) ^ [_421567] : [in(_421469, _421567), in(_421567, _420963)]]]]], (2282 ^ _341635) ^ [_422639] : [relation(_422639), 2285 ^ _341635 : [(2286 ^ _341635) ^ [] : [well_ordering(_422639), 2289 ^ _341635 : [(2290 ^ _341635) ^ [] : [-(reflexive(_422639))], (2292 ^ _341635) ^ [] : [-(transitive(_422639))], (2294 ^ _341635) ^ [] : [-(antisymmetric(_422639))], (2296 ^ _341635) ^ [] : [-(connected(_422639))], (2298 ^ _341635) ^ [] : [-(well_founded_relation(_422639))]]], (2300 ^ _341635) ^ [] : [-(well_ordering(_422639)), reflexive(_422639), transitive(_422639), antisymmetric(_422639), connected(_422639), well_founded_relation(_422639)]]], (2344 ^ _341635) ^ [_424442, _424444, _424446] : [-(_424442 = set_difference(_424446, _424444)), 2356 ^ _341635 : [(2357 ^ _341635) ^ [] : [-(in(2345 ^ [_424442, _424444, _424446], _424446))], (2359 ^ _341635) ^ [] : [in(2345 ^ [_424442, _424444, _424446], _424444)], (2361 ^ _341635) ^ [] : [in(2345 ^ [_424442, _424444, _424446], _424442)]], 2348 ^ _341635 : [(2349 ^ _341635) ^ [] : [-(in(2345 ^ [_424442, _424444, _424446], _424442))], (2351 ^ _341635) ^ [] : [in(2345 ^ [_424442, _424444, _424446], _424446), -(in(2345 ^ [_424442, _424444, _424446], _424444))]]], (2322 ^ _341635) ^ [_423711, _423713, _423715] : [_423711 = set_difference(_423715, _423713), 2325 ^ _341635 : [(2326 ^ _341635) ^ [_423895] : [in(_423895, _423711), 2329 ^ _341635 : [(2330 ^ _341635) ^ [] : [-(in(_423895, _423715))], (2332 ^ _341635) ^ [] : [in(_423895, _423713)]]], (2334 ^ _341635) ^ [_424155] : [-(in(_424155, _423711)), in(_424155, _423715), -(in(_424155, _423713))]]], (2365 ^ _341635) ^ [_425185] : [relation(_425185), function(_425185), 2372 ^ _341635 : [(2396 ^ _341635) ^ [_426339] : [-(_426339 = relation_rng(_425185)), 2409 ^ _341635 : [(2410 ^ _341635) ^ [] : [-(in(2408 ^ [_425185, _426339], relation_dom(_425185)))], (2412 ^ _341635) ^ [] : [-(2397 ^ [_425185, _426339] = apply(_425185, 2408 ^ [_425185, _426339]))], (2414 ^ _341635) ^ [] : [in(2397 ^ [_425185, _426339], _426339)]], 2400 ^ _341635 : [(2401 ^ _341635) ^ [] : [-(in(2397 ^ [_425185, _426339], _426339))], (2403 ^ _341635) ^ [_426634] : [in(_426634, relation_dom(_425185)), 2397 ^ [_425185, _426339] = apply(_425185, _426634)]]], (2373 ^ _341635) ^ [_425457] : [_425457 = relation_rng(_425185), 2376 ^ _341635 : [(2377 ^ _341635) ^ [_425645] : [in(_425645, _425457), 2381 ^ _341635 : [(2382 ^ _341635) ^ [] : [-(in(2380 ^ [_425185, _425457, _425645], relation_dom(_425185)))], (2384 ^ _341635) ^ [] : [-(_425645 = apply(_425185, 2380 ^ [_425185, _425457, _425645]))]]], (2386 ^ _341635) ^ [_425987] : [-(in(_425987, _425457)), 2387 ^ _341635 : [(2388 ^ _341635) ^ [_426090] : [in(_426090, relation_dom(_425185)), _425987 = apply(_425185, _426090)]]]]]]], (2418 ^ _341635) ^ [_427211] : [relation(_427211), 2421 ^ _341635 : [(2439 ^ _341635) ^ [_428023] : [-(_428023 = relation_rng(_427211)), 2443 ^ _341635 : [(2444 ^ _341635) ^ [] : [-(in(2440 ^ [_427211, _428023], _428023))], (2446 ^ _341635) ^ [_428286] : [in(ordered_pair(_428286, 2440 ^ [_427211, _428023]), _427211)]], 2448 ^ _341635 : [(2449 ^ _341635) ^ [] : [-(in(ordered_pair(2447 ^ [_427211, _428023], 2440 ^ [_427211, _428023]), _427211))], (2451 ^ _341635) ^ [] : [in(2440 ^ [_427211, _428023], _428023)]]], (2422 ^ _341635) ^ [_427392] : [_427392 = relation_rng(_427211), 2425 ^ _341635 : [(2426 ^ _341635) ^ [_427572] : [in(_427572, _427392), -(in(ordered_pair(2429 ^ [_427211, _427392, _427572], _427572), _427211))], (2433 ^ _341635) ^ [_427816] : [2434 ^ _341635 : [(2435 ^ _341635) ^ [_427895] : [in(ordered_pair(_427895, _427816), _427211)]], -(in(_427816, _427392))]]]]], (2455 ^ _341635) ^ [_428666, _428668] : [element(_428666, powerset(_428668)), -(subset_complement(_428668, _428666) = set_difference(_428668, _428666))], (2461 ^ _341635) ^ [_428877, _428879] : [-(ordered_pair(_428879, _428877) = unordered_pair(unordered_pair(_428879, _428877), singleton(_428879)))], (2463 ^ _341635) ^ [_428983] : [relation(_428983), 2466 ^ _341635 : [(2467 ^ _341635) ^ [_429167] : [well_orders(_428983, _429167), 2470 ^ _341635 : [(2471 ^ _341635) ^ [] : [-(is_reflexive_in(_428983, _429167))], (2473 ^ _341635) ^ [] : [-(is_transitive_in(_428983, _429167))], (2475 ^ _341635) ^ [] : [-(is_antisymmetric_in(_428983, _429167))], (2477 ^ _341635) ^ [] : [-(is_connected_in(_428983, _429167))], (2479 ^ _341635) ^ [] : [-(is_well_founded_in(_428983, _429167))]]], (2481 ^ _341635) ^ [_429628] : [-(well_orders(_428983, _429628)), is_reflexive_in(_428983, _429628), is_transitive_in(_428983, _429628), is_antisymmetric_in(_428983, _429628), is_connected_in(_428983, _429628), is_well_founded_in(_428983, _429628)]]], (2503 ^ _341635) ^ [_430218] : [being_limit_ordinal(_430218), -(_430218 = union(_430218))], (2509 ^ _341635) ^ [_430376] : [_430376 = union(_430376), -(being_limit_ordinal(_430376))], (2515 ^ _341635) ^ [_430570] : [relation(_430570), -(relation_field(_430570) = set_union2(relation_dom(_430570), relation_rng(_430570)))], (2521 ^ _341635) ^ [_430776] : [relation(_430776), 2524 ^ _341635 : [(2547 ^ _341635) ^ [_431668] : [2550 ^ _341635 : [(2551 ^ _341635) ^ [] : [-(in(2548 ^ [_430776, _431668], _431668))], (2553 ^ _341635) ^ [] : [-(in(2549 ^ [_430776, _431668], _431668))], (2555 ^ _341635) ^ [] : [2548 ^ [_430776, _431668] = 2549 ^ [_430776, _431668]], (2557 ^ _341635) ^ [] : [in(ordered_pair(2548 ^ [_430776, _431668], 2549 ^ [_430776, _431668]), _430776)], (2559 ^ _341635) ^ [] : [in(ordered_pair(2549 ^ [_430776, _431668], 2548 ^ [_430776, _431668]), _430776)]], -(is_connected_in(_430776, _431668))], (2525 ^ _341635) ^ [_430984] : [is_connected_in(_430776, _430984), 2528 ^ _341635 : [(2529 ^ _341635) ^ [_431174, _431176] : [in(_431176, _430984), in(_431174, _430984), -(_431176 = _431174), -(in(ordered_pair(_431176, _431174), _430776)), -(in(ordered_pair(_431174, _431176), _430776))]]]]], (2563 ^ _341635) ^ [_432453] : [relation(_432453), 2566 ^ _341635 : [(2567 ^ _341635) ^ [_432572] : [-(relation_restriction(_432453, _432572) = set_intersection2(_432453, cartesian_product2(_432572, _432572)))]]], (2569 ^ _341635) ^ [_432681] : [relation(_432681), 2572 ^ _341635 : [(2573 ^ _341635) ^ [_432841] : [relation(_432841), 2576 ^ _341635 : [(2593 ^ _341635) ^ [] : [-(_432841 = relation_inverse(_432681)), 2598 ^ _341635 : [(2599 ^ _341635) ^ [] : [-(in(ordered_pair(2594 ^ [_432681, _432841], 2595 ^ [_432681, _432841]), _432841))], (2601 ^ _341635) ^ [] : [in(ordered_pair(2595 ^ [_432681, _432841], 2594 ^ [_432681, _432841]), _432681)]], 2602 ^ _341635 : [(2603 ^ _341635) ^ [] : [-(in(ordered_pair(2595 ^ [_432681, _432841], 2594 ^ [_432681, _432841]), _432681))], (2605 ^ _341635) ^ [] : [in(ordered_pair(2594 ^ [_432681, _432841], 2595 ^ [_432681, _432841]), _432841)]]], (2577 ^ _341635) ^ [] : [_432841 = relation_inverse(_432681), 2580 ^ _341635 : [(2581 ^ _341635) ^ [_433150, _433152] : [in(ordered_pair(_433152, _433150), _432841), -(in(ordered_pair(_433150, _433152), _432681))], (2587 ^ _341635) ^ [_433340, _433342] : [in(ordered_pair(_433340, _433342), _432681), -(in(ordered_pair(_433342, _433340), _432841))]]]]]]], (2609 ^ _341635) ^ [_434145] : [relation(_434145), 2612 ^ _341635 : [(2613 ^ _341635) ^ [_434366] : [relation(_434366), 2616 ^ _341635 : [(2617 ^ _341635) ^ [_434583] : [relation(_434583), function(_434583), 2624 ^ _341635 : [(2659 ^ _341635) ^ [] : [-(relation_isomorphism(_434145, _434366, _434583)), relation_dom(_434583) = relation_field(_434145), relation_rng(_434583) = relation_field(_434366), one_to_one(_434583), 2688 ^ _341635 : [(2689 ^ _341635) ^ [] : [-(in(2672 ^ [_434145, _434366, _434583], relation_field(_434145)))], (2691 ^ _341635) ^ [] : [-(in(2673 ^ [_434145, _434366, _434583], relation_field(_434145)))], (2693 ^ _341635) ^ [] : [-(in(ordered_pair(apply(_434583, 2672 ^ [_434145, _434366, _434583]), apply(_434583, 2673 ^ [_434145, _434366, _434583])), _434366))], (2695 ^ _341635) ^ [] : [in(ordered_pair(2672 ^ [_434145, _434366, _434583], 2673 ^ [_434145, _434366, _434583]), _434145)]], 2676 ^ _341635 : [(2677 ^ _341635) ^ [] : [-(in(ordered_pair(2672 ^ [_434145, _434366, _434583], 2673 ^ [_434145, _434366, _434583]), _434145))], (2679 ^ _341635) ^ [] : [in(2672 ^ [_434145, _434366, _434583], relation_field(_434145)), in(2673 ^ [_434145, _434366, _434583], relation_field(_434145)), in(ordered_pair(apply(_434583, 2672 ^ [_434145, _434366, _434583]), apply(_434583, 2673 ^ [_434145, _434366, _434583])), _434366)]]], (2625 ^ _341635) ^ [] : [relation_isomorphism(_434145, _434366, _434583), 2628 ^ _341635 : [(2629 ^ _341635) ^ [] : [-(relation_dom(_434583) = relation_field(_434145))], (2631 ^ _341635) ^ [] : [-(relation_rng(_434583) = relation_field(_434366))], (2633 ^ _341635) ^ [] : [-(one_to_one(_434583))], (2635 ^ _341635) ^ [_435249, _435251] : [in(ordered_pair(_435251, _435249), _434145), 2638 ^ _341635 : [(2639 ^ _341635) ^ [] : [-(in(_435251, relation_field(_434145)))], (2641 ^ _341635) ^ [] : [-(in(_435249, relation_field(_434145)))], (2643 ^ _341635) ^ [] : [-(in(ordered_pair(apply(_434583, _435251), apply(_434583, _435249)), _434366))]]], (2645 ^ _341635) ^ [_435628, _435630] : [-(in(ordered_pair(_435630, _435628), _434145)), in(_435630, relation_field(_434145)), in(_435628, relation_field(_434145)), in(ordered_pair(apply(_434583, _435630), apply(_434583, _435628)), _434366)]]]]]]]]], (2699 ^ _341635) ^ [_437455, _437457] : [disjoint(_437457, _437455), -(set_intersection2(_437457, _437455) = empty_set)], (2705 ^ _341635) ^ [_437623, _437625] : [set_intersection2(_437625, _437623) = empty_set, -(disjoint(_437625, _437623))], (2711 ^ _341635) ^ [_437827] : [relation(_437827), function(_437827), 2718 ^ _341635 : [(2737 ^ _341635) ^ [] : [2740 ^ _341635 : [(2741 ^ _341635) ^ [] : [-(in(2738 ^ [_437827], relation_dom(_437827)))], (2743 ^ _341635) ^ [] : [-(in(2739 ^ [_437827], relation_dom(_437827)))], (2745 ^ _341635) ^ [] : [-(apply(_437827, 2738 ^ [_437827]) = apply(_437827, 2739 ^ [_437827]))], (2747 ^ _341635) ^ [] : [2738 ^ [_437827] = 2739 ^ [_437827]]], -(one_to_one(_437827))], (2719 ^ _341635) ^ [] : [one_to_one(_437827), 2722 ^ _341635 : [(2723 ^ _341635) ^ [_438190, _438192] : [-(_438192 = _438190), in(_438192, relation_dom(_437827)), in(_438190, relation_dom(_437827)), apply(_437827, _438192) = apply(_437827, _438190)]]]]], (2751 ^ _341635) ^ [_439137] : [relation(_439137), 2754 ^ _341635 : [(2755 ^ _341635) ^ [_439322] : [relation(_439322), 2758 ^ _341635 : [(2759 ^ _341635) ^ [_439503] : [relation(_439503), 2762 ^ _341635 : [(2786 ^ _341635) ^ [] : [-(_439503 = relation_composition(_439137, _439322)), 2800 ^ _341635 : [(2801 ^ _341635) ^ [] : [-(in(ordered_pair(2787 ^ [_439137, _439322, _439503], 2799 ^ [_439137, _439322, _439503]), _439137))], (2803 ^ _341635) ^ [] : [-(in(ordered_pair(2799 ^ [_439137, _439322, _439503], 2788 ^ [_439137, _439322, _439503]), _439322))], (2805 ^ _341635) ^ [] : [in(ordered_pair(2787 ^ [_439137, _439322, _439503], 2788 ^ [_439137, _439322, _439503]), _439503)]], 2791 ^ _341635 : [(2792 ^ _341635) ^ [] : [-(in(ordered_pair(2787 ^ [_439137, _439322, _439503], 2788 ^ [_439137, _439322, _439503]), _439503))], (2794 ^ _341635) ^ [_440967] : [in(ordered_pair(2787 ^ [_439137, _439322, _439503], _440967), _439137), in(ordered_pair(_440967, 2788 ^ [_439137, _439322, _439503]), _439322)]]], (2763 ^ _341635) ^ [] : [_439503 = relation_composition(_439137, _439322), 2766 ^ _341635 : [(2767 ^ _341635) ^ [_439838, _439840] : [in(ordered_pair(_439840, _439838), _439503), 2771 ^ _341635 : [(2772 ^ _341635) ^ [] : [-(in(ordered_pair(_439840, 2770 ^ [_439137, _439322, _439503, _439838, _439840]), _439137))], (2774 ^ _341635) ^ [] : [-(in(ordered_pair(2770 ^ [_439137, _439322, _439503, _439838, _439840], _439838), _439322))]]], (2776 ^ _341635) ^ [_440223, _440225] : [-(in(ordered_pair(_440225, _440223), _439503)), 2777 ^ _341635 : [(2778 ^ _341635) ^ [_440336] : [in(ordered_pair(_440225, _440336), _439137), in(ordered_pair(_440336, _440223), _439322)]]]]]]]]]]], (2809 ^ _341635) ^ [_441639] : [relation(_441639), 2812 ^ _341635 : [(2839 ^ _341635) ^ [_442674] : [2843 ^ _341635 : [(2844 ^ _341635) ^ [] : [-(in(2840 ^ [_441639, _442674], _442674))], (2846 ^ _341635) ^ [] : [-(in(2841 ^ [_441639, _442674], _442674))], (2848 ^ _341635) ^ [] : [-(in(2842 ^ [_441639, _442674], _442674))], (2850 ^ _341635) ^ [] : [-(in(ordered_pair(2840 ^ [_441639, _442674], 2841 ^ [_441639, _442674]), _441639))], (2852 ^ _341635) ^ [] : [-(in(ordered_pair(2841 ^ [_441639, _442674], 2842 ^ [_441639, _442674]), _441639))], (2854 ^ _341635) ^ [] : [in(ordered_pair(2840 ^ [_441639, _442674], 2842 ^ [_441639, _442674]), _441639)]], -(is_transitive_in(_441639, _442674))], (2813 ^ _341635) ^ [_441853] : [is_transitive_in(_441639, _441853), 2816 ^ _341635 : [(2817 ^ _341635) ^ [_442063, _442065, _442067] : [-(in(ordered_pair(_442067, _442063), _441639)), in(_442067, _441853), in(_442065, _441853), in(_442063, _441853), in(ordered_pair(_442067, _442065), _441639), in(ordered_pair(_442065, _442063), _441639)]]]]], (2858 ^ _341635) ^ [_443698, _443700] : [element(_443698, powerset(powerset(_443700))), 2861 ^ _341635 : [(2862 ^ _341635) ^ [_443878] : [element(_443878, powerset(powerset(_443700))), 2865 ^ _341635 : [(2886 ^ _341635) ^ [] : [-(_443878 = complements_of_subsets(_443700, _443698)), 2888 ^ _341635 : [(2889 ^ _341635) ^ [] : [-(element(2887 ^ [_443698, _443700, _443878], powerset(_443700)))], (2891 ^ _341635) ^ [] : [2892 ^ _341635 : [(2893 ^ _341635) ^ [] : [-(in(2887 ^ [_443698, _443700, _443878], _443878))], (2895 ^ _341635) ^ [] : [in(subset_complement(_443700, 2887 ^ [_443698, _443700, _443878]), _443698)]], 2896 ^ _341635 : [(2897 ^ _341635) ^ [] : [-(in(subset_complement(_443700, 2887 ^ [_443698, _443700, _443878]), _443698))], (2899 ^ _341635) ^ [] : [in(2887 ^ [_443698, _443700, _443878], _443878)]]]]], (2866 ^ _341635) ^ [] : [_443878 = complements_of_subsets(_443700, _443698), 2869 ^ _341635 : [(2870 ^ _341635) ^ [_444166] : [element(_444166, powerset(_443700)), 2873 ^ _341635 : [(2874 ^ _341635) ^ [] : [in(_444166, _443878), -(in(subset_complement(_443700, _444166), _443698))], (2880 ^ _341635) ^ [] : [in(subset_complement(_443700, _444166), _443698), -(in(_444166, _443878))]]]]]]]]], (2903 ^ _341635) ^ [_445289, _445291] : [proper_subset(_445291, _445289), 2906 ^ _341635 : [(2907 ^ _341635) ^ [] : [-(subset(_445291, _445289))], (2909 ^ _341635) ^ [] : [_445291 = _445289]]], (2911 ^ _341635) ^ [_445527, _445529] : [-(proper_subset(_445529, _445527)), subset(_445529, _445527), -(_445529 = _445527)], (2921 ^ _341635) ^ [_445817] : [relation(_445817), function(_445817), one_to_one(_445817), -(function_inverse(_445817) = relation_inverse(_445817))], (2935 ^ _341635) ^ [_446181] : [relation(_446181), 2938 ^ _341635 : [(2939 ^ _341635) ^ [] : [reflexive(_446181), -(is_reflexive_in(_446181, relation_field(_446181)))], (2945 ^ _341635) ^ [] : [is_reflexive_in(_446181, relation_field(_446181)), -(reflexive(_446181))]]], (2951 ^ _341635) ^ [] : [true___, -(true___)], (2957 ^ _341635) ^ [] : [true___, -(true___)], (2963 ^ _341635) ^ [] : [true___, -(true___)], (2969 ^ _341635) ^ [] : [true___, -(true___)], (2975 ^ _341635) ^ [] : [true___, -(true___)], (2981 ^ _341635) ^ [] : [true___, -(true___)], (2987 ^ _341635) ^ [] : [true___, -(true___)], (2993 ^ _341635) ^ [] : [true___, -(true___)], (2999 ^ _341635) ^ [] : [true___, -(true___)], (3005 ^ _341635) ^ [_447668] : [-(relation(inclusion_relation(_447668)))], (3007 ^ _341635) ^ [] : [true___, -(true___)], (3013 ^ _341635) ^ [] : [true___, -(true___)], (3019 ^ _341635) ^ [_448000] : [3026 ^ _341635 : [(3027 ^ _341635) ^ [] : [-(relation(function_inverse(_448000)))], (3029 ^ _341635) ^ [] : [-(function(function_inverse(_448000)))]], relation(_448000), function(_448000)], (3031 ^ _341635) ^ [] : [true___, -(true___)], (3037 ^ _341635) ^ [] : [true___, -(true___)], (3043 ^ _341635) ^ [_448571] : [-(element(cast_to_subset(_448571), powerset(_448571)))], (3045 ^ _341635) ^ [] : [true___, -(true___)], (3051 ^ _341635) ^ [_448801, _448803] : [relation(_448803), -(relation(relation_restriction(_448803, _448801)))], (3057 ^ _341635) ^ [] : [true___, -(true___)], (3063 ^ _341635) ^ [] : [true___, -(true___)], (3069 ^ _341635) ^ [] : [true___, -(true___)], (3075 ^ _341635) ^ [_449370, _449372] : [element(_449370, powerset(_449372)), -(element(subset_complement(_449372, _449370), powerset(_449372)))], (3081 ^ _341635) ^ [] : [true___, -(true___)], (3087 ^ _341635) ^ [] : [true___, -(true___)], (3093 ^ _341635) ^ [_449818] : [relation(_449818), -(relation(relation_inverse(_449818)))], (3099 ^ _341635) ^ [_450036, _450038, _450040] : [relation_of2(_450036, _450040, _450038), -(element(relation_dom_as_subset(_450040, _450038, _450036), powerset(_450040)))], (3105 ^ _341635) ^ [] : [true___, -(true___)], (3111 ^ _341635) ^ [] : [true___, -(true___)], (3117 ^ _341635) ^ [_450504, _450506] : [-(relation(relation_composition(_450506, _450504))), relation(_450506), relation(_450504)], (3127 ^ _341635) ^ [_450817, _450819, _450821] : [relation_of2(_450817, _450821, _450819), -(element(relation_rng_as_subset(_450821, _450819, _450817), powerset(_450819)))], (3133 ^ _341635) ^ [_451047, _451049] : [element(_451047, powerset(powerset(_451049))), -(element(union_of_subsets(_451049, _451047), powerset(_451049)))], (3139 ^ _341635) ^ [_451246] : [-(relation(identity_relation(_451246)))], (3141 ^ _341635) ^ [_451354, _451356] : [element(_451354, powerset(powerset(_451356))), -(element(meet_of_subsets(_451356, _451354), powerset(_451356)))], (3147 ^ _341635) ^ [_451596, _451598, _451600] : [-(element(subset_difference(_451600, _451598, _451596), powerset(_451600))), element(_451598, powerset(_451600)), element(_451596, powerset(_451600))], (3157 ^ _341635) ^ [_451925, _451927] : [relation(_451927), -(relation(relation_dom_restriction(_451927, _451925)))], (3163 ^ _341635) ^ [_452137, _452139] : [element(_452137, powerset(powerset(_452139))), -(element(complements_of_subsets(_452139, _452137), powerset(powerset(_452139))))], (3169 ^ _341635) ^ [_452369, _452371] : [relation(_452369), -(relation(relation_rng_restriction(_452371, _452369)))], (3175 ^ _341635) ^ [] : [true___, -(true___)], (3181 ^ _341635) ^ [] : [true___, -(true___)], (3187 ^ _341635) ^ [] : [true___, -(true___)], (3193 ^ _341635) ^ [_452952, _452954, _452956] : [relation_of2_as_subset(_452952, _452956, _452954), -(element(_452952, powerset(cartesian_product2(_452956, _452954))))], (3200 ^ _341635) ^ [_453207, _453209] : [-(relation_of2(3198 ^ [_453207, _453209], _453209, _453207))], (3203 ^ _341635) ^ [_453334] : [-(element(3201 ^ [_453334], _453334))], (3206 ^ _341635) ^ [_453473, _453475] : [-(relation_of2_as_subset(3204 ^ [_453473, _453475], _453475, _453473))], (3208 ^ _341635) ^ [_453590, _453592] : [3215 ^ _341635 : [(3216 ^ _341635) ^ [] : [-(empty(relation_composition(_453590, _453592)))], (3218 ^ _341635) ^ [] : [-(relation(relation_composition(_453590, _453592)))]], empty(_453592), relation(_453590)], (3220 ^ _341635) ^ [_453954] : [empty(_453954), 3223 ^ _341635 : [(3224 ^ _341635) ^ [] : [-(empty(relation_inverse(_453954)))], (3226 ^ _341635) ^ [] : [-(relation(relation_inverse(_453954)))]]], (3228 ^ _341635) ^ [] : [-(empty(empty_set))], (3230 ^ _341635) ^ [] : [-(relation(empty_set))], (3232 ^ _341635) ^ [] : [-(relation_empty_yielding(empty_set))], (3234 ^ _341635) ^ [_454396, _454398] : [3241 ^ _341635 : [(3242 ^ _341635) ^ [] : [-(relation(relation_dom_restriction(_454398, _454396)))], (3244 ^ _341635) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_454398, _454396)))]], relation(_454398), relation_empty_yielding(_454398)], (3246 ^ _341635) ^ [_454774, _454776] : [3261 ^ _341635 : [(3262 ^ _341635) ^ [] : [-(relation(relation_composition(_454776, _454774)))], (3264 ^ _341635) ^ [] : [-(function(relation_composition(_454776, _454774)))]], relation(_454776), function(_454776), relation(_454774), function(_454774)], (3266 ^ _341635) ^ [_455296] : [empty(succ(_455296))], (3268 ^ _341635) ^ [_455404, _455406] : [-(relation(set_intersection2(_455406, _455404))), relation(_455406), relation(_455404)], (3278 ^ _341635) ^ [_455673] : [empty(powerset(_455673))], (3280 ^ _341635) ^ [] : [-(empty(empty_set))], (3282 ^ _341635) ^ [_455818, _455820] : [empty(ordered_pair(_455820, _455818))], (3284 ^ _341635) ^ [_455920] : [-(relation(identity_relation(_455920)))], (3286 ^ _341635) ^ [_455965] : [-(function(identity_relation(_455965)))], (3288 ^ _341635) ^ [] : [-(relation(empty_set))], (3290 ^ _341635) ^ [] : [-(relation_empty_yielding(empty_set))], (3292 ^ _341635) ^ [] : [-(function(empty_set))], (3294 ^ _341635) ^ [] : [-(one_to_one(empty_set))], (3296 ^ _341635) ^ [] : [-(empty(empty_set))], (3298 ^ _341635) ^ [] : [-(epsilon_transitive(empty_set))], (3300 ^ _341635) ^ [] : [-(epsilon_connected(empty_set))], (3302 ^ _341635) ^ [] : [-(ordinal(empty_set))], (3304 ^ _341635) ^ [_456513, _456515] : [-(relation(set_union2(_456515, _456513))), relation(_456515), relation(_456513)], (3314 ^ _341635) ^ [_456782] : [empty(singleton(_456782))], (3316 ^ _341635) ^ [_456890, _456892] : [-(empty(_456892)), empty(set_union2(_456892, _456890))], (3322 ^ _341635) ^ [_457092] : [3333 ^ _341635 : [(3334 ^ _341635) ^ [] : [-(relation(relation_inverse(_457092)))], (3336 ^ _341635) ^ [] : [-(function(relation_inverse(_457092)))]], relation(_457092), function(_457092), one_to_one(_457092)], (3338 ^ _341635) ^ [_457523] : [ordinal(_457523), 3341 ^ _341635 : [(3342 ^ _341635) ^ [] : [empty(succ(_457523))], (3344 ^ _341635) ^ [] : [-(epsilon_transitive(succ(_457523)))], (3346 ^ _341635) ^ [] : [-(epsilon_connected(succ(_457523)))], (3348 ^ _341635) ^ [] : [-(ordinal(succ(_457523)))]]], (3350 ^ _341635) ^ [_457951, _457953] : [-(relation(set_difference(_457953, _457951))), relation(_457953), relation(_457951)], (3360 ^ _341635) ^ [_458234, _458236] : [empty(unordered_pair(_458236, _458234))], (3362 ^ _341635) ^ [_458345, _458347] : [-(empty(_458347)), empty(set_union2(_458345, _458347))], (3368 ^ _341635) ^ [_458561, _458563] : [3375 ^ _341635 : [(3376 ^ _341635) ^ [] : [-(relation(relation_dom_restriction(_458563, _458561)))], (3378 ^ _341635) ^ [] : [-(function(relation_dom_restriction(_458563, _458561)))]], relation(_458563), function(_458563)], (3380 ^ _341635) ^ [_458925] : [ordinal(_458925), 3383 ^ _341635 : [(3384 ^ _341635) ^ [] : [-(epsilon_transitive(union(_458925)))], (3386 ^ _341635) ^ [] : [-(epsilon_connected(union(_458925)))], (3388 ^ _341635) ^ [] : [-(ordinal(union(_458925)))]]], (3390 ^ _341635) ^ [] : [-(empty(empty_set))], (3392 ^ _341635) ^ [] : [-(relation(empty_set))], (3394 ^ _341635) ^ [_459386, _459388] : [empty(cartesian_product2(_459388, _459386)), -(empty(_459388)), -(empty(_459386))], (3404 ^ _341635) ^ [_459692, _459694] : [3411 ^ _341635 : [(3412 ^ _341635) ^ [] : [-(relation(relation_rng_restriction(_459694, _459692)))], (3414 ^ _341635) ^ [] : [-(function(relation_rng_restriction(_459694, _459692)))]], relation(_459692), function(_459692)], (3416 ^ _341635) ^ [_460056] : [empty(relation_dom(_460056)), -(empty(_460056)), relation(_460056)], (3426 ^ _341635) ^ [_460333] : [empty(relation_rng(_460333)), -(empty(_460333)), relation(_460333)], (3436 ^ _341635) ^ [_460610] : [empty(_460610), 3439 ^ _341635 : [(3440 ^ _341635) ^ [] : [-(empty(relation_dom(_460610)))], (3442 ^ _341635) ^ [] : [-(relation(relation_dom(_460610)))]]], (3444 ^ _341635) ^ [_460875] : [empty(_460875), 3447 ^ _341635 : [(3448 ^ _341635) ^ [] : [-(empty(relation_rng(_460875)))], (3450 ^ _341635) ^ [] : [-(relation(relation_rng(_460875)))]]], (3452 ^ _341635) ^ [_461154, _461156] : [3459 ^ _341635 : [(3460 ^ _341635) ^ [] : [-(empty(relation_composition(_461156, _461154)))], (3462 ^ _341635) ^ [] : [-(relation(relation_composition(_461156, _461154)))]], empty(_461156), relation(_461154)], (3464 ^ _341635) ^ [_461517, _461519] : [-(set_union2(_461519, _461519) = _461519)], (3466 ^ _341635) ^ [_461614, _461616] : [-(set_intersection2(_461616, _461616) = _461616)], (3468 ^ _341635) ^ [_461726, _461728] : [element(_461726, powerset(_461728)), -(subset_complement(_461728, subset_complement(_461728, _461726)) = _461726)], (3474 ^ _341635) ^ [_461938] : [relation(_461938), -(relation_inverse(relation_inverse(_461938)) = _461938)], (3480 ^ _341635) ^ [_462148, _462150] : [element(_462148, powerset(powerset(_462150))), -(complements_of_subsets(_462150, complements_of_subsets(_462150, _462148)) = _462148)], (3486 ^ _341635) ^ [_462362, _462364] : [proper_subset(_462364, _462364)], (3488 ^ _341635) ^ [_462457] : [relation(_462457), 3491 ^ _341635 : [(3502 ^ _341635) ^ [] : [3504 ^ _341635 : [(3505 ^ _341635) ^ [] : [-(in(3503 ^ [_462457], relation_field(_462457)))], (3507 ^ _341635) ^ [] : [in(ordered_pair(3503 ^ [_462457], 3503 ^ [_462457]), _462457)]], -(reflexive(_462457))], (3492 ^ _341635) ^ [] : [reflexive(_462457), 3495 ^ _341635 : [(3496 ^ _341635) ^ [_462701] : [in(_462701, relation_field(_462457)), -(in(ordered_pair(_462701, _462701), _462457))]]]]], (3511 ^ _341635) ^ [_463166] : [singleton(_463166) = empty_set], (3513 ^ _341635) ^ [_463275, _463277] : [in(_463277, _463275), -(set_union2(singleton(_463277), _463275) = _463275)], (3519 ^ _341635) ^ [_463495, _463497] : [disjoint(singleton(_463497), _463495), in(_463497, _463495)], (3525 ^ _341635) ^ [_463708, _463710] : [-(in(_463710, _463708)), -(disjoint(singleton(_463710), _463708))], (3531 ^ _341635) ^ [_463925, _463927] : [relation(_463925), -(subset(relation_dom(relation_rng_restriction(_463927, _463925)), relation_dom(_463925)))], (3537 ^ _341635) ^ [_464133] : [relation(_464133), 3540 ^ _341635 : [(3555 ^ _341635) ^ [] : [3559 ^ _341635 : [(3560 ^ _341635) ^ [] : [-(in(ordered_pair(3556 ^ [_464133], 3557 ^ [_464133]), _464133))], (3562 ^ _341635) ^ [] : [-(in(ordered_pair(3557 ^ [_464133], 3558 ^ [_464133]), _464133))], (3564 ^ _341635) ^ [] : [in(ordered_pair(3556 ^ [_464133], 3558 ^ [_464133]), _464133)]], -(transitive(_464133))], (3541 ^ _341635) ^ [] : [transitive(_464133), 3544 ^ _341635 : [(3545 ^ _341635) ^ [_464425, _464427, _464429] : [-(in(ordered_pair(_464429, _464425), _464133)), in(ordered_pair(_464429, _464427), _464133), in(ordered_pair(_464427, _464425), _464133)]]]]], (3568 ^ _341635) ^ [_465332, _465334] : [subset(singleton(_465334), _465332), -(in(_465334, _465332))], (3574 ^ _341635) ^ [_465498, _465500] : [in(_465500, _465498), -(subset(singleton(_465500), _465498))], (3580 ^ _341635) ^ [_465743, _465745] : [set_difference(_465745, _465743) = empty_set, -(subset(_465745, _465743))], (3586 ^ _341635) ^ [_465911, _465913] : [subset(_465913, _465911), -(set_difference(_465913, _465911) = empty_set)], (3592 ^ _341635) ^ [_466129, _466131] : [element(_466129, powerset(_466131)), 3595 ^ _341635 : [(3596 ^ _341635) ^ [_466270] : [in(_466270, _466129), -(in(_466270, _466131))]]], (3602 ^ _341635) ^ [_466481] : [relation(_466481), 3605 ^ _341635 : [(3620 ^ _341635) ^ [] : [3623 ^ _341635 : [(3624 ^ _341635) ^ [] : [-(in(ordered_pair(3621 ^ [_466481], 3622 ^ [_466481]), _466481))], (3626 ^ _341635) ^ [] : [-(in(ordered_pair(3622 ^ [_466481], 3621 ^ [_466481]), _466481))], (3628 ^ _341635) ^ [] : [3621 ^ [_466481] = 3622 ^ [_466481]]], -(antisymmetric(_466481))], (3606 ^ _341635) ^ [] : [antisymmetric(_466481), 3609 ^ _341635 : [(3610 ^ _341635) ^ [_466751, _466753] : [-(_466753 = _466751), in(ordered_pair(_466753, _466751), _466481), in(ordered_pair(_466751, _466753), _466481)]]]]], (3632 ^ _341635) ^ [_467531, _467533, _467535] : [subset(_467535, _467533), -(in(_467531, _467535)), -(subset(_467535, set_difference(_467533, singleton(_467531))))], (3642 ^ _341635) ^ [_467837] : [relation(_467837), 3645 ^ _341635 : [(3668 ^ _341635) ^ [] : [3671 ^ _341635 : [(3672 ^ _341635) ^ [] : [-(in(3669 ^ [_467837], relation_field(_467837)))], (3674 ^ _341635) ^ [] : [-(in(3670 ^ [_467837], relation_field(_467837)))], (3676 ^ _341635) ^ [] : [3669 ^ [_467837] = 3670 ^ [_467837]], (3678 ^ _341635) ^ [] : [in(ordered_pair(3669 ^ [_467837], 3670 ^ [_467837]), _467837)], (3680 ^ _341635) ^ [] : [in(ordered_pair(3670 ^ [_467837], 3669 ^ [_467837]), _467837)]], -(connected(_467837))], (3646 ^ _341635) ^ [] : [connected(_467837), 3649 ^ _341635 : [(3650 ^ _341635) ^ [_468131, _468133] : [in(_468133, relation_field(_467837)), in(_468131, relation_field(_467837)), -(_468133 = _468131), -(in(ordered_pair(_468133, _468131), _467837)), -(in(ordered_pair(_468131, _468133), _467837))]]]]], (3694 ^ _341635) ^ [_469583, _469585] : [3695 ^ _341635 : [(3696 ^ _341635) ^ [] : [_469585 = empty_set], (3698 ^ _341635) ^ [] : [_469585 = singleton(_469583)]], -(subset(_469585, singleton(_469583)))], (3684 ^ _341635) ^ [_469323, _469325] : [subset(_469325, singleton(_469323)), -(_469325 = empty_set), -(_469325 = singleton(_469323))], (3702 ^ _341635) ^ [_469877, _469879] : [in(_469879, _469877), -(subset(_469879, union(_469877)))], (3708 ^ _341635) ^ [_470148, _470150, _470152, _470154] : [in(ordered_pair(_470154, _470152), cartesian_product2(_470150, _470148)), 3711 ^ _341635 : [(3712 ^ _341635) ^ [] : [-(in(_470154, _470150))], (3714 ^ _341635) ^ [] : [-(in(_470152, _470148))]]], (3716 ^ _341635) ^ [_470413, _470415, _470417, _470419] : [-(in(ordered_pair(_470419, _470417), cartesian_product2(_470415, _470413))), in(_470419, _470415), in(_470417, _470413)], (3726 ^ _341635) ^ [_470746, _470748] : [3728 ^ _341635 : [(3729 ^ _341635) ^ [] : [-(in(3727 ^ [_470746, _470748], _470748))], (3731 ^ _341635) ^ [] : [in(3727 ^ [_470746, _470748], _470746)]], -(element(_470748, powerset(_470746)))], (3735 ^ _341635) ^ [_471119, _471121, _471123] : [relation(_471119), function(_471119), 3742 ^ _341635 : [(3743 ^ _341635) ^ [] : [in(_471121, relation_dom(relation_dom_restriction(_471119, _471123))), 3746 ^ _341635 : [(3747 ^ _341635) ^ [] : [-(in(_471121, relation_dom(_471119)))], (3749 ^ _341635) ^ [] : [-(in(_471121, _471123))]]], (3751 ^ _341635) ^ [] : [-(in(_471121, relation_dom(relation_dom_restriction(_471119, _471123)))), in(_471121, relation_dom(_471119)), in(_471121, _471123)]]], (3762 ^ _341635) ^ [] : [-(relation(3760 ^ []))], (3764 ^ _341635) ^ [] : [-(function(3760 ^ []))], (3767 ^ _341635) ^ [] : [-(epsilon_transitive(3765 ^ []))], (3769 ^ _341635) ^ [] : [-(epsilon_connected(3765 ^ []))], (3771 ^ _341635) ^ [] : [-(ordinal(3765 ^ []))], (3774 ^ _341635) ^ [] : [-(empty(3772 ^ []))], (3776 ^ _341635) ^ [] : [-(relation(3772 ^ []))], (3778 ^ _341635) ^ [_472364] : [-(empty(_472364)), 3782 ^ _341635 : [(3783 ^ _341635) ^ [] : [-(element(3781 ^ [_472364], powerset(_472364)))], (3785 ^ _341635) ^ [] : [empty(3781 ^ [_472364])]]], (3788 ^ _341635) ^ [] : [-(empty(3786 ^ []))], (3791 ^ _341635) ^ [] : [-(relation(3789 ^ []))], (3793 ^ _341635) ^ [] : [-(empty(3789 ^ []))], (3795 ^ _341635) ^ [] : [-(function(3789 ^ []))], (3798 ^ _341635) ^ [] : [-(relation(3796 ^ []))], (3800 ^ _341635) ^ [] : [-(function(3796 ^ []))], (3802 ^ _341635) ^ [] : [-(one_to_one(3796 ^ []))], (3804 ^ _341635) ^ [] : [-(empty(3796 ^ []))], (3806 ^ _341635) ^ [] : [-(epsilon_transitive(3796 ^ []))], (3808 ^ _341635) ^ [] : [-(epsilon_connected(3796 ^ []))], (3810 ^ _341635) ^ [] : [-(ordinal(3796 ^ []))], (3813 ^ _341635) ^ [] : [empty(3811 ^ [])], (3815 ^ _341635) ^ [] : [-(relation(3811 ^ []))], (3818 ^ _341635) ^ [_473644] : [-(element(3816 ^ [_473644], powerset(_473644)))], (3820 ^ _341635) ^ [_473695] : [-(empty(3816 ^ [_473695]))], (3823 ^ _341635) ^ [] : [empty(3821 ^ [])], (3826 ^ _341635) ^ [] : [-(relation(3824 ^ []))], (3828 ^ _341635) ^ [] : [-(function(3824 ^ []))], (3830 ^ _341635) ^ [] : [-(one_to_one(3824 ^ []))], (3833 ^ _341635) ^ [] : [empty(3831 ^ [])], (3835 ^ _341635) ^ [] : [-(epsilon_transitive(3831 ^ []))], (3837 ^ _341635) ^ [] : [-(epsilon_connected(3831 ^ []))], (3839 ^ _341635) ^ [] : [-(ordinal(3831 ^ []))], (3842 ^ _341635) ^ [] : [-(relation(3840 ^ []))], (3844 ^ _341635) ^ [] : [-(relation_empty_yielding(3840 ^ []))], (3847 ^ _341635) ^ [] : [-(relation(3845 ^ []))], (3849 ^ _341635) ^ [] : [-(relation_empty_yielding(3845 ^ []))], (3851 ^ _341635) ^ [] : [-(function(3845 ^ []))], (3853 ^ _341635) ^ [_474749, _474751, _474753] : [relation_of2(_474749, _474753, _474751), -(relation_dom_as_subset(_474753, _474751, _474749) = relation_dom(_474749))], (3859 ^ _341635) ^ [_474993, _474995, _474997] : [relation_of2(_474993, _474997, _474995), -(relation_rng_as_subset(_474997, _474995, _474993) = relation_rng(_474993))], (3865 ^ _341635) ^ [_475223, _475225] : [element(_475223, powerset(powerset(_475225))), -(union_of_subsets(_475225, _475223) = union(_475223))], (3871 ^ _341635) ^ [_475451, _475453] : [element(_475451, powerset(powerset(_475453))), -(meet_of_subsets(_475453, _475451) = set_meet(_475451))], (3877 ^ _341635) ^ [_475693, _475695, _475697] : [-(subset_difference(_475697, _475695, _475693) = set_difference(_475695, _475693)), element(_475695, powerset(_475697)), element(_475693, powerset(_475697))], (3887 ^ _341635) ^ [_476067, _476069, _476071] : [relation_of2_as_subset(_476067, _476071, _476069), -(relation_of2(_476067, _476071, _476069))], (3893 ^ _341635) ^ [_476239, _476241, _476243] : [relation_of2(_476239, _476243, _476241), -(relation_of2_as_subset(_476239, _476243, _476241))], (3899 ^ _341635) ^ [_476461, _476463] : [ordinal(_476463), ordinal(_476461), 3906 ^ _341635 : [(3907 ^ _341635) ^ [] : [ordinal_subset(_476463, _476461), -(subset(_476463, _476461))], (3913 ^ _341635) ^ [] : [subset(_476463, _476461), -(ordinal_subset(_476463, _476461))]]], (3919 ^ _341635) ^ [_477008, _477010] : [-(ordinal_subset(_477010, _477010)), ordinal(_477010), ordinal(_477008)], (3929 ^ _341635) ^ [_477288, _477290] : [-(subset(_477290, _477290))], (3931 ^ _341635) ^ [_477383] : [3932 ^ _341635 : [(3933 ^ _341635) ^ [_477504] : [ordinal(_477504), in(_477504, _477383)]], 3939 ^ _341635 : [(3940 ^ _341635) ^ [] : [-(ordinal(3938 ^ [_477383]))], (3942 ^ _341635) ^ [] : [-(in(3938 ^ [_477383], _477383))], (3944 ^ _341635) ^ [_477884] : [ordinal(_477884), in(_477884, _477383), -(ordinal_subset(3938 ^ [_477383], _477884))]]], (3954 ^ _341635) ^ [_478203, _478205] : [ordinal(_478203), 3962 ^ _341635 : [(3963 ^ _341635) ^ [] : [-(3959 ^ [_478203, _478205] = 3960 ^ [_478203, _478205])], (3966 ^ _341635) ^ [] : [-(ordinal(3964 ^ [_478203, _478205]))], (3968 ^ _341635) ^ [] : [-(3960 ^ [_478203, _478205] = 3964 ^ [_478203, _478205])], (3970 ^ _341635) ^ [] : [-(in(3964 ^ [_478203, _478205], _478205))], (3972 ^ _341635) ^ [] : [-(3959 ^ [_478203, _478205] = 3961 ^ [_478203, _478205])], (3975 ^ _341635) ^ [] : [-(ordinal(3973 ^ [_478203, _478205]))], (3977 ^ _341635) ^ [] : [-(3961 ^ [_478203, _478205] = 3973 ^ [_478203, _478205])], (3979 ^ _341635) ^ [] : [-(in(3973 ^ [_478203, _478205], _478205))], (3981 ^ _341635) ^ [] : [3960 ^ [_478203, _478205] = 3961 ^ [_478203, _478205]]], 3983 ^ _341635 : [(3984 ^ _341635) ^ [_479805] : [in(_479805, 3982 ^ [_478203, _478205]), 3988 ^ _341635 : [(3989 ^ _341635) ^ [] : [-(in(3987 ^ [_478203, _478205, _479805], succ(_478203)))], (3991 ^ _341635) ^ [] : [-(3987 ^ [_478203, _478205, _479805] = _479805)], (3994 ^ _341635) ^ [] : [-(ordinal(3992 ^ [_478203, _478205, _479805]))], (3996 ^ _341635) ^ [] : [-(_479805 = 3992 ^ [_478203, _478205, _479805])], (3998 ^ _341635) ^ [] : [-(in(3992 ^ [_478203, _478205, _479805], _478205))]]], (4000 ^ _341635) ^ [_480492] : [-(in(_480492, 3982 ^ [_478203, _478205])), 4001 ^ _341635 : [(4002 ^ _341635) ^ [_480621] : [in(_480621, succ(_478203)), _480621 = _480492, 4009 ^ _341635 : [(4010 ^ _341635) ^ [_480874] : [ordinal(_480874), _480492 = _480874, in(_480874, _478205)]]]]]]], (4022 ^ _341635) ^ [_481289, _481291] : [ordinal(_481289), 4026 ^ _341635 : [(4027 ^ _341635) ^ [_481562] : [in(_481562, 4025 ^ [_481289, _481291]), 4030 ^ _341635 : [(4031 ^ _341635) ^ [] : [-(in(_481562, succ(_481289)))], (4034 ^ _341635) ^ [] : [-(ordinal(4032 ^ [_481289, _481291, _481562]))], (4036 ^ _341635) ^ [] : [-(_481562 = 4032 ^ [_481289, _481291, _481562])], (4038 ^ _341635) ^ [] : [-(in(4032 ^ [_481289, _481291, _481562], _481291))]]], (4040 ^ _341635) ^ [_482071] : [-(in(_482071, 4025 ^ [_481289, _481291])), in(_482071, succ(_481289)), 4045 ^ _341635 : [(4046 ^ _341635) ^ [_482274] : [ordinal(_482274), _482071 = _482274, in(_482274, _481291)]]]]], (4058 ^ _341635) ^ [_482667, _482669] : [disjoint(_482669, _482667), -(disjoint(_482667, _482669))], (4064 ^ _341635) ^ [_482934, _482936, _482938, _482940] : [in(ordered_pair(_482940, _482938), cartesian_product2(_482936, _482934)), 4067 ^ _341635 : [(4068 ^ _341635) ^ [] : [-(in(_482940, _482936))], (4070 ^ _341635) ^ [] : [-(in(_482938, _482934))]]], (4072 ^ _341635) ^ [_483199, _483201, _483203, _483205] : [-(in(ordered_pair(_483205, _483203), cartesian_product2(_483201, _483199))), in(_483205, _483201), in(_483203, _483199)], (4082 ^ _341635) ^ [_483503] : [-(in(_483503, succ(_483503)))], (4084 ^ _341635) ^ [_483640, _483642, _483644, _483646] : [unordered_pair(_483646, _483644) = unordered_pair(_483642, _483640), -(_483646 = _483642), -(_483646 = _483640)], (4094 ^ _341635) ^ [_483990, _483992, _483994] : [relation(_483990), 4097 ^ _341635 : [(4098 ^ _341635) ^ [] : [in(_483994, relation_rng(relation_rng_restriction(_483992, _483990))), 4101 ^ _341635 : [(4102 ^ _341635) ^ [] : [-(in(_483994, _483992))], (4104 ^ _341635) ^ [] : [-(in(_483994, relation_rng(_483990)))]]], (4106 ^ _341635) ^ [] : [-(in(_483994, relation_rng(relation_rng_restriction(_483992, _483990)))), in(_483994, _483992), in(_483994, relation_rng(_483990))]]], (4116 ^ _341635) ^ [_484649, _484651] : [relation(_484649), -(subset(relation_rng(relation_rng_restriction(_484651, _484649)), _484651))], (4122 ^ _341635) ^ [_484867, _484869] : [relation(_484867), -(subset(relation_rng_restriction(_484869, _484867), _484867))], (4128 ^ _341635) ^ [_485081, _485083] : [relation(_485081), -(subset(relation_rng(relation_rng_restriction(_485083, _485081)), relation_rng(_485081)))], (4134 ^ _341635) ^ [_485317, _485319, _485321] : [subset(_485321, _485319), 4137 ^ _341635 : [(4138 ^ _341635) ^ [] : [-(subset(cartesian_product2(_485321, _485317), cartesian_product2(_485319, _485317)))], (4140 ^ _341635) ^ [] : [-(subset(cartesian_product2(_485317, _485321), cartesian_product2(_485317, _485319)))]]], (4142 ^ _341635) ^ [_485634, _485636] : [relation(_485634), -(relation_rng(relation_rng_restriction(_485636, _485634)) = set_intersection2(relation_rng(_485634), _485636))], (4148 ^ _341635) ^ [_485890, _485892, _485894, _485896] : [-(subset(cartesian_product2(_485896, _485892), cartesian_product2(_485894, _485890))), subset(_485896, _485894), subset(_485892, _485890)], (4158 ^ _341635) ^ [_486235, _486237, _486239] : [relation_of2_as_subset(_486235, _486239, _486237), 4161 ^ _341635 : [(4162 ^ _341635) ^ [] : [-(subset(relation_dom(_486235), _486239))], (4164 ^ _341635) ^ [] : [-(subset(relation_rng(_486235), _486237))]]], (4166 ^ _341635) ^ [_486538, _486540] : [subset(_486540, _486538), -(set_union2(_486540, _486538) = _486538)], (4173 ^ _341635) ^ [_486860] : [-(in(_486860, 4171 ^ [_486860]))], (4175 ^ _341635) ^ [_486972, _486974, _486976] : [-(in(_486972, 4171 ^ [_486976])), in(_486974, 4171 ^ [_486976]), subset(_486972, _486974)], (4185 ^ _341635) ^ [_487287, _487289] : [in(_487287, 4171 ^ [_487289]), -(in(powerset(_487287), 4171 ^ [_487289]))], (4191 ^ _341635) ^ [_487487, _487489] : [subset(_487487, 4171 ^ [_487489]), -(are_equipotent(_487487, 4171 ^ [_487489])), -(in(_487487, 4171 ^ [_487489]))], (4201 ^ _341635) ^ [_487841, _487843, _487845] : [relation(_487841), -(relation_dom_restriction(relation_rng_restriction(_487845, _487841), _487843) = relation_rng_restriction(_487845, relation_dom_restriction(_487841, _487843)))], (4207 ^ _341635) ^ [_488093, _488095, _488097] : [relation(_488093), 4210 ^ _341635 : [(4211 ^ _341635) ^ [] : [in(_488097, relation_image(_488093, _488095)), 4215 ^ _341635 : [(4216 ^ _341635) ^ [] : [-(in(4214 ^ [_488093, _488095, _488097], relation_dom(_488093)))], (4218 ^ _341635) ^ [] : [-(in(ordered_pair(4214 ^ [_488093, _488095, _488097], _488097), _488093))], (4220 ^ _341635) ^ [] : [-(in(4214 ^ [_488093, _488095, _488097], _488095))]]], (4222 ^ _341635) ^ [] : [-(in(_488097, relation_image(_488093, _488095))), 4223 ^ _341635 : [(4224 ^ _341635) ^ [_488694] : [in(_488694, relation_dom(_488093)), in(ordered_pair(_488694, _488097), _488093), in(_488694, _488095)]]]]], (4236 ^ _341635) ^ [_489091, _489093] : [relation(_489091), -(subset(relation_image(_489091, _489093), relation_rng(_489091)))], (4242 ^ _341635) ^ [_489309, _489311] : [-(subset(relation_image(_489309, relation_inverse_image(_489309, _489311)), _489311)), relation(_489309), function(_489309)], (4252 ^ _341635) ^ [_489616, _489618] : [relation(_489616), -(relation_image(_489616, _489618) = relation_image(_489616, set_intersection2(relation_dom(_489616), _489618)))], (4258 ^ _341635) ^ [_489846, _489848] : [relation(_489846), subset(_489848, relation_dom(_489846)), -(subset(_489848, relation_inverse_image(_489846, relation_image(_489846, _489848))))], (4268 ^ _341635) ^ [_490145] : [relation(_490145), -(relation_image(_490145, relation_dom(_490145)) = relation_rng(_490145))], (4274 ^ _341635) ^ [_490361, _490363] : [relation(_490361), function(_490361), subset(_490363, relation_rng(_490361)), -(relation_image(_490361, relation_inverse_image(_490361, _490363)) = _490363)], (4288 ^ _341635) ^ [_490791, _490793, _490795, _490797] : [relation_of2_as_subset(_490791, _490793, _490797), subset(relation_rng(_490791), _490795), -(relation_of2_as_subset(_490791, _490793, _490795))], (4298 ^ _341635) ^ [_491104] : [relation(_491104), 4301 ^ _341635 : [(4302 ^ _341635) ^ [_491244] : [relation(_491244), -(relation_rng(relation_composition(_491104, _491244)) = relation_image(_491244, relation_rng(_491104)))]]], (4308 ^ _341635) ^ [_491493, _491495, _491497] : [relation(_491493), 4311 ^ _341635 : [(4312 ^ _341635) ^ [] : [in(_491497, relation_inverse_image(_491493, _491495)), 4316 ^ _341635 : [(4317 ^ _341635) ^ [] : [-(in(4315 ^ [_491493, _491495, _491497], relation_rng(_491493)))], (4319 ^ _341635) ^ [] : [-(in(ordered_pair(_491497, 4315 ^ [_491493, _491495, _491497]), _491493))], (4321 ^ _341635) ^ [] : [-(in(4315 ^ [_491493, _491495, _491497], _491495))]]], (4323 ^ _341635) ^ [] : [-(in(_491497, relation_inverse_image(_491493, _491495))), 4324 ^ _341635 : [(4325 ^ _341635) ^ [_492094] : [in(_492094, relation_rng(_491493)), in(ordered_pair(_491497, _492094), _491493), in(_492094, _491495)]]]]], (4337 ^ _341635) ^ [_492491, _492493] : [relation(_492491), -(subset(relation_inverse_image(_492491, _492493), relation_dom(_492491)))], (4343 ^ _341635) ^ [_492737, _492739, _492741, _492743] : [relation_of2_as_subset(_492737, _492739, _492743), subset(_492743, _492741), -(relation_of2_as_subset(_492737, _492739, _492741))], (4353 ^ _341635) ^ [_493074, _493076, _493078] : [relation(_493074), 4356 ^ _341635 : [(4357 ^ _341635) ^ [] : [in(_493078, relation_restriction(_493074, _493076)), 4360 ^ _341635 : [(4361 ^ _341635) ^ [] : [-(in(_493078, _493074))], (4363 ^ _341635) ^ [] : [-(in(_493078, cartesian_product2(_493076, _493076)))]]], (4365 ^ _341635) ^ [] : [-(in(_493078, relation_restriction(_493074, _493076))), in(_493078, _493074), in(_493078, cartesian_product2(_493076, _493076))]]], (4375 ^ _341635) ^ [_493730, _493732] : [relation(_493730), -(_493732 = empty_set), subset(_493732, relation_rng(_493730)), relation_inverse_image(_493730, _493732) = empty_set], (4389 ^ _341635) ^ [_494144, _494146, _494148] : [relation(_494144), subset(_494148, _494146), -(subset(relation_inverse_image(_494144, _494148), relation_inverse_image(_494144, _494146)))], (4399 ^ _341635) ^ [_494463, _494465] : [relation(_494463), -(relation_restriction(_494463, _494465) = relation_dom_restriction(relation_rng_restriction(_494465, _494463), _494465))], (4405 ^ _341635) ^ [_494674, _494676] : [-(subset(set_intersection2(_494676, _494674), _494676))], (4407 ^ _341635) ^ [_494786, _494788] : [relation(_494786), -(relation_restriction(_494786, _494788) = relation_rng_restriction(_494788, relation_dom_restriction(_494786, _494788)))], (4413 ^ _341635) ^ [_495026, _495028, _495030] : [relation(_495026), in(_495030, relation_field(relation_restriction(_495026, _495028))), 4420 ^ _341635 : [(4421 ^ _341635) ^ [] : [-(in(_495030, relation_field(_495026)))], (4423 ^ _341635) ^ [] : [-(in(_495030, _495028))]]], (4425 ^ _341635) ^ [_495438, _495440, _495442] : [-(subset(_495442, set_intersection2(_495440, _495438))), subset(_495442, _495440), subset(_495442, _495438)], (4435 ^ _341635) ^ [_495724] : [-(set_union2(_495724, empty_set) = _495724)], (4437 ^ _341635) ^ [_495834, _495836] : [in(_495836, _495834), -(element(_495836, _495834))], (4443 ^ _341635) ^ [_496058, _496060, _496062] : [-(subset(_496062, _496058)), subset(_496062, _496060), subset(_496060, _496058)], (4453 ^ _341635) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (4455 ^ _341635) ^ [_496434, _496436, _496438] : [relation(_496434), in(ordered_pair(_496438, _496436), _496434), 4462 ^ _341635 : [(4463 ^ _341635) ^ [] : [-(in(_496438, relation_dom(_496434)))], (4465 ^ _341635) ^ [] : [-(in(_496436, relation_rng(_496434)))]]], (4467 ^ _341635) ^ [_496832, _496834] : [relation(_496832), 4470 ^ _341635 : [(4471 ^ _341635) ^ [] : [-(subset(relation_field(relation_restriction(_496832, _496834)), relation_field(_496832)))], (4473 ^ _341635) ^ [] : [-(subset(relation_field(relation_restriction(_496832, _496834)), _496834))]]], (4475 ^ _341635) ^ [_497139, _497141] : [relation(_497139), function(_497139), 4482 ^ _341635 : [(4483 ^ _341635) ^ [_497389] : [relation(_497389), function(_497389), 4490 ^ _341635 : [(4491 ^ _341635) ^ [] : [in(_497141, relation_dom(relation_composition(_497389, _497139))), 4494 ^ _341635 : [(4495 ^ _341635) ^ [] : [-(in(_497141, relation_dom(_497389)))], (4497 ^ _341635) ^ [] : [-(in(apply(_497389, _497141), relation_dom(_497139)))]]], (4499 ^ _341635) ^ [] : [-(in(_497141, relation_dom(relation_composition(_497389, _497139)))), in(_497141, relation_dom(_497389)), in(apply(_497389, _497141), relation_dom(_497139))]]]]], (4509 ^ _341635) ^ [_498153] : [epsilon_transitive(_498153), 4512 ^ _341635 : [(4513 ^ _341635) ^ [_498289] : [ordinal(_498289), proper_subset(_498153, _498289), -(in(_498153, _498289))]]], (4523 ^ _341635) ^ [_498579] : [relation(_498579), -(subset(_498579, cartesian_product2(relation_dom(_498579), relation_rng(_498579))))], (4529 ^ _341635) ^ [_498809, _498811, _498813] : [relation(_498809), -(subset(fiber(relation_restriction(_498809, _498813), _498811), fiber(_498809, _498811)))], (4535 ^ _341635) ^ [_499041, _499043] : [relation(_499041), function(_499041), 4542 ^ _341635 : [(4543 ^ _341635) ^ [_499290] : [relation(_499290), function(_499290), in(_499043, relation_dom(relation_composition(_499290, _499041))), -(apply(relation_composition(_499290, _499041), _499043) = apply(_499041, apply(_499290, _499043)))]]], (4557 ^ _341635) ^ [_499749, _499751, _499753] : [relation_of2_as_subset(_499749, _499751, _499753), 4560 ^ _341635 : [(4561 ^ _341635) ^ [] : [4563 ^ _341635 : [(4564 ^ _341635) ^ [] : [-(in(4562 ^ [_499749, _499751, _499753], _499751))], (4566 ^ _341635) ^ [_500107] : [in(ordered_pair(4562 ^ [_499749, _499751, _499753], _500107), _499749)]], -(relation_dom_as_subset(_499751, _499753, _499749) = _499751)], (4570 ^ _341635) ^ [] : [relation_dom_as_subset(_499751, _499753, _499749) = _499751, 4573 ^ _341635 : [(4574 ^ _341635) ^ [_500344] : [in(_500344, _499751), -(in(ordered_pair(_500344, 4577 ^ [_499749, _499751, _499753, _500344]), _499749))]]]]], (4581 ^ _341635) ^ [_500666, _500668] : [relation(_500666), reflexive(_500666), -(reflexive(relation_restriction(_500666, _500668)))], (4591 ^ _341635) ^ [_500965, _500967] : [relation(_500965), function(_500965), 4598 ^ _341635 : [(4599 ^ _341635) ^ [_501211] : [relation(_501211), function(_501211), in(_500967, relation_dom(_500965)), -(apply(relation_composition(_500965, _501211), _500967) = apply(_501211, apply(_500965, _500967)))]]], (4613 ^ _341635) ^ [_501650, _501652] : [ordinal(_501650), in(_501652, _501650), -(ordinal(_501652))], (4623 ^ _341635) ^ [_501959, _501961, _501963] : [relation_of2_as_subset(_501959, _501963, _501961), 4626 ^ _341635 : [(4627 ^ _341635) ^ [] : [4629 ^ _341635 : [(4630 ^ _341635) ^ [] : [-(in(4628 ^ [_501959, _501961, _501963], _501961))], (4632 ^ _341635) ^ [_502317] : [in(ordered_pair(_502317, 4628 ^ [_501959, _501961, _501963]), _501959)]], -(relation_rng_as_subset(_501963, _501961, _501959) = _501961)], (4636 ^ _341635) ^ [] : [relation_rng_as_subset(_501963, _501961, _501959) = _501961, 4639 ^ _341635 : [(4640 ^ _341635) ^ [_502554] : [in(_502554, _501961), -(in(ordered_pair(4643 ^ [_501959, _501961, _501963, _502554], _502554), _501959))]]]]], (4647 ^ _341635) ^ [_502876, _502878] : [relation(_502876), connected(_502876), -(connected(relation_restriction(_502876, _502878)))], (4657 ^ _341635) ^ [_503161] : [ordinal(_503161), 4660 ^ _341635 : [(4661 ^ _341635) ^ [_503311] : [ordinal(_503311), -(in(_503161, _503311)), -(_503161 = _503311), -(in(_503311, _503161))]]], (4675 ^ _341635) ^ [_503714, _503716] : [relation(_503714), transitive(_503714), -(transitive(relation_restriction(_503714, _503716)))], (4685 ^ _341635) ^ [_503999] : [relation(_503999), 4688 ^ _341635 : [(4689 ^ _341635) ^ [_504149] : [relation(_504149), subset(_503999, _504149), 4696 ^ _341635 : [(4697 ^ _341635) ^ [] : [-(subset(relation_dom(_503999), relation_dom(_504149)))], (4699 ^ _341635) ^ [] : [-(subset(relation_rng(_503999), relation_rng(_504149)))]]]]], (4701 ^ _341635) ^ [_504544, _504546] : [relation(_504544), antisymmetric(_504544), -(antisymmetric(relation_restriction(_504544, _504546)))], (4711 ^ _341635) ^ [_504857, _504859, _504861] : [subset(_504861, _504859), -(subset(set_intersection2(_504861, _504857), set_intersection2(_504859, _504857)))], (4717 ^ _341635) ^ [_505085, _505087] : [subset(_505087, _505085), -(set_intersection2(_505087, _505085) = _505087)], (4723 ^ _341635) ^ [_505272] : [-(set_intersection2(_505272, empty_set) = empty_set)], (4725 ^ _341635) ^ [_505382, _505384] : [element(_505384, _505382), -(empty(_505382)), -(in(_505384, _505382))], (4735 ^ _341635) ^ [_505680, _505682] : [-(_505682 = _505680), 4739 ^ _341635 : [(4740 ^ _341635) ^ [] : [-(in(4736 ^ [_505680, _505682], _505682))], (4742 ^ _341635) ^ [] : [in(4736 ^ [_505680, _505682], _505680)]], 4743 ^ _341635 : [(4744 ^ _341635) ^ [] : [-(in(4736 ^ [_505680, _505682], _505680))], (4746 ^ _341635) ^ [] : [in(4736 ^ [_505680, _505682], _505682)]]], (4750 ^ _341635) ^ [_506181] : [-(reflexive(inclusion_relation(_506181)))], (4752 ^ _341635) ^ [_506260] : [-(subset(empty_set, _506260))], (4754 ^ _341635) ^ [_506381, _506383, _506385] : [relation(_506381), in(ordered_pair(_506385, _506383), _506381), 4761 ^ _341635 : [(4762 ^ _341635) ^ [] : [-(in(_506385, relation_field(_506381)))], (4764 ^ _341635) ^ [] : [-(in(_506383, relation_field(_506381)))]]], (4766 ^ _341635) ^ [_506765] : [-(ordinal(_506765)), 4768 ^ _341635 : [(4769 ^ _341635) ^ [] : [-(in(4767 ^ [_506765], _506765))], (4771 ^ _341635) ^ [] : [ordinal(4767 ^ [_506765]), subset(4767 ^ [_506765], _506765)]]], (4779 ^ _341635) ^ [_507195, _507197] : [relation(_507195), well_founded_relation(_507195), -(well_founded_relation(relation_restriction(_507195, _507197)))], (4789 ^ _341635) ^ [_507494, _507496] : [ordinal(_507494), subset(_507496, _507494), -(_507496 = empty_set), 4801 ^ _341635 : [(4802 ^ _341635) ^ [] : [-(ordinal(4800 ^ [_507494, _507496]))], (4804 ^ _341635) ^ [] : [-(in(4800 ^ [_507494, _507496], _507496))], (4806 ^ _341635) ^ [_508046] : [ordinal(_508046), in(_508046, _507496), -(ordinal_subset(4800 ^ [_507494, _507496], _508046))]]], (4816 ^ _341635) ^ [_508388, _508390] : [relation(_508388), well_ordering(_508388), -(well_ordering(relation_restriction(_508388, _508390)))], (4826 ^ _341635) ^ [_508673] : [ordinal(_508673), 4829 ^ _341635 : [(4830 ^ _341635) ^ [_508811] : [ordinal(_508811), 4833 ^ _341635 : [(4834 ^ _341635) ^ [] : [in(_508673, _508811), -(ordinal_subset(succ(_508673), _508811))], (4840 ^ _341635) ^ [] : [ordinal_subset(succ(_508673), _508811), -(in(_508673, _508811))]]]]], (4846 ^ _341635) ^ [_509296, _509298, _509300] : [subset(_509300, _509298), -(subset(set_difference(_509300, _509296), set_difference(_509298, _509296)))], (4852 ^ _341635) ^ [_509552, _509554, _509556, _509558] : [ordered_pair(_509558, _509556) = ordered_pair(_509554, _509552), 4855 ^ _341635 : [(4856 ^ _341635) ^ [] : [-(_509558 = _509554)], (4858 ^ _341635) ^ [] : [-(_509556 = _509552)]]], (4860 ^ _341635) ^ [_509865, _509867] : [relation(_509865), function(_509865), 4867 ^ _341635 : [(4868 ^ _341635) ^ [] : [_509865 = identity_relation(_509867), 4871 ^ _341635 : [(4872 ^ _341635) ^ [] : [-(relation_dom(_509865) = _509867)], (4874 ^ _341635) ^ [_510284] : [in(_510284, _509867), -(apply(_509865, _510284) = _510284)]]], (4880 ^ _341635) ^ [] : [-(_509865 = identity_relation(_509867)), relation_dom(_509865) = _509867, 4886 ^ _341635 : [(4887 ^ _341635) ^ [] : [-(in(4885 ^ [_509865, _509867], _509867))], (4889 ^ _341635) ^ [] : [apply(_509865, 4885 ^ [_509865, _509867]) = 4885 ^ [_509865, _509867]]]]]], (4893 ^ _341635) ^ [_510889, _510891] : [in(_510889, _510891), -(apply(identity_relation(_510891), _510889) = _510889)], (4899 ^ _341635) ^ [_511094, _511096] : [-(subset(set_difference(_511096, _511094), _511096))], (4901 ^ _341635) ^ [_511192] : [relation(_511192), 4904 ^ _341635 : [(4905 ^ _341635) ^ [] : [-(relation_rng(_511192) = relation_dom(relation_inverse(_511192)))], (4907 ^ _341635) ^ [] : [-(relation_dom(_511192) = relation_rng(relation_inverse(_511192)))]]], (4909 ^ _341635) ^ [_511520, _511522] : [set_difference(_511522, _511520) = empty_set, -(subset(_511522, _511520))], (4915 ^ _341635) ^ [_511688, _511690] : [subset(_511690, _511688), -(set_difference(_511690, _511688) = empty_set)], (4921 ^ _341635) ^ [_511935, _511937] : [subset(singleton(_511937), _511935), -(in(_511937, _511935))], (4927 ^ _341635) ^ [_512101, _512103] : [in(_512103, _512101), -(subset(singleton(_512103), _512101))], (4933 ^ _341635) ^ [_512360, _512362, _512364] : [subset(unordered_pair(_512364, _512362), _512360), 4936 ^ _341635 : [(4937 ^ _341635) ^ [] : [-(in(_512364, _512360))], (4939 ^ _341635) ^ [] : [-(in(_512362, _512360))]]], (4941 ^ _341635) ^ [_512611, _512613, _512615] : [-(subset(unordered_pair(_512615, _512613), _512611)), in(_512615, _512611), in(_512613, _512611)], (4951 ^ _341635) ^ [_512928, _512930] : [relation(_512928), -(relation_field(relation_restriction(_512928, _512930)) = _512930), well_ordering(_512928), subset(_512930, relation_field(_512928))], (4965 ^ _341635) ^ [_513311, _513313] : [-(set_union2(_513313, set_difference(_513311, _513313)) = set_union2(_513313, _513311))], (4977 ^ _341635) ^ [_513718, _513720] : [4978 ^ _341635 : [(4979 ^ _341635) ^ [] : [_513720 = empty_set], (4981 ^ _341635) ^ [] : [_513720 = singleton(_513718)]], -(subset(_513720, singleton(_513718)))], (4967 ^ _341635) ^ [_513458, _513460] : [subset(_513460, singleton(_513458)), -(_513460 = empty_set), -(_513460 = singleton(_513458))], (4985 ^ _341635) ^ [_513983] : [-(set_difference(_513983, empty_set) = _513983)], (4987 ^ _341635) ^ [_514107, _514109, _514111] : [in(_514111, _514109), in(_514109, _514107), in(_514107, _514111)], (4997 ^ _341635) ^ [_514444, _514446] : [element(_514446, powerset(_514444)), -(subset(_514446, _514444))], (5003 ^ _341635) ^ [_514610, _514612] : [subset(_514612, _514610), -(element(_514612, powerset(_514610)))], (5009 ^ _341635) ^ [_514797] : [-(transitive(inclusion_relation(_514797)))], (5011 ^ _341635) ^ [_514925, _514927] : [-(disjoint(_514927, _514925)), 5015 ^ _341635 : [(5016 ^ _341635) ^ [] : [-(in(5014 ^ [_514925, _514927], _514927))], (5018 ^ _341635) ^ [] : [-(in(5014 ^ [_514925, _514927], _514925))]]], (5020 ^ _341635) ^ [_515239, _515241] : [disjoint(_515241, _515239), 5021 ^ _341635 : [(5022 ^ _341635) ^ [_515331] : [in(_515331, _515241), in(_515331, _515239)]]], (5030 ^ _341635) ^ [_515588] : [subset(_515588, empty_set), -(_515588 = empty_set)], (5036 ^ _341635) ^ [_515777, _515779] : [-(set_difference(set_union2(_515779, _515777), _515777) = set_difference(_515779, _515777))], (5038 ^ _341635) ^ [_515881] : [ordinal(_515881), 5041 ^ _341635 : [(5056 ^ _341635) ^ [] : [5058 ^ _341635 : [(5059 ^ _341635) ^ [] : [-(ordinal(5057 ^ [_515881]))], (5061 ^ _341635) ^ [] : [-(in(5057 ^ [_515881], _515881))], (5063 ^ _341635) ^ [] : [in(succ(5057 ^ [_515881]), _515881)]], -(being_limit_ordinal(_515881))], (5042 ^ _341635) ^ [] : [being_limit_ordinal(_515881), 5045 ^ _341635 : [(5046 ^ _341635) ^ [_516127] : [ordinal(_516127), in(_516127, _515881), -(in(succ(_516127), _515881))]]]]], (5067 ^ _341635) ^ [_516753] : [ordinal(_516753), 5070 ^ _341635 : [(5071 ^ _341635) ^ [] : [-(being_limit_ordinal(_516753)), 5075 ^ _341635 : [(5076 ^ _341635) ^ [] : [-(ordinal(5074 ^ [_516753]))], (5078 ^ _341635) ^ [] : [-(_516753 = succ(5074 ^ [_516753]))]]], (5080 ^ _341635) ^ [] : [being_limit_ordinal(_516753), 5081 ^ _341635 : [(5082 ^ _341635) ^ [_517224] : [ordinal(_517224), _516753 = succ(_517224)]]]]], (5090 ^ _341635) ^ [_517491, _517493] : [element(_517491, powerset(_517493)), 5093 ^ _341635 : [(5094 ^ _341635) ^ [_517643] : [element(_517643, powerset(_517493)), 5097 ^ _341635 : [(5098 ^ _341635) ^ [] : [disjoint(_517491, _517643), -(subset(_517491, subset_complement(_517493, _517643)))], (5104 ^ _341635) ^ [] : [subset(_517491, subset_complement(_517493, _517643)), -(disjoint(_517491, _517643))]]]]], (5110 ^ _341635) ^ [_518127] : [relation(_518127), 5113 ^ _341635 : [(5114 ^ _341635) ^ [_518264] : [relation(_518264), -(subset(relation_dom(relation_composition(_518127, _518264)), relation_dom(_518127)))]]], (5120 ^ _341635) ^ [_518479] : [relation(_518479), 5123 ^ _341635 : [(5124 ^ _341635) ^ [_518616] : [relation(_518616), -(subset(relation_rng(relation_composition(_518479, _518616)), relation_rng(_518616)))]]], (5130 ^ _341635) ^ [_518845, _518847] : [subset(_518847, _518845), -(_518845 = set_union2(_518847, set_difference(_518845, _518847)))], (5136 ^ _341635) ^ [_519053] : [relation(_519053), 5139 ^ _341635 : [(5140 ^ _341635) ^ [_519200] : [relation(_519200), subset(relation_rng(_519053), relation_dom(_519200)), -(relation_dom(relation_composition(_519053, _519200)) = relation_dom(_519053))]]], (5150 ^ _341635) ^ [_519526, _519528] : [element(_519526, powerset(powerset(_519528))), -(_519526 = empty_set), complements_of_subsets(_519528, _519526) = empty_set], (5160 ^ _341635) ^ [_519843, _519845] : [in(_519845, _519843), -(set_union2(singleton(_519845), _519843) = _519843)], (5166 ^ _341635) ^ [_520049] : [relation(_520049), 5169 ^ _341635 : [(5170 ^ _341635) ^ [_520196] : [relation(_520196), subset(relation_dom(_520049), relation_rng(_520196)), -(relation_rng(relation_composition(_520196, _520049)) = relation_rng(_520049))]]], (5180 ^ _341635) ^ [_520522, _520524] : [element(_520522, powerset(powerset(_520524))), -(_520522 = empty_set), -(subset_difference(_520524, cast_to_subset(_520524), union_of_subsets(_520524, _520522)) = meet_of_subsets(_520524, complements_of_subsets(_520524, _520522)))], (5190 ^ _341635) ^ [_520862, _520864] : [element(_520862, powerset(powerset(_520864))), -(_520862 = empty_set), -(union_of_subsets(_520864, complements_of_subsets(_520864, _520862)) = subset_difference(_520864, cast_to_subset(_520864), meet_of_subsets(_520864, _520862)))], (5200 ^ _341635) ^ [_521187, _521189] : [-(set_difference(_521189, set_difference(_521189, _521187)) = set_intersection2(_521189, _521187))], (5202 ^ _341635) ^ [_521291] : [relation(_521291), 5205 ^ _341635 : [(5206 ^ _341635) ^ [_521446] : [relation(_521446), 5209 ^ _341635 : [(5210 ^ _341635) ^ [_521597] : [relation(_521597), function(_521597), relation_isomorphism(_521291, _521446, _521597), -(relation_isomorphism(_521446, _521291, function_inverse(_521597)))]]]]], (5224 ^ _341635) ^ [_521990] : [-(set_difference(empty_set, _521990) = empty_set)], (5226 ^ _341635) ^ [_522114, _522116, _522118] : [-(element(_522118, _522114)), in(_522118, _522116), element(_522116, powerset(_522114))], (5236 ^ _341635) ^ [_522413] : [ordinal(_522413), -(connected(inclusion_relation(_522413)))], (5242 ^ _341635) ^ [_522637, _522639] : [-(disjoint(_522639, _522637)), -(in(5245 ^ [_522637, _522639], set_intersection2(_522639, _522637)))], (5249 ^ _341635) ^ [_522872, _522874] : [5250 ^ _341635 : [(5251 ^ _341635) ^ [_522945] : [in(_522945, set_intersection2(_522874, _522872))]], disjoint(_522874, _522872)], (5255 ^ _341635) ^ [_523097] : [-(_523097 = empty_set), 5258 ^ _341635 : [(5259 ^ _341635) ^ [_523257] : [element(_523257, powerset(_523097)), 5262 ^ _341635 : [(5263 ^ _341635) ^ [_523411] : [element(_523411, _523097), -(in(_523411, _523257)), -(in(_523411, subset_complement(_523097, _523257)))]]]]], (5273 ^ _341635) ^ [_523729] : [relation(_523729), 5276 ^ _341635 : [(5277 ^ _341635) ^ [_523925] : [relation(_523925), 5280 ^ _341635 : [(5281 ^ _341635) ^ [_524117] : [relation(_524117), function(_524117), relation_isomorphism(_523729, _523925, _524117), 5292 ^ _341635 : [(5293 ^ _341635) ^ [] : [reflexive(_523729), -(reflexive(_523925))], (5299 ^ _341635) ^ [] : [transitive(_523729), -(transitive(_523925))], (5305 ^ _341635) ^ [] : [connected(_523729), -(connected(_523925))], (5311 ^ _341635) ^ [] : [antisymmetric(_523729), -(antisymmetric(_523925))], (5317 ^ _341635) ^ [] : [well_founded_relation(_523729), -(well_founded_relation(_523925))]]]]]]], (5323 ^ _341635) ^ [_525269] : [relation(_525269), function(_525269), one_to_one(_525269), 5334 ^ _341635 : [(5335 ^ _341635) ^ [_525656] : [relation(_525656), function(_525656), 5342 ^ _341635 : [(5373 ^ _341635) ^ [] : [-(_525656 = function_inverse(_525269)), relation_dom(_525656) = relation_rng(_525269), 5382 ^ _341635 : [(5383 ^ _341635) ^ [] : [-(in(5378 ^ [_525269, _525656], relation_rng(_525269)))], (5385 ^ _341635) ^ [] : [-(5379 ^ [_525269, _525656] = apply(_525656, 5378 ^ [_525269, _525656]))], (5387 ^ _341635) ^ [] : [in(5379 ^ [_525269, _525656], relation_dom(_525269)), 5378 ^ [_525269, _525656] = apply(_525269, 5379 ^ [_525269, _525656])]], 5392 ^ _341635 : [(5393 ^ _341635) ^ [] : [-(in(5379 ^ [_525269, _525656], relation_dom(_525269)))], (5395 ^ _341635) ^ [] : [-(5378 ^ [_525269, _525656] = apply(_525269, 5379 ^ [_525269, _525656]))], (5397 ^ _341635) ^ [] : [in(5378 ^ [_525269, _525656], relation_rng(_525269)), 5379 ^ [_525269, _525656] = apply(_525656, 5378 ^ [_525269, _525656])]]], (5343 ^ _341635) ^ [] : [_525656 = function_inverse(_525269), 5346 ^ _341635 : [(5347 ^ _341635) ^ [] : [-(relation_dom(_525656) = relation_rng(_525269))], (5349 ^ _341635) ^ [_526173, _526175] : [5356 ^ _341635 : [(5357 ^ _341635) ^ [] : [-(in(_526173, relation_dom(_525269)))], (5359 ^ _341635) ^ [] : [-(_526175 = apply(_525269, _526173))]], in(_526175, relation_rng(_525269)), _526173 = apply(_525656, _526175)], (5361 ^ _341635) ^ [_526547, _526549] : [5368 ^ _341635 : [(5369 ^ _341635) ^ [] : [-(in(_526549, relation_rng(_525269)))], (5371 ^ _341635) ^ [] : [-(_526547 = apply(_525656, _526549))]], in(_526547, relation_dom(_525269)), _526549 = apply(_525269, _526547)]]]]]]], (5405 ^ _341635) ^ [_528122, _528124, _528126] : [element(_528122, powerset(_528126)), in(_528124, subset_complement(_528126, _528122)), in(_528124, _528122)], (5415 ^ _341635) ^ [_528428] : [relation(_528428), 5418 ^ _341635 : [(5419 ^ _341635) ^ [_528584] : [relation(_528584), 5422 ^ _341635 : [(5423 ^ _341635) ^ [_528736] : [relation(_528736), function(_528736), -(well_ordering(_528584)), well_ordering(_528428), relation_isomorphism(_528428, _528584, _528736)]]]]], (5441 ^ _341635) ^ [_529227] : [relation(_529227), function(_529227), one_to_one(_529227), 5452 ^ _341635 : [(5453 ^ _341635) ^ [] : [-(relation_rng(_529227) = relation_dom(function_inverse(_529227)))], (5455 ^ _341635) ^ [] : [-(relation_dom(_529227) = relation_rng(function_inverse(_529227)))]]], (5457 ^ _341635) ^ [_529680] : [relation(_529680), -(in(ordered_pair(5462 ^ [_529680], 5463 ^ [_529680]), _529680)), -(_529680 = empty_set)], (5469 ^ _341635) ^ [_530098, _530100] : [relation(_530098), function(_530098), 5484 ^ _341635 : [(5485 ^ _341635) ^ [] : [-(_530100 = apply(_530098, apply(function_inverse(_530098), _530100)))], (5487 ^ _341635) ^ [] : [-(_530100 = apply(relation_composition(function_inverse(_530098), _530098), _530100))]], one_to_one(_530098), in(_530100, relation_rng(_530098))], (5489 ^ _341635) ^ [_530696, _530698, _530700] : [in(_530700, _530698), element(_530698, powerset(_530696)), empty(_530696)], (5499 ^ _341635) ^ [_530992] : [relation(_530992), 5502 ^ _341635 : [(5503 ^ _341635) ^ [] : [well_founded_relation(_530992), -(is_well_founded_in(_530992, relation_field(_530992)))], (5509 ^ _341635) ^ [] : [is_well_founded_in(_530992, relation_field(_530992)), -(well_founded_relation(_530992))]]], (5515 ^ _341635) ^ [_531408] : [-(antisymmetric(inclusion_relation(_531408)))], (5517 ^ _341635) ^ [] : [-(relation_dom(empty_set) = empty_set)], (5519 ^ _341635) ^ [] : [-(relation_rng(empty_set) = empty_set)], (5521 ^ _341635) ^ [_531624, _531626] : [subset(_531626, _531624), proper_subset(_531624, _531626)], (5527 ^ _341635) ^ [_531819] : [relation(_531819), function(_531819), one_to_one(_531819), -(one_to_one(function_inverse(_531819)))], (5541 ^ _341635) ^ [_532205, _532207, _532209] : [-(disjoint(_532209, _532205)), subset(_532209, _532207), disjoint(_532207, _532205)], (5551 ^ _341635) ^ [_532500] : [relation(_532500), 5556 ^ _341635 : [(5557 ^ _341635) ^ [] : [relation_dom(_532500) = empty_set], (5559 ^ _341635) ^ [] : [relation_rng(_532500) = empty_set]], -(_532500 = empty_set)], (5563 ^ _341635) ^ [_532853] : [relation(_532853), 5566 ^ _341635 : [(5567 ^ _341635) ^ [] : [relation_dom(_532853) = empty_set, -(relation_rng(_532853) = empty_set)], (5573 ^ _341635) ^ [] : [relation_rng(_532853) = empty_set, -(relation_dom(_532853) = empty_set)]]], (5579 ^ _341635) ^ [_533336, _533338] : [set_difference(_533338, singleton(_533336)) = _533338, in(_533336, _533338)], (5585 ^ _341635) ^ [_533509, _533511] : [-(in(_533509, _533511)), -(set_difference(_533511, singleton(_533509)) = _533511)], (5591 ^ _341635) ^ [_533734, _533736] : [relation(_533734), function(_533734), 5598 ^ _341635 : [(5599 ^ _341635) ^ [_534001] : [relation(_534001), function(_534001), 5606 ^ _341635 : [(5607 ^ _341635) ^ [] : [_533734 = relation_dom_restriction(_534001, _533736), 5610 ^ _341635 : [(5611 ^ _341635) ^ [] : [-(relation_dom(_533734) = set_intersection2(relation_dom(_534001), _533736))], (5613 ^ _341635) ^ [_534455] : [in(_534455, relation_dom(_533734)), -(apply(_533734, _534455) = apply(_534001, _534455))]]], (5619 ^ _341635) ^ [] : [-(_533734 = relation_dom_restriction(_534001, _533736)), relation_dom(_533734) = set_intersection2(relation_dom(_534001), _533736), 5625 ^ _341635 : [(5626 ^ _341635) ^ [] : [-(in(5624 ^ [_533734, _533736, _534001], relation_dom(_533734)))], (5628 ^ _341635) ^ [] : [apply(_533734, 5624 ^ [_533734, _533736, _534001]) = apply(_534001, 5624 ^ [_533734, _533736, _534001])]]]]]]], (5632 ^ _341635) ^ [_535094] : [-(unordered_pair(_535094, _535094) = singleton(_535094))], (5634 ^ _341635) ^ [_535192] : [empty(_535192), -(_535192 = empty_set)], (5640 ^ _341635) ^ [_535380] : [ordinal(_535380), -(well_founded_relation(inclusion_relation(_535380)))], (5646 ^ _341635) ^ [_535584, _535586] : [subset(singleton(_535586), singleton(_535584)), -(_535586 = _535584)], (5652 ^ _341635) ^ [_535816, _535818, _535820] : [relation(_535816), function(_535816), in(_535818, relation_dom(relation_dom_restriction(_535816, _535820))), -(apply(relation_dom_restriction(_535816, _535820), _535818) = apply(_535816, _535818))], (5666 ^ _341635) ^ [_536235] : [-(relation_dom(identity_relation(_536235)) = _536235)], (5668 ^ _341635) ^ [_536283] : [-(relation_rng(identity_relation(_536283)) = _536283)], (5670 ^ _341635) ^ [_536410, _536412, _536414] : [relation(_536410), function(_536410), in(_536412, _536414), -(apply(relation_dom_restriction(_536410, _536414), _536412) = apply(_536410, _536412))], (5684 ^ _341635) ^ [_536856, _536858, _536860, _536862] : [relation(_536856), 5687 ^ _341635 : [(5688 ^ _341635) ^ [] : [in(ordered_pair(_536862, _536860), relation_composition(identity_relation(_536858), _536856)), 5691 ^ _341635 : [(5692 ^ _341635) ^ [] : [-(in(_536862, _536858))], (5694 ^ _341635) ^ [] : [-(in(ordered_pair(_536862, _536860), _536856))]]], (5696 ^ _341635) ^ [] : [-(in(ordered_pair(_536862, _536860), relation_composition(identity_relation(_536858), _536856))), in(_536862, _536858), in(ordered_pair(_536862, _536860), _536856)]]], (5706 ^ _341635) ^ [_537549, _537551] : [in(_537551, _537549), empty(_537549)], (5712 ^ _341635) ^ [_537761, _537763] : [-(pair_first(ordered_pair(_537763, _537761)) = _537763)], (5714 ^ _341635) ^ [_537812, _537814] : [-(pair_second(ordered_pair(_537814, _537812)) = _537812)], (5716 ^ _341635) ^ [_537928, _537930] : [in(_537930, _537928), 5720 ^ _341635 : [(5721 ^ _341635) ^ [] : [-(in(5719 ^ [_537928, _537930], _537928))], (5723 ^ _341635) ^ [_538219] : [in(_538219, _537928), in(_538219, 5719 ^ [_537928, _537930])]]], (5729 ^ _341635) ^ [_538444, _538446] : [-(subset(_538446, set_union2(_538446, _538444)))], (5731 ^ _341635) ^ [_538585, _538587] : [disjoint(_538587, _538585), -(set_difference(_538587, _538585) = _538587)], (5737 ^ _341635) ^ [_538753, _538755] : [set_difference(_538755, _538753) = _538755, -(disjoint(_538755, _538753))], (5743 ^ _341635) ^ [_538985, _538987, _538989] : [relation(_538985), 5746 ^ _341635 : [(5747 ^ _341635) ^ [] : [in(_538989, relation_dom(relation_dom_restriction(_538985, _538987))), 5750 ^ _341635 : [(5751 ^ _341635) ^ [] : [-(in(_538989, _538987))], (5753 ^ _341635) ^ [] : [-(in(_538989, relation_dom(_538985)))]]], (5755 ^ _341635) ^ [] : [-(in(_538989, relation_dom(relation_dom_restriction(_538985, _538987)))), in(_538989, _538987), in(_538989, relation_dom(_538985))]]], (5765 ^ _341635) ^ [_539644, _539646] : [relation(_539644), -(subset(relation_dom_restriction(_539644, _539646), _539644))], (5771 ^ _341635) ^ [_539858, _539860] : [empty(_539860), -(_539860 = _539858), empty(_539858)], (5781 ^ _341635) ^ [_540169, _540171, _540173] : [relation(_540169), function(_540169), 5788 ^ _341635 : [(5789 ^ _341635) ^ [] : [in(ordered_pair(_540173, _540171), _540169), 5792 ^ _341635 : [(5793 ^ _341635) ^ [] : [-(in(_540173, relation_dom(_540169)))], (5795 ^ _341635) ^ [] : [-(_540171 = apply(_540169, _540173))]]], (5797 ^ _341635) ^ [] : [-(in(ordered_pair(_540173, _540171), _540169)), in(_540173, relation_dom(_540169)), _540171 = apply(_540169, _540173)]]], (5807 ^ _341635) ^ [_540910] : [relation(_540910), 5810 ^ _341635 : [(5811 ^ _341635) ^ [] : [well_orders(_540910, relation_field(_540910)), -(well_ordering(_540910))], (5817 ^ _341635) ^ [] : [well_ordering(_540910), -(well_orders(_540910, relation_field(_540910)))]]], (5823 ^ _341635) ^ [_541369, _541371, _541373] : [-(subset(set_union2(_541373, _541369), _541371)), subset(_541373, _541371), subset(_541369, _541371)], (5833 ^ _341635) ^ [_541698, _541700, _541702] : [singleton(_541702) = unordered_pair(_541700, _541698), -(_541702 = _541700)], (5839 ^ _341635) ^ [_541924, _541926] : [relation(_541924), -(relation_dom(relation_dom_restriction(_541924, _541926)) = set_intersection2(relation_dom(_541924), _541926))], (5845 ^ _341635) ^ [_542152, _542154] : [in(_542154, _542152), -(subset(_542154, union(_542152)))], (5851 ^ _341635) ^ [_542366, _542368] : [relation(_542366), -(relation_dom_restriction(_542366, _542368) = relation_composition(identity_relation(_542368), _542366))], (5857 ^ _341635) ^ [_542590, _542592] : [relation(_542590), -(subset(relation_rng(relation_dom_restriction(_542590, _542592)), relation_rng(_542590)))], (5863 ^ _341635) ^ [_542783] : [-(union(powerset(_542783)) = _542783)], (5901 ^ _341635) ^ [_544304, _544306, _544308] : [singleton(_544308) = unordered_pair(_544306, _544304), -(_544306 = _544304)], (5866 ^ _341635) ^ [_543024] : [-(in(_543024, 5864 ^ [_543024]))], (5868 ^ _341635) ^ [_543136, _543138, _543140] : [-(in(_543136, 5864 ^ [_543140])), in(_543138, 5864 ^ [_543140]), subset(_543136, _543138)], (5878 ^ _341635) ^ [_543451, _543453] : [in(_543451, 5864 ^ [_543453]), 5882 ^ _341635 : [(5883 ^ _341635) ^ [] : [-(in(5881 ^ [_543451, _543453], 5864 ^ [_543453]))], (5885 ^ _341635) ^ [_543763] : [subset(_543763, _543451), -(in(_543763, 5881 ^ [_543451, _543453]))]]], (5891 ^ _341635) ^ [_543970, _543972] : [subset(_543970, 5864 ^ [_543972]), -(are_equipotent(_543970, 5864 ^ [_543972])), -(in(_543970, 5864 ^ [_543972]))]], input).
% 1.61/2.45 ncf('1',plain,[well_ordering(inclusion_relation(5906 ^ []))],start(5910 ^ 0)).
% 1.61/2.45 ncf('1.1',plain,[-(well_ordering(inclusion_relation(5906 ^ []))), 2300 : reflexive(inclusion_relation(5906 ^ [])), 2300 : transitive(inclusion_relation(5906 ^ [])), 2300 : antisymmetric(inclusion_relation(5906 ^ [])), 2300 : connected(inclusion_relation(5906 ^ [])), 2300 : well_founded_relation(inclusion_relation(5906 ^ [])), 2300 : relation(inclusion_relation(5906 ^ []))],extension(2282 ^ 1,bind([[_422639], [inclusion_relation(5906 ^ [])]]))).
% 1.61/2.45 ncf('1.1.1',plain,[-(reflexive(inclusion_relation(5906 ^ [])))],extension(4750 ^ 4,bind([[_506181], [5906 ^ []]]))).
% 1.61/2.45 ncf('1.1.2',plain,[-(transitive(inclusion_relation(5906 ^ [])))],extension(5009 ^ 4,bind([[_514797], [5906 ^ []]]))).
% 1.61/2.45 ncf('1.1.3',plain,[-(antisymmetric(inclusion_relation(5906 ^ [])))],extension(5515 ^ 4,bind([[_531408], [5906 ^ []]]))).
% 1.61/2.45 ncf('1.1.4',plain,[-(connected(inclusion_relation(5906 ^ []))), ordinal(5906 ^ [])],extension(5236 ^ 4,bind([[_522413], [5906 ^ []]]))).
% 1.61/2.45 ncf('1.1.4.1',plain,[-(ordinal(5906 ^ []))],extension(5908 ^ 5)).
% 1.61/2.45 ncf('1.1.5',plain,[-(well_founded_relation(inclusion_relation(5906 ^ []))), ordinal(5906 ^ [])],extension(5640 ^ 4,bind([[_535380], [5906 ^ []]]))).
% 1.61/2.45 ncf('1.1.5.1',plain,[-(ordinal(5906 ^ []))],extension(5908 ^ 5)).
% 1.61/2.45 ncf('1.1.6',plain,[-(relation(inclusion_relation(5906 ^ [])))],extension(3005 ^ 2,bind([[_447668], [5906 ^ []]]))).
% 1.61/2.45 %-----------------------------------------------------
% 1.61/2.45 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------