%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU193+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:35 EDT 2023
% Result : Theorem 6.23s 6.54s
% Output : Proof 6.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU193+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 12:41:27 EDT 2023
% 0.12/0.33 % CPUTime :
% 6.23/6.54
% 6.23/6.54 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 6.23/6.54 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.23/6.54 %-----------------------------------------------------
% 6.23/6.54 ncf(matrix, plain, [(2431 ^ _329283) ^ [] : [-(relation(2429 ^ []))], (2433 ^ _329283) ^ [] : [subset(relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ [])], (2 ^ _329283) ^ [_329427] : [-(_329427 = _329427)], (4 ^ _329283) ^ [_329534, _329536] : [_329536 = _329534, -(_329534 = _329536)], (10 ^ _329283) ^ [_329738, _329740, _329742] : [-(_329742 = _329738), _329742 = _329740, _329740 = _329738], (20 ^ _329283) ^ [_330079, _330081, _330083, _330085] : [-(element(_330083, _330079)), element(_330085, _330081), _330085 = _330083, _330081 = _330079], (34 ^ _329283) ^ [_330523, _330525, _330527, _330529] : [-(proper_subset(_330527, _330523)), proper_subset(_330529, _330525), _330529 = _330527, _330525 = _330523], (48 ^ _329283) ^ [_330967, _330969, _330971, _330973] : [-(disjoint(_330971, _330967)), disjoint(_330973, _330969), _330973 = _330971, _330969 = _330967], (62 ^ _329283) ^ [_331383, _331385] : [-(empty(_331383)), _331385 = _331383, empty(_331385)], (72 ^ _329283) ^ [_331706, _331708, _331710, _331712] : [-(are_equipotent(_331710, _331706)), are_equipotent(_331712, _331708), _331712 = _331710, _331708 = _331706], (86 ^ _329283) ^ [_332150, _332152, _332154, _332156] : [-(in(_332154, _332150)), in(_332156, _332152), _332156 = _332154, _332152 = _332150], (100 ^ _329283) ^ [_332566, _332568] : [-(relation(_332566)), _332568 = _332566, relation(_332568)], (110 ^ _329283) ^ [_332869, _332871, _332873, _332875] : [-(subset(_332873, _332869)), subset(_332875, _332871), _332875 = _332873, _332871 = _332869], (124 ^ _329283) ^ [_333305, _333307] : [_333307 = _333305, -(set_meet(_333307) = set_meet(_333305))], (130 ^ _329283) ^ [_333551, _333553, _333555, _333557] : [-(cartesian_product2(_333557, _333553) = cartesian_product2(_333555, _333551)), _333557 = _333555, _333553 = _333551], (140 ^ _329283) ^ [_333882, _333884] : [_333884 = _333882, -(relation_field(_333884) = relation_field(_333882))], (146 ^ _329283) ^ [_334100, _334102] : [_334102 = _334100, -(relation_inverse(_334102) = relation_inverse(_334100))], (152 ^ _329283) ^ [_334346, _334348, _334350, _334352] : [-(union_of_subsets(_334352, _334348) = union_of_subsets(_334350, _334346)), _334352 = _334350, _334348 = _334346], (162 ^ _329283) ^ [_334705, _334707, _334709, _334711] : [-(complements_of_subsets(_334711, _334707) = complements_of_subsets(_334709, _334705)), _334711 = _334709, _334707 = _334705], (172 ^ _329283) ^ [_335092, _335094, _335096, _335098, _335100, _335102] : [-(subset_difference(_335102, _335098, _335094) = subset_difference(_335100, _335096, _335092)), _335102 = _335100, _335098 = _335096, _335094 = _335092], (186 ^ _329283) ^ [_335552, _335554] : [_335554 = _335552, -(cast_to_subset(_335554) = cast_to_subset(_335552))], (192 ^ _329283) ^ [_335798, _335800, _335802, _335804] : [-(meet_of_subsets(_335804, _335800) = meet_of_subsets(_335802, _335798)), _335804 = _335802, _335800 = _335798], (202 ^ _329283) ^ [_336157, _336159, _336161, _336163] : [-(set_intersection2(_336163, _336159) = set_intersection2(_336161, _336157)), _336163 = _336161, _336159 = _336157], (212 ^ _329283) ^ [_336516, _336518, _336520, _336522] : [-(subset_complement(_336522, _336518) = subset_complement(_336520, _336516)), _336522 = _336520, _336518 = _336516], (222 ^ _329283) ^ [_336847, _336849] : [_336849 = _336847, -(relation_rng(_336849) = relation_rng(_336847))], (228 ^ _329283) ^ [_337093, _337095, _337097, _337099] : [-(relation_composition(_337099, _337095) = relation_composition(_337097, _337093)), _337099 = _337097, _337095 = _337093], (238 ^ _329283) ^ [_337424, _337426] : [_337426 = _337424, -(identity_relation(_337426) = identity_relation(_337424))], (244 ^ _329283) ^ [_337670, _337672, _337674, _337676] : [-(ordered_pair(_337676, _337672) = ordered_pair(_337674, _337670)), _337676 = _337674, _337672 = _337670], (254 ^ _329283) ^ [_338029, _338031, _338033, _338035] : [-(set_difference(_338035, _338031) = set_difference(_338033, _338029)), _338035 = _338033, _338031 = _338029], (264 ^ _329283) ^ [_338360, _338362] : [_338362 = _338360, -(relation_dom(_338362) = relation_dom(_338360))], (270 ^ _329283) ^ [_338606, _338608, _338610, _338612] : [-(set_union2(_338612, _338608) = set_union2(_338610, _338606)), _338612 = _338610, _338608 = _338606], (280 ^ _329283) ^ [_338937, _338939] : [_338939 = _338937, -(union(_338939) = union(_338937))], (286 ^ _329283) ^ [_339155, _339157] : [_339157 = _339155, -(powerset(_339157) = powerset(_339155))], (292 ^ _329283) ^ [_339373, _339375] : [_339375 = _339373, -(singleton(_339375) = singleton(_339373))], (298 ^ _329283) ^ [_339619, _339621, _339623, _339625] : [-(unordered_pair(_339625, _339621) = unordered_pair(_339623, _339619)), _339625 = _339623, _339621 = _339619], (308 ^ _329283) ^ [_339958, _339960, _339962, _339964] : [-(relation_dom_restriction(_339964, _339960) = relation_dom_restriction(_339962, _339958)), _339964 = _339962, _339960 = _339958], (318 ^ _329283) ^ [_340391, _340393] : [in(_340393, _340391), in(_340391, _340393)], (324 ^ _329283) ^ [_340602, _340604] : [proper_subset(_340604, _340602), proper_subset(_340602, _340604)], (330 ^ _329283) ^ [_340799] : [empty(_340799), -(relation(_340799))], (336 ^ _329283) ^ [_340984, _340986] : [-(unordered_pair(_340986, _340984) = unordered_pair(_340984, _340986))], (338 ^ _329283) ^ [_341084, _341086] : [-(set_union2(_341086, _341084) = set_union2(_341084, _341086))], (340 ^ _329283) ^ [_341184, _341186] : [-(set_intersection2(_341186, _341184) = set_intersection2(_341184, _341186))], (342 ^ _329283) ^ [_341299, _341301] : [relation(_341299), 345 ^ _329283 : [(368 ^ _329283) ^ [] : [-(_341299 = identity_relation(_341301)), 381 ^ _329283 : [(382 ^ _329283) ^ [] : [-(in(369 ^ [_341299, _341301], _341301))], (384 ^ _329283) ^ [] : [-(369 ^ [_341299, _341301] = 370 ^ [_341299, _341301])], (386 ^ _329283) ^ [] : [in(ordered_pair(369 ^ [_341299, _341301], 370 ^ [_341299, _341301]), _341299)]], 373 ^ _329283 : [(374 ^ _329283) ^ [] : [-(in(ordered_pair(369 ^ [_341299, _341301], 370 ^ [_341299, _341301]), _341299))], (376 ^ _329283) ^ [] : [in(369 ^ [_341299, _341301], _341301), 369 ^ [_341299, _341301] = 370 ^ [_341299, _341301]]]], (346 ^ _329283) ^ [] : [_341299 = identity_relation(_341301), 349 ^ _329283 : [(350 ^ _329283) ^ [_341609, _341611] : [in(ordered_pair(_341611, _341609), _341299), 353 ^ _329283 : [(354 ^ _329283) ^ [] : [-(in(_341611, _341301))], (356 ^ _329283) ^ [] : [-(_341611 = _341609)]]], (358 ^ _329283) ^ [_341872, _341874] : [-(in(ordered_pair(_341874, _341872), _341299)), in(_341874, _341301), _341874 = _341872]]]]], (390 ^ _329283) ^ [_342980, _342982] : [_342982 = _342980, 393 ^ _329283 : [(394 ^ _329283) ^ [] : [-(subset(_342982, _342980))], (396 ^ _329283) ^ [] : [-(subset(_342980, _342982))]]], (398 ^ _329283) ^ [_343217, _343219] : [-(_343219 = _343217), subset(_343219, _343217), subset(_343217, _343219)], (408 ^ _329283) ^ [_343504] : [relation(_343504), 411 ^ _329283 : [(412 ^ _329283) ^ [_343690, _343692] : [relation(_343690), 415 ^ _329283 : [(438 ^ _329283) ^ [] : [-(_343690 = relation_dom_restriction(_343504, _343692)), 451 ^ _329283 : [(452 ^ _329283) ^ [] : [-(in(439 ^ [_343504, _343690, _343692], _343692))], (454 ^ _329283) ^ [] : [-(in(ordered_pair(439 ^ [_343504, _343690, _343692], 440 ^ [_343504, _343690, _343692]), _343504))], (456 ^ _329283) ^ [] : [in(ordered_pair(439 ^ [_343504, _343690, _343692], 440 ^ [_343504, _343690, _343692]), _343690)]], 443 ^ _329283 : [(444 ^ _329283) ^ [] : [-(in(ordered_pair(439 ^ [_343504, _343690, _343692], 440 ^ [_343504, _343690, _343692]), _343690))], (446 ^ _329283) ^ [] : [in(439 ^ [_343504, _343690, _343692], _343692), in(ordered_pair(439 ^ [_343504, _343690, _343692], 440 ^ [_343504, _343690, _343692]), _343504)]]], (416 ^ _329283) ^ [] : [_343690 = relation_dom_restriction(_343504, _343692), 419 ^ _329283 : [(420 ^ _329283) ^ [_344015, _344017] : [in(ordered_pair(_344017, _344015), _343690), 423 ^ _329283 : [(424 ^ _329283) ^ [] : [-(in(_344017, _343692))], (426 ^ _329283) ^ [] : [-(in(ordered_pair(_344017, _344015), _343504))]]], (428 ^ _329283) ^ [_344294, _344296] : [-(in(ordered_pair(_344296, _344294), _343690)), in(_344296, _343692), in(ordered_pair(_344296, _344294), _343504)]]]]]]], (472 ^ _329283) ^ [_345939] : [474 ^ _329283 : [(475 ^ _329283) ^ [] : [-(in(473 ^ [_345939], _345939))], (477 ^ _329283) ^ [_346176, _346178] : [473 ^ [_345939] = ordered_pair(_346178, _346176)]], -(relation(_345939))], (460 ^ _329283) ^ [_345478] : [relation(_345478), 463 ^ _329283 : [(464 ^ _329283) ^ [_345626] : [in(_345626, _345478), -(_345626 = ordered_pair(467 ^ [_345478, _345626], 468 ^ [_345478, _345626]))]]], (530 ^ _329283) ^ [_348074, _348076] : [_348076 = empty_set, 533 ^ _329283 : [(534 ^ _329283) ^ [] : [_348074 = set_meet(_348076), -(_348074 = empty_set)], (540 ^ _329283) ^ [] : [_348074 = empty_set, -(_348074 = set_meet(_348076))]]], (481 ^ _329283) ^ [_346367, _346369] : [-(_346369 = empty_set), 484 ^ _329283 : [(508 ^ _329283) ^ [] : [-(_346367 = set_meet(_346369)), 512 ^ _329283 : [(513 ^ _329283) ^ [] : [-(in(509 ^ [_346367, _346369], _346367))], (516 ^ _329283) ^ [] : [-(in(514 ^ [_346367, _346369], _346369))], (518 ^ _329283) ^ [] : [in(509 ^ [_346367, _346369], 514 ^ [_346367, _346369])]], 519 ^ _329283 : [(526 ^ _329283) ^ [] : [in(509 ^ [_346367, _346369], _346367)], (520 ^ _329283) ^ [_347769] : [in(_347769, _346369), -(in(509 ^ [_346367, _346369], _347769))]]], (485 ^ _329283) ^ [] : [_346367 = set_meet(_346369), 488 ^ _329283 : [(499 ^ _329283) ^ [_346995] : [501 ^ _329283 : [(502 ^ _329283) ^ [] : [-(in(500 ^ [_346367, _346369, _346995], _346369))], (504 ^ _329283) ^ [] : [in(_346995, 500 ^ [_346367, _346369, _346995])]], -(in(_346995, _346367))], (489 ^ _329283) ^ [_346665] : [in(_346665, _346367), 492 ^ _329283 : [(493 ^ _329283) ^ [_346810] : [in(_346810, _346369), -(in(_346665, _346810))]]]]]]], (562 ^ _329283) ^ [_349092, _349094] : [-(_349092 = singleton(_349094)), 566 ^ _329283 : [(567 ^ _329283) ^ [] : [-(in(563 ^ [_349092, _349094], _349092))], (569 ^ _329283) ^ [] : [563 ^ [_349092, _349094] = _349094]], 570 ^ _329283 : [(571 ^ _329283) ^ [] : [-(563 ^ [_349092, _349094] = _349094)], (573 ^ _329283) ^ [] : [in(563 ^ [_349092, _349094], _349092)]]], (546 ^ _329283) ^ [_348571, _348573] : [_348571 = singleton(_348573), 549 ^ _329283 : [(550 ^ _329283) ^ [_348741] : [in(_348741, _348571), -(_348741 = _348573)], (556 ^ _329283) ^ [_348913] : [_348913 = _348573, -(in(_348913, _348571))]]], (577 ^ _329283) ^ [_349643] : [_349643 = empty_set, 580 ^ _329283 : [(581 ^ _329283) ^ [_349756] : [in(_349756, _349643)]]], (583 ^ _329283) ^ [_349822] : [-(in(584 ^ [_349822], _349822)), -(_349822 = empty_set)], (606 ^ _329283) ^ [_350634, _350636] : [-(_350634 = powerset(_350636)), 610 ^ _329283 : [(611 ^ _329283) ^ [] : [-(in(607 ^ [_350634, _350636], _350634))], (613 ^ _329283) ^ [] : [subset(607 ^ [_350634, _350636], _350636)]], 614 ^ _329283 : [(615 ^ _329283) ^ [] : [-(subset(607 ^ [_350634, _350636], _350636))], (617 ^ _329283) ^ [] : [in(607 ^ [_350634, _350636], _350634)]]], (590 ^ _329283) ^ [_350113, _350115] : [_350113 = powerset(_350115), 593 ^ _329283 : [(594 ^ _329283) ^ [_350283] : [in(_350283, _350113), -(subset(_350283, _350115))], (600 ^ _329283) ^ [_350455] : [subset(_350455, _350115), -(in(_350455, _350113))]]], (621 ^ _329283) ^ [_351190, _351192] : [-(empty(_351192)), 624 ^ _329283 : [(625 ^ _329283) ^ [] : [element(_351190, _351192), -(in(_351190, _351192))], (631 ^ _329283) ^ [] : [in(_351190, _351192), -(element(_351190, _351192))]]], (637 ^ _329283) ^ [_351603, _351605] : [empty(_351605), 640 ^ _329283 : [(641 ^ _329283) ^ [] : [element(_351603, _351605), -(empty(_351603))], (647 ^ _329283) ^ [] : [empty(_351603), -(element(_351603, _351605))]]], (675 ^ _329283) ^ [_352828, _352830, _352832] : [-(_352828 = unordered_pair(_352832, _352830)), 679 ^ _329283 : [(680 ^ _329283) ^ [] : [-(in(676 ^ [_352828, _352830, _352832], _352828))], (682 ^ _329283) ^ [] : [676 ^ [_352828, _352830, _352832] = _352832], (684 ^ _329283) ^ [] : [676 ^ [_352828, _352830, _352832] = _352830]], 685 ^ _329283 : [(692 ^ _329283) ^ [] : [in(676 ^ [_352828, _352830, _352832], _352828)], (686 ^ _329283) ^ [] : [-(676 ^ [_352828, _352830, _352832] = _352832), -(676 ^ [_352828, _352830, _352832] = _352830)]]], (653 ^ _329283) ^ [_352103, _352105, _352107] : [_352103 = unordered_pair(_352107, _352105), 656 ^ _329283 : [(667 ^ _329283) ^ [_352563] : [668 ^ _329283 : [(669 ^ _329283) ^ [] : [_352563 = _352107], (671 ^ _329283) ^ [] : [_352563 = _352105]], -(in(_352563, _352103))], (657 ^ _329283) ^ [_352285] : [in(_352285, _352103), -(_352285 = _352107), -(_352285 = _352105)]]], (718 ^ _329283) ^ [_354347, _354349, _354351] : [-(_354347 = set_union2(_354351, _354349)), 722 ^ _329283 : [(723 ^ _329283) ^ [] : [-(in(719 ^ [_354347, _354349, _354351], _354347))], (725 ^ _329283) ^ [] : [in(719 ^ [_354347, _354349, _354351], _354351)], (727 ^ _329283) ^ [] : [in(719 ^ [_354347, _354349, _354351], _354349)]], 728 ^ _329283 : [(735 ^ _329283) ^ [] : [in(719 ^ [_354347, _354349, _354351], _354347)], (729 ^ _329283) ^ [] : [-(in(719 ^ [_354347, _354349, _354351], _354351)), -(in(719 ^ [_354347, _354349, _354351], _354349))]]], (696 ^ _329283) ^ [_353622, _353624, _353626] : [_353622 = set_union2(_353626, _353624), 699 ^ _329283 : [(710 ^ _329283) ^ [_354082] : [711 ^ _329283 : [(712 ^ _329283) ^ [] : [in(_354082, _353626)], (714 ^ _329283) ^ [] : [in(_354082, _353624)]], -(in(_354082, _353622))], (700 ^ _329283) ^ [_353804] : [in(_353804, _353622), -(in(_353804, _353626)), -(in(_353804, _353624))]]], (769 ^ _329283) ^ [_356398, _356400, _356402] : [-(_356398 = cartesian_product2(_356402, _356400)), 787 ^ _329283 : [(788 ^ _329283) ^ [] : [-(in(785 ^ [_356398, _356400, _356402], _356402))], (790 ^ _329283) ^ [] : [-(in(786 ^ [_356398, _356400, _356402], _356400))], (792 ^ _329283) ^ [] : [-(770 ^ [_356398, _356400, _356402] = ordered_pair(785 ^ [_356398, _356400, _356402], 786 ^ [_356398, _356400, _356402]))], (794 ^ _329283) ^ [] : [in(770 ^ [_356398, _356400, _356402], _356398)]], 773 ^ _329283 : [(774 ^ _329283) ^ [] : [-(in(770 ^ [_356398, _356400, _356402], _356398))], (776 ^ _329283) ^ [_356736, _356738] : [in(_356738, _356402), in(_356736, _356400), 770 ^ [_356398, _356400, _356402] = ordered_pair(_356738, _356736)]]], (739 ^ _329283) ^ [_355141, _355143, _355145] : [_355141 = cartesian_product2(_355145, _355143), 742 ^ _329283 : [(743 ^ _329283) ^ [_355342] : [in(_355342, _355141), 748 ^ _329283 : [(749 ^ _329283) ^ [] : [-(in(746 ^ [_355141, _355143, _355145, _355342], _355145))], (751 ^ _329283) ^ [] : [-(in(747 ^ [_355141, _355143, _355145, _355342], _355143))], (753 ^ _329283) ^ [] : [-(_355342 = ordered_pair(746 ^ [_355141, _355143, _355145, _355342], 747 ^ [_355141, _355143, _355145, _355342]))]]], (755 ^ _329283) ^ [_355902] : [-(in(_355902, _355141)), 756 ^ _329283 : [(757 ^ _329283) ^ [_356032, _356034] : [in(_356034, _355145), in(_356032, _355143), _355902 = ordered_pair(_356034, _356032)]]]]], (798 ^ _329283) ^ [_357632] : [relation(_357632), 801 ^ _329283 : [(802 ^ _329283) ^ [_357790] : [relation(_357790), 805 ^ _329283 : [(816 ^ _329283) ^ [] : [819 ^ _329283 : [(820 ^ _329283) ^ [] : [-(in(ordered_pair(817 ^ [_357632, _357790], 818 ^ [_357632, _357790]), _357632))], (822 ^ _329283) ^ [] : [in(ordered_pair(817 ^ [_357632, _357790], 818 ^ [_357632, _357790]), _357790)]], -(subset(_357632, _357790))], (806 ^ _329283) ^ [] : [subset(_357632, _357790), 809 ^ _329283 : [(810 ^ _329283) ^ [_358066, _358068] : [in(ordered_pair(_358068, _358066), _357632), -(in(ordered_pair(_358068, _358066), _357790))]]]]]]], (836 ^ _329283) ^ [_359029, _359031] : [838 ^ _329283 : [(839 ^ _329283) ^ [] : [-(in(837 ^ [_359029, _359031], _359031))], (841 ^ _329283) ^ [] : [in(837 ^ [_359029, _359031], _359029)]], -(subset(_359031, _359029))], (826 ^ _329283) ^ [_358715, _358717] : [subset(_358717, _358715), 829 ^ _329283 : [(830 ^ _329283) ^ [_358852] : [in(_358852, _358717), -(in(_358852, _358715))]]], (867 ^ _329283) ^ [_360154, _360156, _360158] : [-(_360154 = set_intersection2(_360158, _360156)), 879 ^ _329283 : [(880 ^ _329283) ^ [] : [-(in(868 ^ [_360154, _360156, _360158], _360158))], (882 ^ _329283) ^ [] : [-(in(868 ^ [_360154, _360156, _360158], _360156))], (884 ^ _329283) ^ [] : [in(868 ^ [_360154, _360156, _360158], _360154)]], 871 ^ _329283 : [(872 ^ _329283) ^ [] : [-(in(868 ^ [_360154, _360156, _360158], _360154))], (874 ^ _329283) ^ [] : [in(868 ^ [_360154, _360156, _360158], _360158), in(868 ^ [_360154, _360156, _360158], _360156)]]], (845 ^ _329283) ^ [_359429, _359431, _359433] : [_359429 = set_intersection2(_359433, _359431), 848 ^ _329283 : [(849 ^ _329283) ^ [_359611] : [in(_359611, _359429), 852 ^ _329283 : [(853 ^ _329283) ^ [] : [-(in(_359611, _359433))], (855 ^ _329283) ^ [] : [-(in(_359611, _359431))]]], (857 ^ _329283) ^ [_359870] : [-(in(_359870, _359429)), in(_359870, _359433), in(_359870, _359431)]]], (888 ^ _329283) ^ [_360893] : [relation(_360893), 891 ^ _329283 : [(909 ^ _329283) ^ [_361705] : [-(_361705 = relation_dom(_360893)), 913 ^ _329283 : [(914 ^ _329283) ^ [] : [-(in(910 ^ [_360893, _361705], _361705))], (916 ^ _329283) ^ [_361968] : [in(ordered_pair(910 ^ [_360893, _361705], _361968), _360893)]], 918 ^ _329283 : [(919 ^ _329283) ^ [] : [-(in(ordered_pair(910 ^ [_360893, _361705], 917 ^ [_360893, _361705]), _360893))], (921 ^ _329283) ^ [] : [in(910 ^ [_360893, _361705], _361705)]]], (892 ^ _329283) ^ [_361074] : [_361074 = relation_dom(_360893), 895 ^ _329283 : [(896 ^ _329283) ^ [_361254] : [in(_361254, _361074), -(in(ordered_pair(_361254, 899 ^ [_360893, _361074, _361254]), _360893))], (903 ^ _329283) ^ [_361498] : [904 ^ _329283 : [(905 ^ _329283) ^ [_361577] : [in(ordered_pair(_361498, _361577), _360893)]], -(in(_361498, _361074))]]]]], (925 ^ _329283) ^ [_362319] : [-(cast_to_subset(_362319) = _362319)], (950 ^ _329283) ^ [_363302, _363304] : [-(_363302 = union(_363304)), 963 ^ _329283 : [(964 ^ _329283) ^ [] : [-(in(951 ^ [_363302, _363304], 962 ^ [_363302, _363304]))], (966 ^ _329283) ^ [] : [-(in(962 ^ [_363302, _363304], _363304))], (968 ^ _329283) ^ [] : [in(951 ^ [_363302, _363304], _363302)]], 954 ^ _329283 : [(955 ^ _329283) ^ [] : [-(in(951 ^ [_363302, _363304], _363302))], (957 ^ _329283) ^ [_363585] : [in(951 ^ [_363302, _363304], _363585), in(_363585, _363304)]]], (927 ^ _329283) ^ [_362457, _362459] : [_362457 = union(_362459), 930 ^ _329283 : [(931 ^ _329283) ^ [_362638] : [in(_362638, _362457), 935 ^ _329283 : [(936 ^ _329283) ^ [] : [-(in(_362638, 934 ^ [_362457, _362459, _362638]))], (938 ^ _329283) ^ [] : [-(in(934 ^ [_362457, _362459, _362638], _362459))]]], (940 ^ _329283) ^ [_362965] : [-(in(_362965, _362457)), 941 ^ _329283 : [(942 ^ _329283) ^ [_363063] : [in(_362965, _363063), in(_363063, _362459)]]]]], (994 ^ _329283) ^ [_364923, _364925, _364927] : [-(_364923 = set_difference(_364927, _364925)), 1006 ^ _329283 : [(1007 ^ _329283) ^ [] : [-(in(995 ^ [_364923, _364925, _364927], _364927))], (1009 ^ _329283) ^ [] : [in(995 ^ [_364923, _364925, _364927], _364925)], (1011 ^ _329283) ^ [] : [in(995 ^ [_364923, _364925, _364927], _364923)]], 998 ^ _329283 : [(999 ^ _329283) ^ [] : [-(in(995 ^ [_364923, _364925, _364927], _364923))], (1001 ^ _329283) ^ [] : [in(995 ^ [_364923, _364925, _364927], _364927), -(in(995 ^ [_364923, _364925, _364927], _364925))]]], (972 ^ _329283) ^ [_364192, _364194, _364196] : [_364192 = set_difference(_364196, _364194), 975 ^ _329283 : [(976 ^ _329283) ^ [_364376] : [in(_364376, _364192), 979 ^ _329283 : [(980 ^ _329283) ^ [] : [-(in(_364376, _364196))], (982 ^ _329283) ^ [] : [in(_364376, _364194)]]], (984 ^ _329283) ^ [_364636] : [-(in(_364636, _364192)), in(_364636, _364196), -(in(_364636, _364194))]]], (1015 ^ _329283) ^ [_365666] : [relation(_365666), 1018 ^ _329283 : [(1036 ^ _329283) ^ [_366478] : [-(_366478 = relation_rng(_365666)), 1040 ^ _329283 : [(1041 ^ _329283) ^ [] : [-(in(1037 ^ [_365666, _366478], _366478))], (1043 ^ _329283) ^ [_366741] : [in(ordered_pair(_366741, 1037 ^ [_365666, _366478]), _365666)]], 1045 ^ _329283 : [(1046 ^ _329283) ^ [] : [-(in(ordered_pair(1044 ^ [_365666, _366478], 1037 ^ [_365666, _366478]), _365666))], (1048 ^ _329283) ^ [] : [in(1037 ^ [_365666, _366478], _366478)]]], (1019 ^ _329283) ^ [_365847] : [_365847 = relation_rng(_365666), 1022 ^ _329283 : [(1023 ^ _329283) ^ [_366027] : [in(_366027, _365847), -(in(ordered_pair(1026 ^ [_365666, _365847, _366027], _366027), _365666))], (1030 ^ _329283) ^ [_366271] : [1031 ^ _329283 : [(1032 ^ _329283) ^ [_366350] : [in(ordered_pair(_366350, _366271), _365666)]], -(in(_366271, _365847))]]]]], (1052 ^ _329283) ^ [_367121, _367123] : [element(_367121, powerset(_367123)), -(subset_complement(_367123, _367121) = set_difference(_367123, _367121))], (1058 ^ _329283) ^ [_367332, _367334] : [-(ordered_pair(_367334, _367332) = unordered_pair(unordered_pair(_367334, _367332), singleton(_367334)))], (1060 ^ _329283) ^ [_367438] : [relation(_367438), -(relation_field(_367438) = set_union2(relation_dom(_367438), relation_rng(_367438)))], (1066 ^ _329283) ^ [_367644] : [relation(_367644), 1069 ^ _329283 : [(1070 ^ _329283) ^ [_367804] : [relation(_367804), 1073 ^ _329283 : [(1090 ^ _329283) ^ [] : [-(_367804 = relation_inverse(_367644)), 1095 ^ _329283 : [(1096 ^ _329283) ^ [] : [-(in(ordered_pair(1091 ^ [_367644, _367804], 1092 ^ [_367644, _367804]), _367804))], (1098 ^ _329283) ^ [] : [in(ordered_pair(1092 ^ [_367644, _367804], 1091 ^ [_367644, _367804]), _367644)]], 1099 ^ _329283 : [(1100 ^ _329283) ^ [] : [-(in(ordered_pair(1092 ^ [_367644, _367804], 1091 ^ [_367644, _367804]), _367644))], (1102 ^ _329283) ^ [] : [in(ordered_pair(1091 ^ [_367644, _367804], 1092 ^ [_367644, _367804]), _367804)]]], (1074 ^ _329283) ^ [] : [_367804 = relation_inverse(_367644), 1077 ^ _329283 : [(1078 ^ _329283) ^ [_368113, _368115] : [in(ordered_pair(_368115, _368113), _367804), -(in(ordered_pair(_368113, _368115), _367644))], (1084 ^ _329283) ^ [_368303, _368305] : [in(ordered_pair(_368303, _368305), _367644), -(in(ordered_pair(_368305, _368303), _367804))]]]]]]], (1106 ^ _329283) ^ [_369151, _369153] : [disjoint(_369153, _369151), -(set_intersection2(_369153, _369151) = empty_set)], (1112 ^ _329283) ^ [_369319, _369321] : [set_intersection2(_369321, _369319) = empty_set, -(disjoint(_369321, _369319))], (1118 ^ _329283) ^ [_369523] : [relation(_369523), 1121 ^ _329283 : [(1122 ^ _329283) ^ [_369708] : [relation(_369708), 1125 ^ _329283 : [(1126 ^ _329283) ^ [_369889] : [relation(_369889), 1129 ^ _329283 : [(1153 ^ _329283) ^ [] : [-(_369889 = relation_composition(_369523, _369708)), 1167 ^ _329283 : [(1168 ^ _329283) ^ [] : [-(in(ordered_pair(1154 ^ [_369523, _369708, _369889], 1166 ^ [_369523, _369708, _369889]), _369523))], (1170 ^ _329283) ^ [] : [-(in(ordered_pair(1166 ^ [_369523, _369708, _369889], 1155 ^ [_369523, _369708, _369889]), _369708))], (1172 ^ _329283) ^ [] : [in(ordered_pair(1154 ^ [_369523, _369708, _369889], 1155 ^ [_369523, _369708, _369889]), _369889)]], 1158 ^ _329283 : [(1159 ^ _329283) ^ [] : [-(in(ordered_pair(1154 ^ [_369523, _369708, _369889], 1155 ^ [_369523, _369708, _369889]), _369889))], (1161 ^ _329283) ^ [_371353] : [in(ordered_pair(1154 ^ [_369523, _369708, _369889], _371353), _369523), in(ordered_pair(_371353, 1155 ^ [_369523, _369708, _369889]), _369708)]]], (1130 ^ _329283) ^ [] : [_369889 = relation_composition(_369523, _369708), 1133 ^ _329283 : [(1134 ^ _329283) ^ [_370224, _370226] : [in(ordered_pair(_370226, _370224), _369889), 1138 ^ _329283 : [(1139 ^ _329283) ^ [] : [-(in(ordered_pair(_370226, 1137 ^ [_369523, _369708, _369889, _370224, _370226]), _369523))], (1141 ^ _329283) ^ [] : [-(in(ordered_pair(1137 ^ [_369523, _369708, _369889, _370224, _370226], _370224), _369708))]]], (1143 ^ _329283) ^ [_370609, _370611] : [-(in(ordered_pair(_370611, _370609), _369889)), 1144 ^ _329283 : [(1145 ^ _329283) ^ [_370722] : [in(ordered_pair(_370611, _370722), _369523), in(ordered_pair(_370722, _370609), _369708)]]]]]]]]]]], (1176 ^ _329283) ^ [_372039, _372041] : [element(_372039, powerset(powerset(_372041))), 1179 ^ _329283 : [(1180 ^ _329283) ^ [_372219] : [element(_372219, powerset(powerset(_372041))), 1183 ^ _329283 : [(1204 ^ _329283) ^ [] : [-(_372219 = complements_of_subsets(_372041, _372039)), 1206 ^ _329283 : [(1207 ^ _329283) ^ [] : [-(element(1205 ^ [_372039, _372041, _372219], powerset(_372041)))], (1209 ^ _329283) ^ [] : [1210 ^ _329283 : [(1211 ^ _329283) ^ [] : [-(in(1205 ^ [_372039, _372041, _372219], _372219))], (1213 ^ _329283) ^ [] : [in(subset_complement(_372041, 1205 ^ [_372039, _372041, _372219]), _372039)]], 1214 ^ _329283 : [(1215 ^ _329283) ^ [] : [-(in(subset_complement(_372041, 1205 ^ [_372039, _372041, _372219]), _372039))], (1217 ^ _329283) ^ [] : [in(1205 ^ [_372039, _372041, _372219], _372219)]]]]], (1184 ^ _329283) ^ [] : [_372219 = complements_of_subsets(_372041, _372039), 1187 ^ _329283 : [(1188 ^ _329283) ^ [_372507] : [element(_372507, powerset(_372041)), 1191 ^ _329283 : [(1192 ^ _329283) ^ [] : [in(_372507, _372219), -(in(subset_complement(_372041, _372507), _372039))], (1198 ^ _329283) ^ [] : [in(subset_complement(_372041, _372507), _372039), -(in(_372507, _372219))]]]]]]]]], (1221 ^ _329283) ^ [_373630, _373632] : [proper_subset(_373632, _373630), 1224 ^ _329283 : [(1225 ^ _329283) ^ [] : [-(subset(_373632, _373630))], (1227 ^ _329283) ^ [] : [_373632 = _373630]]], (1229 ^ _329283) ^ [_373868, _373870] : [-(proper_subset(_373870, _373868)), subset(_373870, _373868), -(_373870 = _373868)], (1239 ^ _329283) ^ [] : [true___, -(true___)], (1245 ^ _329283) ^ [] : [true___, -(true___)], (1251 ^ _329283) ^ [] : [true___, -(true___)], (1257 ^ _329283) ^ [] : [true___, -(true___)], (1263 ^ _329283) ^ [] : [true___, -(true___)], (1269 ^ _329283) ^ [] : [true___, -(true___)], (1275 ^ _329283) ^ [_374857] : [-(element(cast_to_subset(_374857), powerset(_374857)))], (1277 ^ _329283) ^ [] : [true___, -(true___)], (1283 ^ _329283) ^ [] : [true___, -(true___)], (1289 ^ _329283) ^ [] : [true___, -(true___)], (1295 ^ _329283) ^ [] : [true___, -(true___)], (1301 ^ _329283) ^ [_375444, _375446] : [element(_375444, powerset(_375446)), -(element(subset_complement(_375446, _375444), powerset(_375446)))], (1307 ^ _329283) ^ [] : [true___, -(true___)], (1313 ^ _329283) ^ [] : [true___, -(true___)], (1319 ^ _329283) ^ [_375892] : [relation(_375892), -(relation(relation_inverse(_375892)))], (1325 ^ _329283) ^ [] : [true___, -(true___)], (1331 ^ _329283) ^ [] : [true___, -(true___)], (1337 ^ _329283) ^ [_376334, _376336] : [-(relation(relation_composition(_376336, _376334))), relation(_376336), relation(_376334)], (1347 ^ _329283) ^ [_376633, _376635] : [element(_376633, powerset(powerset(_376635))), -(element(union_of_subsets(_376635, _376633), powerset(_376635)))], (1353 ^ _329283) ^ [_376832] : [-(relation(identity_relation(_376832)))], (1355 ^ _329283) ^ [_376940, _376942] : [element(_376940, powerset(powerset(_376942))), -(element(meet_of_subsets(_376942, _376940), powerset(_376942)))], (1361 ^ _329283) ^ [_377182, _377184, _377186] : [-(element(subset_difference(_377186, _377184, _377182), powerset(_377186))), element(_377184, powerset(_377186)), element(_377182, powerset(_377186))], (1371 ^ _329283) ^ [_377511, _377513] : [relation(_377513), -(relation(relation_dom_restriction(_377513, _377511)))], (1377 ^ _329283) ^ [_377723, _377725] : [element(_377723, powerset(powerset(_377725))), -(element(complements_of_subsets(_377725, _377723), powerset(powerset(_377725))))], (1383 ^ _329283) ^ [] : [true___, -(true___)], (1390 ^ _329283) ^ [_378084] : [-(element(1388 ^ [_378084], _378084))], (1392 ^ _329283) ^ [_378196, _378198] : [1399 ^ _329283 : [(1400 ^ _329283) ^ [] : [-(empty(relation_composition(_378196, _378198)))], (1402 ^ _329283) ^ [] : [-(relation(relation_composition(_378196, _378198)))]], empty(_378198), relation(_378196)], (1404 ^ _329283) ^ [_378544] : [empty(powerset(_378544))], (1406 ^ _329283) ^ [] : [-(empty(empty_set))], (1408 ^ _329283) ^ [_378689, _378691] : [empty(ordered_pair(_378691, _378689))], (1410 ^ _329283) ^ [_378800, _378802] : [-(relation(set_union2(_378802, _378800))), relation(_378802), relation(_378800)], (1420 ^ _329283) ^ [_379069] : [empty(singleton(_379069))], (1422 ^ _329283) ^ [_379177, _379179] : [-(empty(_379179)), empty(set_union2(_379179, _379177))], (1428 ^ _329283) ^ [_379377, _379379] : [empty(unordered_pair(_379379, _379377))], (1430 ^ _329283) ^ [_379488, _379490] : [-(empty(_379490)), empty(set_union2(_379488, _379490))], (1436 ^ _329283) ^ [] : [-(empty(empty_set))], (1438 ^ _329283) ^ [] : [-(relation(empty_set))], (1440 ^ _329283) ^ [_379812, _379814] : [empty(cartesian_product2(_379814, _379812)), -(empty(_379814)), -(empty(_379812))], (1450 ^ _329283) ^ [_380104] : [empty(relation_dom(_380104)), -(empty(_380104)), relation(_380104)], (1460 ^ _329283) ^ [_380381] : [empty(relation_rng(_380381)), -(empty(_380381)), relation(_380381)], (1470 ^ _329283) ^ [_380658] : [empty(_380658), 1473 ^ _329283 : [(1474 ^ _329283) ^ [] : [-(empty(relation_dom(_380658)))], (1476 ^ _329283) ^ [] : [-(relation(relation_dom(_380658)))]]], (1478 ^ _329283) ^ [_380923] : [empty(_380923), 1481 ^ _329283 : [(1482 ^ _329283) ^ [] : [-(empty(relation_rng(_380923)))], (1484 ^ _329283) ^ [] : [-(relation(relation_rng(_380923)))]]], (1486 ^ _329283) ^ [_381202, _381204] : [1493 ^ _329283 : [(1494 ^ _329283) ^ [] : [-(empty(relation_composition(_381204, _381202)))], (1496 ^ _329283) ^ [] : [-(relation(relation_composition(_381204, _381202)))]], empty(_381204), relation(_381202)], (1498 ^ _329283) ^ [_381565, _381567] : [-(set_union2(_381567, _381567) = _381567)], (1500 ^ _329283) ^ [_381662, _381664] : [-(set_intersection2(_381664, _381664) = _381664)], (1502 ^ _329283) ^ [_381774, _381776] : [element(_381774, powerset(_381776)), -(subset_complement(_381776, subset_complement(_381776, _381774)) = _381774)], (1508 ^ _329283) ^ [_381986] : [relation(_381986), -(relation_inverse(relation_inverse(_381986)) = _381986)], (1514 ^ _329283) ^ [_382196, _382198] : [element(_382196, powerset(powerset(_382198))), -(complements_of_subsets(_382198, complements_of_subsets(_382198, _382196)) = _382196)], (1520 ^ _329283) ^ [_382410, _382412] : [proper_subset(_382412, _382412)], (1522 ^ _329283) ^ [_382489] : [singleton(_382489) = empty_set], (1524 ^ _329283) ^ [_382598, _382600] : [in(_382600, _382598), -(set_union2(singleton(_382600), _382598) = _382598)], (1530 ^ _329283) ^ [_382818, _382820] : [disjoint(singleton(_382820), _382818), in(_382820, _382818)], (1536 ^ _329283) ^ [_383031, _383033] : [-(in(_383033, _383031)), -(disjoint(singleton(_383033), _383031))], (1542 ^ _329283) ^ [_383277, _383279] : [subset(singleton(_383279), _383277), -(in(_383279, _383277))], (1548 ^ _329283) ^ [_383443, _383445] : [in(_383445, _383443), -(subset(singleton(_383445), _383443))], (1554 ^ _329283) ^ [_383688, _383690] : [set_difference(_383690, _383688) = empty_set, -(subset(_383690, _383688))], (1560 ^ _329283) ^ [_383856, _383858] : [subset(_383858, _383856), -(set_difference(_383858, _383856) = empty_set)], (1566 ^ _329283) ^ [_384074, _384076] : [element(_384074, powerset(_384076)), 1569 ^ _329283 : [(1570 ^ _329283) ^ [_384215] : [in(_384215, _384074), -(in(_384215, _384076))]]], (1576 ^ _329283) ^ [_384454, _384456, _384458] : [subset(_384458, _384456), -(in(_384454, _384458)), -(subset(_384458, set_difference(_384456, singleton(_384454))))], (1596 ^ _329283) ^ [_385063, _385065] : [1597 ^ _329283 : [(1598 ^ _329283) ^ [] : [_385065 = empty_set], (1600 ^ _329283) ^ [] : [_385065 = singleton(_385063)]], -(subset(_385065, singleton(_385063)))], (1586 ^ _329283) ^ [_384803, _384805] : [subset(_384805, singleton(_384803)), -(_384805 = empty_set), -(_384805 = singleton(_384803))], (1604 ^ _329283) ^ [_385357, _385359] : [in(_385359, _385357), -(subset(_385359, union(_385357)))], (1610 ^ _329283) ^ [_385628, _385630, _385632, _385634] : [in(ordered_pair(_385634, _385632), cartesian_product2(_385630, _385628)), 1613 ^ _329283 : [(1614 ^ _329283) ^ [] : [-(in(_385634, _385630))], (1616 ^ _329283) ^ [] : [-(in(_385632, _385628))]]], (1618 ^ _329283) ^ [_385893, _385895, _385897, _385899] : [-(in(ordered_pair(_385899, _385897), cartesian_product2(_385895, _385893))), in(_385899, _385895), in(_385897, _385893)], (1628 ^ _329283) ^ [_386226, _386228] : [1630 ^ _329283 : [(1631 ^ _329283) ^ [] : [-(in(1629 ^ [_386226, _386228], _386228))], (1633 ^ _329283) ^ [] : [in(1629 ^ [_386226, _386228], _386226)]], -(element(_386228, powerset(_386226)))], (1638 ^ _329283) ^ [] : [-(empty(1636 ^ []))], (1640 ^ _329283) ^ [] : [-(relation(1636 ^ []))], (1642 ^ _329283) ^ [_386720] : [-(empty(_386720)), 1646 ^ _329283 : [(1647 ^ _329283) ^ [] : [-(element(1645 ^ [_386720], powerset(_386720)))], (1649 ^ _329283) ^ [] : [empty(1645 ^ [_386720])]]], (1652 ^ _329283) ^ [] : [-(empty(1650 ^ []))], (1655 ^ _329283) ^ [] : [empty(1653 ^ [])], (1657 ^ _329283) ^ [] : [-(relation(1653 ^ []))], (1660 ^ _329283) ^ [_387342] : [-(element(1658 ^ [_387342], powerset(_387342)))], (1662 ^ _329283) ^ [_387393] : [-(empty(1658 ^ [_387393]))], (1665 ^ _329283) ^ [] : [empty(1663 ^ [])], (1667 ^ _329283) ^ [_387596, _387598] : [element(_387596, powerset(powerset(_387598))), -(union_of_subsets(_387598, _387596) = union(_387596))], (1673 ^ _329283) ^ [_387824, _387826] : [element(_387824, powerset(powerset(_387826))), -(meet_of_subsets(_387826, _387824) = set_meet(_387824))], (1679 ^ _329283) ^ [_388066, _388068, _388070] : [-(subset_difference(_388070, _388068, _388066) = set_difference(_388068, _388066)), element(_388068, powerset(_388070)), element(_388066, powerset(_388070))], (1689 ^ _329283) ^ [_388382, _388384] : [-(subset(_388384, _388384))], (1691 ^ _329283) ^ [_388491, _388493] : [disjoint(_388493, _388491), -(disjoint(_388491, _388493))], (1697 ^ _329283) ^ [_388758, _388760, _388762, _388764] : [in(ordered_pair(_388764, _388762), cartesian_product2(_388760, _388758)), 1700 ^ _329283 : [(1701 ^ _329283) ^ [] : [-(in(_388764, _388760))], (1703 ^ _329283) ^ [] : [-(in(_388762, _388758))]]], (1705 ^ _329283) ^ [_389023, _389025, _389027, _389029] : [-(in(ordered_pair(_389029, _389027), cartesian_product2(_389025, _389023))), in(_389029, _389025), in(_389027, _389023)], (1715 ^ _329283) ^ [_389384, _389386, _389388, _389390] : [unordered_pair(_389390, _389388) = unordered_pair(_389386, _389384), -(_389390 = _389386), -(_389390 = _389384)], (1725 ^ _329283) ^ [_389734, _389736, _389738] : [subset(_389738, _389736), 1728 ^ _329283 : [(1729 ^ _329283) ^ [] : [-(subset(cartesian_product2(_389738, _389734), cartesian_product2(_389736, _389734)))], (1731 ^ _329283) ^ [] : [-(subset(cartesian_product2(_389734, _389738), cartesian_product2(_389734, _389736)))]]], (1733 ^ _329283) ^ [_390079, _390081, _390083, _390085] : [-(subset(cartesian_product2(_390085, _390081), cartesian_product2(_390083, _390079))), subset(_390085, _390083), subset(_390081, _390079)], (1743 ^ _329283) ^ [_390410, _390412] : [subset(_390412, _390410), -(set_union2(_390412, _390410) = _390410)], (1750 ^ _329283) ^ [_390732] : [-(in(_390732, 1748 ^ [_390732]))], (1752 ^ _329283) ^ [_390844, _390846, _390848] : [-(in(_390844, 1748 ^ [_390848])), in(_390846, 1748 ^ [_390848]), subset(_390844, _390846)], (1762 ^ _329283) ^ [_391159, _391161] : [in(_391159, 1748 ^ [_391161]), -(in(powerset(_391159), 1748 ^ [_391161]))], (1768 ^ _329283) ^ [_391359, _391361] : [subset(_391359, 1748 ^ [_391361]), -(are_equipotent(_391359, 1748 ^ [_391361])), -(in(_391359, 1748 ^ [_391361]))], (1778 ^ _329283) ^ [_391684, _391686] : [-(subset(set_intersection2(_391686, _391684), _391686))], (1780 ^ _329283) ^ [_391810, _391812, _391814] : [-(subset(_391814, set_intersection2(_391812, _391810))), subset(_391814, _391812), subset(_391814, _391810)], (1790 ^ _329283) ^ [_392096] : [-(set_union2(_392096, empty_set) = _392096)], (1792 ^ _329283) ^ [_392206, _392208] : [in(_392208, _392206), -(element(_392208, _392206))], (1798 ^ _329283) ^ [_392430, _392432, _392434] : [-(subset(_392434, _392430)), subset(_392434, _392432), subset(_392432, _392430)], (1808 ^ _329283) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (1810 ^ _329283) ^ [_392806, _392808, _392810] : [relation(_392806), in(ordered_pair(_392810, _392808), _392806), 1817 ^ _329283 : [(1818 ^ _329283) ^ [] : [-(in(_392810, relation_dom(_392806)))], (1820 ^ _329283) ^ [] : [-(in(_392808, relation_rng(_392806)))]]], (1822 ^ _329283) ^ [_393190] : [relation(_393190), -(subset(_393190, cartesian_product2(relation_dom(_393190), relation_rng(_393190))))], (1828 ^ _329283) ^ [_393392] : [relation(_393392), 1831 ^ _329283 : [(1832 ^ _329283) ^ [_393542] : [relation(_393542), subset(_393392, _393542), 1839 ^ _329283 : [(1840 ^ _329283) ^ [] : [-(subset(relation_dom(_393392), relation_dom(_393542)))], (1842 ^ _329283) ^ [] : [-(subset(relation_rng(_393392), relation_rng(_393542)))]]]]], (1844 ^ _329283) ^ [_393951, _393953, _393955] : [subset(_393955, _393953), -(subset(set_intersection2(_393955, _393951), set_intersection2(_393953, _393951)))], (1850 ^ _329283) ^ [_394179, _394181] : [subset(_394181, _394179), -(set_intersection2(_394181, _394179) = _394181)], (1856 ^ _329283) ^ [_394366] : [-(set_intersection2(_394366, empty_set) = empty_set)], (1858 ^ _329283) ^ [_394476, _394478] : [element(_394478, _394476), -(empty(_394476)), -(in(_394478, _394476))], (1868 ^ _329283) ^ [_394774, _394776] : [-(_394776 = _394774), 1872 ^ _329283 : [(1873 ^ _329283) ^ [] : [-(in(1869 ^ [_394774, _394776], _394776))], (1875 ^ _329283) ^ [] : [in(1869 ^ [_394774, _394776], _394774)]], 1876 ^ _329283 : [(1877 ^ _329283) ^ [] : [-(in(1869 ^ [_394774, _394776], _394774))], (1879 ^ _329283) ^ [] : [in(1869 ^ [_394774, _394776], _394776)]]], (1883 ^ _329283) ^ [_395275] : [-(subset(empty_set, _395275))], (1885 ^ _329283) ^ [_395396, _395398, _395400] : [relation(_395396), in(ordered_pair(_395400, _395398), _395396), 1892 ^ _329283 : [(1893 ^ _329283) ^ [] : [-(in(_395400, relation_field(_395396)))], (1895 ^ _329283) ^ [] : [-(in(_395398, relation_field(_395396)))]]], (1897 ^ _329283) ^ [_395808, _395810, _395812] : [subset(_395812, _395810), -(subset(set_difference(_395812, _395808), set_difference(_395810, _395808)))], (1903 ^ _329283) ^ [_396064, _396066, _396068, _396070] : [ordered_pair(_396070, _396068) = ordered_pair(_396066, _396064), 1906 ^ _329283 : [(1907 ^ _329283) ^ [] : [-(_396070 = _396066)], (1909 ^ _329283) ^ [] : [-(_396068 = _396064)]]], (1911 ^ _329283) ^ [_396362, _396364] : [-(subset(set_difference(_396364, _396362), _396364))], (1913 ^ _329283) ^ [_396460] : [relation(_396460), 1916 ^ _329283 : [(1917 ^ _329283) ^ [] : [-(relation_rng(_396460) = relation_dom(relation_inverse(_396460)))], (1919 ^ _329283) ^ [] : [-(relation_dom(_396460) = relation_rng(relation_inverse(_396460)))]]], (1921 ^ _329283) ^ [_396788, _396790] : [set_difference(_396790, _396788) = empty_set, -(subset(_396790, _396788))], (1927 ^ _329283) ^ [_396956, _396958] : [subset(_396958, _396956), -(set_difference(_396958, _396956) = empty_set)], (1933 ^ _329283) ^ [_397203, _397205] : [subset(singleton(_397205), _397203), -(in(_397205, _397203))], (1939 ^ _329283) ^ [_397369, _397371] : [in(_397371, _397369), -(subset(singleton(_397371), _397369))], (1945 ^ _329283) ^ [_397628, _397630, _397632] : [subset(unordered_pair(_397632, _397630), _397628), 1948 ^ _329283 : [(1949 ^ _329283) ^ [] : [-(in(_397632, _397628))], (1951 ^ _329283) ^ [] : [-(in(_397630, _397628))]]], (1953 ^ _329283) ^ [_397879, _397881, _397883] : [-(subset(unordered_pair(_397883, _397881), _397879)), in(_397883, _397879), in(_397881, _397879)], (1963 ^ _329283) ^ [_398181, _398183] : [-(set_union2(_398183, set_difference(_398181, _398183)) = set_union2(_398183, _398181))], (1975 ^ _329283) ^ [_398588, _398590] : [1976 ^ _329283 : [(1977 ^ _329283) ^ [] : [_398590 = empty_set], (1979 ^ _329283) ^ [] : [_398590 = singleton(_398588)]], -(subset(_398590, singleton(_398588)))], (1965 ^ _329283) ^ [_398328, _398330] : [subset(_398330, singleton(_398328)), -(_398330 = empty_set), -(_398330 = singleton(_398328))], (1983 ^ _329283) ^ [_398853] : [-(set_difference(_398853, empty_set) = _398853)], (1985 ^ _329283) ^ [_398992, _398994] : [element(_398994, powerset(_398992)), -(subset(_398994, _398992))], (1991 ^ _329283) ^ [_399158, _399160] : [subset(_399160, _399158), -(element(_399160, powerset(_399158)))], (1997 ^ _329283) ^ [_399394, _399396] : [-(disjoint(_399396, _399394)), 2001 ^ _329283 : [(2002 ^ _329283) ^ [] : [-(in(2000 ^ [_399394, _399396], _399396))], (2004 ^ _329283) ^ [] : [-(in(2000 ^ [_399394, _399396], _399394))]]], (2006 ^ _329283) ^ [_399708, _399710] : [disjoint(_399710, _399708), 2007 ^ _329283 : [(2008 ^ _329283) ^ [_399800] : [in(_399800, _399710), in(_399800, _399708)]]], (2016 ^ _329283) ^ [_400057] : [subset(_400057, empty_set), -(_400057 = empty_set)], (2022 ^ _329283) ^ [_400246, _400248] : [-(set_difference(set_union2(_400248, _400246), _400246) = set_difference(_400248, _400246))], (2024 ^ _329283) ^ [_400364, _400366] : [element(_400364, powerset(_400366)), 2027 ^ _329283 : [(2028 ^ _329283) ^ [_400516] : [element(_400516, powerset(_400366)), 2031 ^ _329283 : [(2032 ^ _329283) ^ [] : [disjoint(_400364, _400516), -(subset(_400364, subset_complement(_400366, _400516)))], (2038 ^ _329283) ^ [] : [subset(_400364, subset_complement(_400366, _400516)), -(disjoint(_400364, _400516))]]]]], (2044 ^ _329283) ^ [_401000] : [relation(_401000), 2047 ^ _329283 : [(2048 ^ _329283) ^ [_401137] : [relation(_401137), -(subset(relation_dom(relation_composition(_401000, _401137)), relation_dom(_401000)))]]], (2054 ^ _329283) ^ [_401352] : [relation(_401352), 2057 ^ _329283 : [(2058 ^ _329283) ^ [_401489] : [relation(_401489), -(subset(relation_rng(relation_composition(_401352, _401489)), relation_rng(_401489)))]]], (2064 ^ _329283) ^ [_401718, _401720] : [subset(_401720, _401718), -(_401718 = set_union2(_401720, set_difference(_401718, _401720)))], (2070 ^ _329283) ^ [_401926] : [relation(_401926), 2073 ^ _329283 : [(2074 ^ _329283) ^ [_402073] : [relation(_402073), subset(relation_rng(_401926), relation_dom(_402073)), -(relation_dom(relation_composition(_401926, _402073)) = relation_dom(_401926))]]], (2084 ^ _329283) ^ [_402399, _402401] : [element(_402399, powerset(powerset(_402401))), -(_402399 = empty_set), complements_of_subsets(_402401, _402399) = empty_set], (2094 ^ _329283) ^ [_402716, _402718] : [in(_402718, _402716), -(set_union2(singleton(_402718), _402716) = _402716)], (2100 ^ _329283) ^ [_402922] : [relation(_402922), 2103 ^ _329283 : [(2104 ^ _329283) ^ [_403069] : [relation(_403069), subset(relation_dom(_402922), relation_rng(_403069)), -(relation_rng(relation_composition(_403069, _402922)) = relation_rng(_402922))]]], (2114 ^ _329283) ^ [_403395, _403397] : [element(_403395, powerset(powerset(_403397))), -(_403395 = empty_set), -(subset_difference(_403397, cast_to_subset(_403397), union_of_subsets(_403397, _403395)) = meet_of_subsets(_403397, complements_of_subsets(_403397, _403395)))], (2124 ^ _329283) ^ [_403735, _403737] : [element(_403735, powerset(powerset(_403737))), -(_403735 = empty_set), -(union_of_subsets(_403737, complements_of_subsets(_403737, _403735)) = subset_difference(_403737, cast_to_subset(_403737), meet_of_subsets(_403737, _403735)))], (2134 ^ _329283) ^ [_404060, _404062] : [-(set_difference(_404062, set_difference(_404062, _404060)) = set_intersection2(_404062, _404060))], (2136 ^ _329283) ^ [_404149] : [-(set_difference(empty_set, _404149) = empty_set)], (2138 ^ _329283) ^ [_404273, _404275, _404277] : [-(element(_404277, _404273)), in(_404277, _404275), element(_404275, powerset(_404273))], (2148 ^ _329283) ^ [_404606, _404608] : [-(disjoint(_404608, _404606)), -(in(2151 ^ [_404606, _404608], set_intersection2(_404608, _404606)))], (2155 ^ _329283) ^ [_404841, _404843] : [2156 ^ _329283 : [(2157 ^ _329283) ^ [_404914] : [in(_404914, set_intersection2(_404843, _404841))]], disjoint(_404843, _404841)], (2161 ^ _329283) ^ [_405066] : [-(_405066 = empty_set), 2164 ^ _329283 : [(2165 ^ _329283) ^ [_405226] : [element(_405226, powerset(_405066)), 2168 ^ _329283 : [(2169 ^ _329283) ^ [_405380] : [element(_405380, _405066), -(in(_405380, _405226)), -(in(_405380, subset_complement(_405066, _405226)))]]]]], (2179 ^ _329283) ^ [_405726, _405728, _405730] : [element(_405726, powerset(_405730)), in(_405728, subset_complement(_405730, _405726)), in(_405728, _405726)], (2189 ^ _329283) ^ [_406032] : [relation(_406032), -(in(ordered_pair(2194 ^ [_406032], 2195 ^ [_406032]), _406032)), -(_406032 = empty_set)], (2201 ^ _329283) ^ [_406464, _406466, _406468] : [in(_406468, _406466), element(_406466, powerset(_406464)), empty(_406464)], (2211 ^ _329283) ^ [] : [-(relation_dom(empty_set) = empty_set)], (2213 ^ _329283) ^ [] : [-(relation_rng(empty_set) = empty_set)], (2215 ^ _329283) ^ [_406882, _406884] : [subset(_406884, _406882), proper_subset(_406882, _406884)], (2221 ^ _329283) ^ [_407105, _407107, _407109] : [-(disjoint(_407109, _407105)), subset(_407109, _407107), disjoint(_407107, _407105)], (2231 ^ _329283) ^ [_407400] : [relation(_407400), 2236 ^ _329283 : [(2237 ^ _329283) ^ [] : [relation_dom(_407400) = empty_set], (2239 ^ _329283) ^ [] : [relation_rng(_407400) = empty_set]], -(_407400 = empty_set)], (2243 ^ _329283) ^ [_407753] : [relation(_407753), 2246 ^ _329283 : [(2247 ^ _329283) ^ [] : [relation_dom(_407753) = empty_set, -(relation_rng(_407753) = empty_set)], (2253 ^ _329283) ^ [] : [relation_rng(_407753) = empty_set, -(relation_dom(_407753) = empty_set)]]], (2259 ^ _329283) ^ [_408236, _408238] : [set_difference(_408238, singleton(_408236)) = _408238, in(_408236, _408238)], (2265 ^ _329283) ^ [_408409, _408411] : [-(in(_408409, _408411)), -(set_difference(_408411, singleton(_408409)) = _408411)], (2271 ^ _329283) ^ [_408605] : [-(unordered_pair(_408605, _408605) = singleton(_408605))], (2273 ^ _329283) ^ [_408703] : [empty(_408703), -(_408703 = empty_set)], (2279 ^ _329283) ^ [_408905, _408907] : [subset(singleton(_408907), singleton(_408905)), -(_408907 = _408905)], (2285 ^ _329283) ^ [_409114] : [-(relation_dom(identity_relation(_409114)) = _409114)], (2287 ^ _329283) ^ [_409162] : [-(relation_rng(identity_relation(_409162)) = _409162)], (2289 ^ _329283) ^ [_409303, _409305, _409307, _409309] : [relation(_409303), 2292 ^ _329283 : [(2293 ^ _329283) ^ [] : [in(ordered_pair(_409309, _409307), relation_composition(identity_relation(_409305), _409303)), 2296 ^ _329283 : [(2297 ^ _329283) ^ [] : [-(in(_409309, _409305))], (2299 ^ _329283) ^ [] : [-(in(ordered_pair(_409309, _409307), _409303))]]], (2301 ^ _329283) ^ [] : [-(in(ordered_pair(_409309, _409307), relation_composition(identity_relation(_409305), _409303))), in(_409309, _409305), in(ordered_pair(_409309, _409307), _409303)]]], (2311 ^ _329283) ^ [_409996, _409998] : [in(_409998, _409996), empty(_409996)], (2317 ^ _329283) ^ [_410188, _410190] : [-(subset(_410190, set_union2(_410190, _410188)))], (2319 ^ _329283) ^ [_410329, _410331] : [disjoint(_410331, _410329), -(set_difference(_410331, _410329) = _410331)], (2325 ^ _329283) ^ [_410497, _410499] : [set_difference(_410499, _410497) = _410499, -(disjoint(_410499, _410497))], (2331 ^ _329283) ^ [_410729, _410731, _410733] : [relation(_410729), 2334 ^ _329283 : [(2335 ^ _329283) ^ [] : [in(_410733, relation_dom(relation_dom_restriction(_410729, _410731))), 2338 ^ _329283 : [(2339 ^ _329283) ^ [] : [-(in(_410733, _410731))], (2341 ^ _329283) ^ [] : [-(in(_410733, relation_dom(_410729)))]]], (2343 ^ _329283) ^ [] : [-(in(_410733, relation_dom(relation_dom_restriction(_410729, _410731)))), in(_410733, _410731), in(_410733, relation_dom(_410729))]]], (2353 ^ _329283) ^ [_411388, _411390] : [empty(_411390), -(_411390 = _411388), empty(_411388)], (2363 ^ _329283) ^ [_411699, _411701, _411703] : [-(subset(set_union2(_411703, _411699), _411701)), subset(_411703, _411701), subset(_411699, _411701)], (2373 ^ _329283) ^ [_412028, _412030, _412032] : [singleton(_412032) = unordered_pair(_412030, _412028), -(_412032 = _412030)], (2379 ^ _329283) ^ [_412254, _412256] : [in(_412256, _412254), -(subset(_412256, union(_412254)))], (2385 ^ _329283) ^ [_412439] : [-(union(powerset(_412439)) = _412439)], (2423 ^ _329283) ^ [_413960, _413962, _413964] : [singleton(_413964) = unordered_pair(_413962, _413960), -(_413962 = _413960)], (2388 ^ _329283) ^ [_412680] : [-(in(_412680, 2386 ^ [_412680]))], (2390 ^ _329283) ^ [_412792, _412794, _412796] : [-(in(_412792, 2386 ^ [_412796])), in(_412794, 2386 ^ [_412796]), subset(_412792, _412794)], (2400 ^ _329283) ^ [_413107, _413109] : [in(_413107, 2386 ^ [_413109]), 2404 ^ _329283 : [(2405 ^ _329283) ^ [] : [-(in(2403 ^ [_413107, _413109], 2386 ^ [_413109]))], (2407 ^ _329283) ^ [_413419] : [subset(_413419, _413107), -(in(_413419, 2403 ^ [_413107, _413109]))]]], (2413 ^ _329283) ^ [_413626, _413628] : [subset(_413626, 2386 ^ [_413628]), -(are_equipotent(_413626, 2386 ^ [_413628])), -(in(_413626, 2386 ^ [_413628]))]], input).
% 6.23/6.55 ncf('1',plain,[subset(relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ [])],start(2433 ^ 0)).
% 6.23/6.55 ncf('1.1',plain,[-(subset(relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ [])), 822 : in(ordered_pair(817 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []], 818 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []]), 2429 ^ []), 816 : relation(2429 ^ []), 802 : relation(relation_dom_restriction(2429 ^ [], 2428 ^ []))],extension(798 ^ 1,bind([[_357632, _357790], [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []]]))).
% 6.23/6.55 ncf('1.1.1',plain,[-(in(ordered_pair(817 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []], 818 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []]), 2429 ^ [])), 420 : in(ordered_pair(817 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []], 818 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []]), relation_dom_restriction(2429 ^ [], 2428 ^ [])), 420 : relation_dom_restriction(2429 ^ [], 2428 ^ []) = relation_dom_restriction(2429 ^ [], 2428 ^ []), 416 : relation(relation_dom_restriction(2429 ^ [], 2428 ^ [])), 412 : relation(2429 ^ [])],extension(408 ^ 8,bind([[_343504, _343690, _343692, _344015, _344017], [2429 ^ [], relation_dom_restriction(2429 ^ [], 2428 ^ []), 2428 ^ [], 818 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []], 817 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []]]]))).
% 6.23/6.55 ncf('1.1.1.1',plain,[-(in(ordered_pair(817 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []], 818 ^ [relation_dom_restriction(2429 ^ [], 2428 ^ []), 2429 ^ []]), relation_dom_restriction(2429 ^ [], 2428 ^ [])))],extension(820 ^ 15)).
% 6.23/6.55 ncf('1.1.1.2',plain,[-(relation_dom_restriction(2429 ^ [], 2428 ^ []) = relation_dom_restriction(2429 ^ [], 2428 ^ []))],extension(2 ^ 13,bind([[_329427], [relation_dom_restriction(2429 ^ [], 2428 ^ [])]]))).
% 6.23/6.55 ncf('1.1.1.3',plain,[-(relation(relation_dom_restriction(2429 ^ [], 2428 ^ []))), relation(2429 ^ [])],extension(1371 ^ 11,bind([[_377511, _377513], [2428 ^ [], 2429 ^ []]]))).
% 6.23/6.55 ncf('1.1.1.3.1',plain,[-(relation(2429 ^ []))],extension(2431 ^ 12)).
% 6.23/6.55 ncf('1.1.1.4',plain,[-(relation(2429 ^ []))],extension(2431 ^ 9)).
% 6.23/6.55 ncf('1.1.2',plain,[-(relation(2429 ^ []))],extension(2431 ^ 4)).
% 6.23/6.55 ncf('1.1.3',plain,[-(relation(relation_dom_restriction(2429 ^ [], 2428 ^ []))), relation(2429 ^ [])],extension(1371 ^ 2,bind([[_377511, _377513], [2428 ^ [], 2429 ^ []]]))).
% 6.23/6.55 ncf('1.1.3.1',plain,[-(relation(2429 ^ []))],extension(2431 ^ 3)).
% 6.23/6.55 %-----------------------------------------------------
% 6.23/6.55 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------