%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU188+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:34 EDT 2023
% Result : Theorem 46.45s 45.82s
% Output : Proof 46.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU188+2 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n031.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 13:43:55 EDT 2023
% 0.12/0.34 % CPUTime :
% 46.45/45.82
% 46.45/45.82 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 46.45/45.82 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.45/45.82 %-----------------------------------------------------
% 46.45/45.82 ncf(matrix, plain, [(2180 ^ _403397) ^ [] : [-(relation_dom(2176 ^ []) = empty_set), -(relation_rng(2176 ^ []) = empty_set)], (2186 ^ _403397) ^ [] : [2176 ^ [] = empty_set], (2178 ^ _403397) ^ [] : [-(relation(2176 ^ []))], !, (580 ^ _325860) ^ [_345997, _345999, _346001] : [_345997 = set_union2(_346001, _345999), 583 ^ _325860 : [(584 ^ _325860) ^ [_346179] : [in(_346179, _345997), -(in(_346179, _346001)), -(in(_346179, _345999))], (594 ^ _325860) ^ [_346457] : [595 ^ _325860 : [(598 ^ _325860) ^ [] : [in(_346457, _345999)], (596 ^ _325860) ^ [] : [in(_346457, _346001)]], -(in(_346457, _345997))]]], (1622 ^ _325860) ^ [_382718, _382720, _382722] : [-(subset(_382722, _382718)), subset(_382722, _382720), subset(_382720, _382718)], (1513 ^ _325860) ^ [_378670, _378672] : [-(subset(_378672, _378672))], (467 ^ _325860) ^ [_342197] : [-(in(468 ^ [_342197], _342197)), -(_342197 = empty_set)], (1646 ^ _325860) ^ [_383478] : [relation(_383478), -(subset(_383478, cartesian_product2(relation_dom(_383478), relation_rng(_383478))))], (1276 ^ _325860) ^ [_370478, _370480] : [empty(cartesian_product2(_370480, _370478)), -(empty(_370480)), -(empty(_370478))], (1586 ^ _325860) ^ [_381447, _381449] : [in(_381447, 1572 ^ [_381449]), -(in(powerset(_381447), 1572 ^ [_381449]))], (140 ^ _325860) ^ [_330439, _330441] : [_330441 = _330439, -(relation_field(_330441) = relation_field(_330439))], (124 ^ _325860) ^ [_329862, _329864] : [_329864 = _329862, -(set_meet(_329864) = set_meet(_329862))], (365 ^ _325860) ^ [_338742, _338744] : [-(_338744 = empty_set), 368 ^ _325860 : [(369 ^ _325860) ^ [] : [_338742 = set_meet(_338744), 372 ^ _325860 : [(373 ^ _325860) ^ [_339040] : [in(_339040, _338742), 376 ^ _325860 : [(377 ^ _325860) ^ [_339185] : [in(_339185, _338744), -(in(_339040, _339185))]]], (383 ^ _325860) ^ [_339370] : [385 ^ _325860 : [(388 ^ _325860) ^ [] : [in(_339370, 384 ^ [_338742, _338744, _339370])], (386 ^ _325860) ^ [] : [-(in(384 ^ [_338742, _338744, _339370], _338744))]], -(in(_339370, _338742))]]], (392 ^ _325860) ^ [] : [-(_338742 = set_meet(_338744)), 396 ^ _325860 : [(402 ^ _325860) ^ [] : [in(393 ^ [_338742, _338744], 398 ^ [_338742, _338744])], (400 ^ _325860) ^ [] : [-(in(398 ^ [_338742, _338744], _338744))], (397 ^ _325860) ^ [] : [-(in(393 ^ [_338742, _338744], _338742))]], 403 ^ _325860 : [(404 ^ _325860) ^ [_340144] : [in(_340144, _338744), -(in(393 ^ [_338742, _338744], _340144))], (410 ^ _325860) ^ [] : [in(393 ^ [_338742, _338744], _338742)]]]]], (1360 ^ _325860) ^ [_373319, _373321] : [-(in(_373321, _373319)), -(disjoint(singleton(_373321), _373319))], (1962 ^ _325860) ^ [_394561, _394563, _394565] : [-(element(_394565, _394561)), in(_394565, _394563), element(_394563, powerset(_394561))], (723 ^ _325860) ^ [_351489, _351491, _351493] : [-(_351489 = set_intersection2(_351493, _351491)), 735 ^ _325860 : [(740 ^ _325860) ^ [] : [in(724 ^ [_351489, _351491, _351493], _351489)], (738 ^ _325860) ^ [] : [-(in(724 ^ [_351489, _351491, _351493], _351491))], (736 ^ _325860) ^ [] : [-(in(724 ^ [_351489, _351491, _351493], _351493))]], 727 ^ _325860 : [(730 ^ _325860) ^ [] : [in(724 ^ [_351489, _351491, _351493], _351493), in(724 ^ [_351489, _351491, _351493], _351491)], (728 ^ _325860) ^ [] : [-(in(724 ^ [_351489, _351491, _351493], _351489))]]], (1682 ^ _325860) ^ [_384764, _384766] : [element(_384766, _384764), -(empty(_384764)), -(in(_384766, _384764))], (344 ^ _325860) ^ [_337853] : [relation(_337853), 347 ^ _325860 : [(348 ^ _325860) ^ [_338001] : [in(_338001, _337853), -(_338001 = ordered_pair(351 ^ [_337853, _338001], 352 ^ [_337853, _338001]))]]], (1751 ^ _325860) ^ [_387244, _387246] : [subset(_387246, _387244), -(set_difference(_387246, _387244) = empty_set)], (1169 ^ _325860) ^ [] : [true___, -(true___)], (1306 ^ _325860) ^ [_371324] : [empty(_371324), 1309 ^ _325860 : [(1312 ^ _325860) ^ [] : [-(relation(relation_dom(_371324)))], (1310 ^ _325860) ^ [] : [-(empty(relation_dom(_371324)))]]], (10 ^ _325860) ^ [_326295, _326297, _326299] : [-(_326299 = _326295), _326299 = _326297, _326297 = _326295], (1769 ^ _325860) ^ [_387916, _387918, _387920] : [subset(unordered_pair(_387920, _387918), _387916), 1772 ^ _325860 : [(1775 ^ _325860) ^ [] : [-(in(_387918, _387916))], (1773 ^ _325860) ^ [] : [-(in(_387920, _387916))]]], (1157 ^ _325860) ^ [_366779, _366781] : [element(_366779, powerset(_366781)), -(element(subset_complement(_366781, _366779), powerset(_366781)))], (1668 ^ _325860) ^ [_384239, _384241, _384243] : [subset(_384243, _384241), -(subset(set_intersection2(_384243, _384239), set_intersection2(_384241, _384239)))], (1175 ^ _325860) ^ [_367227] : [relation(_367227), -(relation(relation_inverse(_367227)))], (1378 ^ _325860) ^ [_373976, _373978] : [set_difference(_373978, _373976) = empty_set, -(subset(_373978, _373976))], (1735 ^ _325860) ^ [_386650, _386652] : [-(subset(set_difference(_386652, _386650), _386652))], (1476 ^ _325860) ^ [] : [-(empty(1474 ^ []))], (1452 ^ _325860) ^ [_376514, _376516] : [1454 ^ _325860 : [(1457 ^ _325860) ^ [] : [in(1453 ^ [_376514, _376516], _376514)], (1455 ^ _325860) ^ [] : [-(in(1453 ^ [_376514, _376516], _376516))]], -(element(_376516, powerset(_376514)))], (1231 ^ _325860) ^ [] : [true___, -(true___)], (172 ^ _325860) ^ [_331621, _331623, _331625, _331627] : [-(complements_of_subsets(_331627, _331623) = complements_of_subsets(_331625, _331621)), _331627 = _331625, _331623 = _331621], (1256 ^ _325860) ^ [_369735] : [empty(singleton(_369735))], (86 ^ _325860) ^ [_328707, _328709, _328711, _328713] : [-(are_equipotent(_328711, _328707)), are_equipotent(_328713, _328709), _328713 = _328711, _328709 = _328707], (1095 ^ _325860) ^ [] : [true___, -(true___)], (4 ^ _325860) ^ [_326091, _326093] : [_326093 = _326091, -(_326091 = _326093)], (1787 ^ _325860) ^ [_388469, _388471] : [-(set_union2(_388471, set_difference(_388469, _388471)) = set_union2(_388471, _388469))], (1286 ^ _325860) ^ [_370770] : [empty(relation_dom(_370770)), -(empty(_370770)), relation(_370770)], (1549 ^ _325860) ^ [_380022, _380024, _380026] : [subset(_380026, _380024), 1552 ^ _325860 : [(1555 ^ _325860) ^ [] : [-(subset(cartesian_product2(_380022, _380026), cartesian_product2(_380022, _380024)))], (1553 ^ _325860) ^ [] : [-(subset(cartesian_product2(_380026, _380022), cartesian_product2(_380024, _380022)))]]], (1680 ^ _325860) ^ [_384654] : [-(set_intersection2(_384654, empty_set) = empty_set)], (1032 ^ _325860) ^ [_363374, _363376] : [element(_363374, powerset(powerset(_363376))), 1035 ^ _325860 : [(1036 ^ _325860) ^ [_363554] : [element(_363554, powerset(powerset(_363376))), 1039 ^ _325860 : [(1040 ^ _325860) ^ [] : [_363554 = complements_of_subsets(_363376, _363374), 1043 ^ _325860 : [(1044 ^ _325860) ^ [_363842] : [element(_363842, powerset(_363376)), 1047 ^ _325860 : [(1054 ^ _325860) ^ [] : [in(subset_complement(_363376, _363842), _363374), -(in(_363842, _363554))], (1048 ^ _325860) ^ [] : [in(_363842, _363554), -(in(subset_complement(_363376, _363842), _363374))]]]]], (1060 ^ _325860) ^ [] : [-(_363554 = complements_of_subsets(_363376, _363374)), 1062 ^ _325860 : [(1065 ^ _325860) ^ [] : [1066 ^ _325860 : [(1069 ^ _325860) ^ [] : [in(subset_complement(_363376, 1061 ^ [_363374, _363376, _363554]), _363374)], (1067 ^ _325860) ^ [] : [-(in(1061 ^ [_363374, _363376, _363554], _363554))]], 1070 ^ _325860 : [(1073 ^ _325860) ^ [] : [in(1061 ^ [_363374, _363376, _363554], _363554)], (1071 ^ _325860) ^ [] : [-(in(subset_complement(_363376, 1061 ^ [_363374, _363376, _363554]), _363374))]]], (1063 ^ _325860) ^ [] : [-(element(1061 ^ [_363374, _363376, _363554], powerset(_363376)))]]]]]]], (2101 ^ _325860) ^ [_399337, _399339] : [empty(_399339), -(_399339 = _399337), empty(_399337)], (2013 ^ _325860) ^ [_396320] : [relation(_396320), -(in(ordered_pair(2018 ^ [_396320], 2019 ^ [_396320]), _396320)), -(_396320 = empty_set)], (334 ^ _325860) ^ [_337537, _337539] : [-(_337539 = _337537), subset(_337539, _337537), subset(_337537, _337539)], (1131 ^ _325860) ^ [_366192] : [-(element(cast_to_subset(_366192), powerset(_366192)))], (114 ^ _325860) ^ [_329547, _329549] : [-(relation(_329547)), _329549 = _329547, relation(_329549)], (1894 ^ _325860) ^ [_392214] : [relation(_392214), 1897 ^ _325860 : [(1898 ^ _325860) ^ [_392361] : [relation(_392361), subset(relation_rng(_392214), relation_dom(_392361)), -(relation_dom(relation_composition(_392214, _392361)) = relation_dom(_392214))]]], (2025 ^ _325860) ^ [_396752, _396754, _396756] : [in(_396756, _396754), element(_396754, powerset(_396752)), empty(_396752)], (701 ^ _325860) ^ [_350764, _350766, _350768] : [_350764 = set_intersection2(_350768, _350766), 704 ^ _325860 : [(713 ^ _325860) ^ [_351205] : [-(in(_351205, _350764)), in(_351205, _350768), in(_351205, _350766)], (705 ^ _325860) ^ [_350946] : [in(_350946, _350764), 708 ^ _325860 : [(711 ^ _325860) ^ [] : [-(in(_350946, _350766))], (709 ^ _325860) ^ [] : [-(in(_350946, _350768))]]]]], (1503 ^ _325860) ^ [_378354, _378356, _378358] : [-(subset_difference(_378358, _378356, _378354) = set_difference(_378356, _378354)), element(_378356, powerset(_378358)), element(_378354, powerset(_378358))], (1466 ^ _325860) ^ [_377008] : [-(empty(_377008)), 1470 ^ _325860 : [(1473 ^ _325860) ^ [] : [empty(1469 ^ [_377008])], (1471 ^ _325860) ^ [] : [-(element(1469 ^ [_377008], powerset(_377008)))]]], (1539 ^ _325860) ^ [_379672, _379674, _379676, _379678] : [unordered_pair(_379678, _379676) = unordered_pair(_379674, _379672), -(_379678 = _379674), -(_379678 = _379672)], (2138 ^ _325860) ^ [_400741, _400743, _400745] : [-(in(_400741, 2134 ^ [_400745])), in(_400743, 2134 ^ [_400745]), subset(_400741, _400743)], (48 ^ _325860) ^ [_327524, _327526, _327528, _327530] : [-(disjoint(_327528, _327524)), disjoint(_327530, _327526), _327530 = _327528, _327526 = _327524], (1428 ^ _325860) ^ [_375645, _375647] : [in(_375647, _375645), -(subset(_375647, union(_375645)))], (1244 ^ _325860) ^ [_369355, _369357] : [empty(ordered_pair(_369357, _369355))], (356 ^ _325860) ^ [_338314] : [358 ^ _325860 : [(361 ^ _325860) ^ [_338551, _338553] : [357 ^ [_338314] = ordered_pair(_338553, _338551)], (359 ^ _325860) ^ [] : [-(in(357 ^ [_338314], _338314))]], -(relation(_338314))], (1151 ^ _325860) ^ [] : [true___, -(true___)], (1163 ^ _325860) ^ [] : [true___, -(true___)], (1240 ^ _325860) ^ [_369210] : [empty(powerset(_369210))], (1815 ^ _325860) ^ [_389446, _389448] : [subset(_389448, _389446), -(element(_389448, powerset(_389446)))], (1938 ^ _325860) ^ [_393683, _393685] : [element(_393683, powerset(powerset(_393685))), -(_393683 = empty_set), -(subset_difference(_393685, cast_to_subset(_393685), union_of_subsets(_393685, _393683)) = meet_of_subsets(_393685, complements_of_subsets(_393685, _393683)))], (1576 ^ _325860) ^ [_381132, _381134, _381136] : [-(in(_381132, 1572 ^ [_381136])), in(_381134, 1572 ^ [_381136]), subset(_381132, _381134)], (196 ^ _325860) ^ [_332468, _332470] : [_332470 = _332468, -(cast_to_subset(_332470) = cast_to_subset(_332468))], (2055 ^ _325860) ^ [_397731, _397733] : [set_difference(_397733, singleton(_397731)) = _397733, in(_397731, _397733)], (1972 ^ _325860) ^ [_394894, _394896] : [-(disjoint(_394896, _394894)), -(in(1975 ^ [_394894, _394896], set_intersection2(_394896, _394894)))], (1985 ^ _325860) ^ [_395354] : [-(_395354 = empty_set), 1988 ^ _325860 : [(1989 ^ _325860) ^ [_395514] : [element(_395514, powerset(_395354)), 1992 ^ _325860 : [(1993 ^ _325860) ^ [_395668] : [element(_395668, _395354), -(in(_395668, _395514)), -(in(_395668, subset_complement(_395354, _395514)))]]]]], (1777 ^ _325860) ^ [_388167, _388169, _388171] : [-(subset(unordered_pair(_388171, _388169), _388167)), in(_388171, _388167), in(_388169, _388167)], (2075 ^ _325860) ^ [_398400, _398402] : [subset(singleton(_398402), singleton(_398400)), -(_398402 = _398400)], (1604 ^ _325860) ^ [_382098, _382100, _382102] : [-(subset(_382102, set_intersection2(_382100, _382098))), subset(_382102, _382100), subset(_382102, _382098)], (1721 ^ _325860) ^ [_386096, _386098, _386100] : [subset(_386100, _386098), -(subset(set_difference(_386100, _386096), set_difference(_386098, _386096)))], (1616 ^ _325860) ^ [_382494, _382496] : [in(_382496, _382494), -(element(_382496, _382494))], (430 ^ _325860) ^ [_340946, _340948] : [_340946 = singleton(_340948), 433 ^ _325860 : [(440 ^ _325860) ^ [_341288] : [_341288 = _340948, -(in(_341288, _340946))], (434 ^ _325860) ^ [_341116] : [in(_341116, _340946), -(_341116 = _340948)]]], (1420 ^ _325860) ^ [_375351, _375353] : [1421 ^ _325860 : [(1424 ^ _325860) ^ [] : [_375353 = singleton(_375351)], (1422 ^ _325860) ^ [] : [_375353 = empty_set]], -(subset(_375353, singleton(_375351)))], (1652 ^ _325860) ^ [_383680] : [relation(_383680), 1655 ^ _325860 : [(1656 ^ _325860) ^ [_383830] : [relation(_383830), subset(_383680, _383830), 1663 ^ _325860 : [(1666 ^ _325860) ^ [] : [-(subset(relation_rng(_383680), relation_rng(_383830)))], (1664 ^ _325860) ^ [] : [-(subset(relation_dom(_383680), relation_dom(_383830)))]]]]], (1809 ^ _325860) ^ [_389280, _389282] : [element(_389282, powerset(_389280)), -(subset(_389282, _389280))], (2003 ^ _325860) ^ [_396014, _396016, _396018] : [element(_396014, powerset(_396018)), in(_396016, subset_complement(_396018, _396014)), in(_396016, _396014)], (1908 ^ _325860) ^ [_392687, _392689] : [element(_392687, powerset(powerset(_392689))), -(_392687 = empty_set), complements_of_subsets(_392689, _392687) = empty_set], (461 ^ _325860) ^ [_342018] : [_342018 = empty_set, 464 ^ _325860 : [(465 ^ _325860) ^ [_342131] : [in(_342131, _342018)]]], (2136 ^ _325860) ^ [_400629] : [-(in(_400629, 2134 ^ [_400629]))], (72 ^ _325860) ^ [_328263, _328265, _328267, _328269] : [-(subset(_328267, _328263)), subset(_328269, _328265), _328269 = _328267, _328265 = _328263], (922 ^ _325860) ^ [_358979] : [relation(_358979), 925 ^ _325860 : [(926 ^ _325860) ^ [_359139] : [relation(_359139), 929 ^ _325860 : [(930 ^ _325860) ^ [] : [_359139 = relation_inverse(_358979), 933 ^ _325860 : [(940 ^ _325860) ^ [_359638, _359640] : [in(ordered_pair(_359638, _359640), _358979), -(in(ordered_pair(_359640, _359638), _359139))], (934 ^ _325860) ^ [_359448, _359450] : [in(ordered_pair(_359450, _359448), _359139), -(in(ordered_pair(_359448, _359450), _358979))]]], (946 ^ _325860) ^ [] : [-(_359139 = relation_inverse(_358979)), 951 ^ _325860 : [(954 ^ _325860) ^ [] : [in(ordered_pair(948 ^ [_358979, _359139], 947 ^ [_358979, _359139]), _358979)], (952 ^ _325860) ^ [] : [-(in(ordered_pair(947 ^ [_358979, _359139], 948 ^ [_358979, _359139]), _359139))]], 955 ^ _325860 : [(958 ^ _325860) ^ [] : [in(ordered_pair(947 ^ [_358979, _359139], 948 ^ [_358979, _359139]), _359139)], (956 ^ _325860) ^ [] : [-(in(ordered_pair(948 ^ [_358979, _359139], 947 ^ [_358979, _359139]), _358979))]]]]]]], (1567 ^ _325860) ^ [_380698, _380700] : [subset(_380700, _380698), -(set_union2(_380700, _380698) = _380698)], (962 ^ _325860) ^ [_360486, _360488] : [disjoint(_360488, _360486), -(set_intersection2(_360488, _360486) = empty_set)], (602 ^ _325860) ^ [_346722, _346724, _346726] : [-(_346722 = set_union2(_346726, _346724)), 606 ^ _325860 : [(611 ^ _325860) ^ [] : [in(603 ^ [_346722, _346724, _346726], _346724)], (609 ^ _325860) ^ [] : [in(603 ^ [_346722, _346724, _346726], _346726)], (607 ^ _325860) ^ [] : [-(in(603 ^ [_346722, _346724, _346726], _346722))]], 612 ^ _325860 : [(613 ^ _325860) ^ [] : [-(in(603 ^ [_346722, _346724, _346726], _346726)), -(in(603 ^ [_346722, _346724, _346726], _346724))], (619 ^ _325860) ^ [] : [in(603 ^ [_346722, _346724, _346726], _346722)]]], (34 ^ _325860) ^ [_327080, _327082, _327084, _327086] : [-(proper_subset(_327084, _327080)), proper_subset(_327086, _327082), _327086 = _327084, _327082 = _327080], (414 ^ _325860) ^ [_340449, _340451] : [_340451 = empty_set, 417 ^ _325860 : [(424 ^ _325860) ^ [] : [_340449 = empty_set, -(_340449 = set_meet(_340451))], (418 ^ _325860) ^ [] : [_340449 = set_meet(_340451), -(_340449 = empty_set)]]], (1763 ^ _325860) ^ [_387657, _387659] : [in(_387659, _387657), -(subset(singleton(_387659), _387657))], (212 ^ _325860) ^ [_333073, _333075, _333077, _333079] : [-(set_intersection2(_333079, _333075) = set_intersection2(_333077, _333073)), _333079 = _333077, _333075 = _333073], (653 ^ _325860) ^ [_348773, _348775, _348777] : [-(_348773 = cartesian_product2(_348777, _348775)), 671 ^ _325860 : [(674 ^ _325860) ^ [] : [-(in(670 ^ [_348773, _348775, _348777], _348775))], (676 ^ _325860) ^ [] : [-(654 ^ [_348773, _348775, _348777] = ordered_pair(669 ^ [_348773, _348775, _348777], 670 ^ [_348773, _348775, _348777]))], (678 ^ _325860) ^ [] : [in(654 ^ [_348773, _348775, _348777], _348773)], (672 ^ _325860) ^ [] : [-(in(669 ^ [_348773, _348775, _348777], _348777))]], 657 ^ _325860 : [(660 ^ _325860) ^ [_349111, _349113] : [in(_349113, _348777), in(_349111, _348775), 654 ^ [_348773, _348775, _348777] = ordered_pair(_349113, _349111)], (658 ^ _325860) ^ [] : [-(in(654 ^ [_348773, _348775, _348777], _348773))]]], (1462 ^ _325860) ^ [] : [-(empty(1460 ^ []))], (1979 ^ _325860) ^ [_395129, _395131] : [1980 ^ _325860 : [(1981 ^ _325860) ^ [_395202] : [in(_395202, set_intersection2(_395131, _395129))]], disjoint(_395131, _395129)], (1674 ^ _325860) ^ [_384467, _384469] : [subset(_384469, _384467), -(set_intersection2(_384469, _384467) = _384469)], (1107 ^ _325860) ^ [] : [true___, -(true___)], (146 ^ _325860) ^ [_330657, _330659] : [_330659 = _330657, -(relation_inverse(_330659) = relation_inverse(_330657))], (324 ^ _325860) ^ [_337156, _337158] : [-(set_intersection2(_337158, _337156) = set_intersection2(_337156, _337158))], (1486 ^ _325860) ^ [_377681] : [-(empty(1482 ^ [_377681]))], (2095 ^ _325860) ^ [_399119, _399121] : [set_difference(_399121, _399119) = _399121, -(disjoint(_399121, _399119))], (274 ^ _325860) ^ [_335276, _335278] : [_335278 = _335276, -(singleton(_335278) = singleton(_335276))], (1326 ^ _325860) ^ [_372062, _372064] : [element(_372062, powerset(_372064)), -(subset_complement(_372064, subset_complement(_372064, _372062)) = _372062)], (1193 ^ _325860) ^ [_367669, _367671] : [-(relation(relation_composition(_367671, _367669))), relation(_367671), relation(_367669)], (1960 ^ _325860) ^ [_394437] : [-(set_difference(empty_set, _394437) = empty_set)], (2161 ^ _325860) ^ [_401575, _401577] : [subset(_401575, 2134 ^ [_401577]), -(are_equipotent(_401575, 2134 ^ [_401577])), -(in(_401575, 2134 ^ [_401577]))], (1634 ^ _325860) ^ [_383094, _383096, _383098] : [relation(_383094), in(ordered_pair(_383098, _383096), _383094), 1641 ^ _325860 : [(1644 ^ _325860) ^ [] : [-(in(_383096, relation_rng(_383094)))], (1642 ^ _325860) ^ [] : [-(in(_383098, relation_dom(_383094)))]]], (537 ^ _325860) ^ [_344478, _344480, _344482] : [_344478 = unordered_pair(_344482, _344480), 540 ^ _325860 : [(541 ^ _325860) ^ [_344660] : [in(_344660, _344478), -(_344660 = _344482), -(_344660 = _344480)], (551 ^ _325860) ^ [_344938] : [552 ^ _325860 : [(555 ^ _325860) ^ [] : [_344938 = _344480], (553 ^ _325860) ^ [] : [_344938 = _344482]], -(in(_344938, _344478))]]], (781 ^ _325860) ^ [_353654] : [-(cast_to_subset(_353654) = _353654)], (1203 ^ _325860) ^ [_367968, _367970] : [element(_367968, powerset(powerset(_367970))), -(element(union_of_subsets(_367970, _367968), powerset(_367970)))], (2061 ^ _325860) ^ [_397904, _397906] : [-(in(_397904, _397906)), -(set_difference(_397906, singleton(_397904)) = _397906)], (2171 ^ _325860) ^ [_401909, _401911, _401913] : [singleton(_401913) = unordered_pair(_401911, _401909), -(_401911 = _401909)], (1372 ^ _325860) ^ [_373731, _373733] : [in(_373733, _373731), -(subset(singleton(_373733), _373731))], (2121 ^ _325860) ^ [_399977, _399979, _399981] : [singleton(_399981) = unordered_pair(_399979, _399977), -(_399981 = _399979)], (1557 ^ _325860) ^ [_380367, _380369, _380371, _380373] : [-(subset(cartesian_product2(_380373, _380369), cartesian_product2(_380371, _380367))), subset(_380373, _380371), subset(_380369, _380367)], (850 ^ _325860) ^ [_356258, _356260, _356262] : [-(_356258 = set_difference(_356262, _356260)), 862 ^ _325860 : [(867 ^ _325860) ^ [] : [in(851 ^ [_356258, _356260, _356262], _356258)], (865 ^ _325860) ^ [] : [in(851 ^ [_356258, _356260, _356262], _356260)], (863 ^ _325860) ^ [] : [-(in(851 ^ [_356258, _356260, _356262], _356262))]], 854 ^ _325860 : [(857 ^ _325860) ^ [] : [in(851 ^ [_356258, _356260, _356262], _356262), -(in(851 ^ [_356258, _356260, _356262], _356260))], (855 ^ _325860) ^ [] : [-(in(851 ^ [_356258, _356260, _356262], _356258))]]], (1709 ^ _325860) ^ [_385684, _385686, _385688] : [relation(_385684), in(ordered_pair(_385688, _385686), _385684), 1716 ^ _325860 : [(1719 ^ _325860) ^ [] : [-(in(_385686, relation_field(_385684)))], (1717 ^ _325860) ^ [] : [-(in(_385688, relation_field(_385684)))]]], (2127 ^ _325860) ^ [_400203, _400205] : [in(_400205, _400203), -(subset(_400205, union(_400203)))], (1246 ^ _325860) ^ [_369466, _369468] : [-(relation(set_union2(_369468, _369466))), relation(_369468), relation(_369466)], (2111 ^ _325860) ^ [_399648, _399650, _399652] : [-(subset(set_union2(_399652, _399648), _399650)), subset(_399652, _399650), subset(_399648, _399650)], (521 ^ _325860) ^ [_343978, _343980] : [empty(_343980), 524 ^ _325860 : [(531 ^ _325860) ^ [] : [empty(_343978), -(element(_343978, _343980))], (525 ^ _325860) ^ [] : [element(_343978, _343980), -(empty(_343978))]]], (1077 ^ _325860) ^ [_364965, _364967] : [proper_subset(_364967, _364965), 1080 ^ _325860 : [(1083 ^ _325860) ^ [] : [_364967 = _364965], (1081 ^ _325860) ^ [] : [-(subset(_364967, _364965))]]], (559 ^ _325860) ^ [_345203, _345205, _345207] : [-(_345203 = unordered_pair(_345207, _345205)), 563 ^ _325860 : [(568 ^ _325860) ^ [] : [560 ^ [_345203, _345205, _345207] = _345205], (566 ^ _325860) ^ [] : [560 ^ [_345203, _345205, _345207] = _345207], (564 ^ _325860) ^ [] : [-(in(560 ^ [_345203, _345205, _345207], _345203))]], 569 ^ _325860 : [(570 ^ _325860) ^ [] : [-(560 ^ [_345203, _345205, _345207] = _345207), -(560 ^ [_345203, _345205, _345207] = _345205)], (576 ^ _325860) ^ [] : [in(560 ^ [_345203, _345205, _345207], _345203)]]], (505 ^ _325860) ^ [_343565, _343567] : [-(empty(_343567)), 508 ^ _325860 : [(515 ^ _325860) ^ [] : [in(_343565, _343567), -(element(_343565, _343567))], (509 ^ _325860) ^ [] : [element(_343565, _343567), -(in(_343565, _343567))]]], (2067 ^ _325860) ^ [_398100] : [-(unordered_pair(_398100, _398100) = singleton(_398100))], (1139 ^ _325860) ^ [] : [true___, -(true___)], (2089 ^ _325860) ^ [_398951, _398953] : [disjoint(_398953, _398951), -(set_difference(_398953, _398951) = _398953)], (2133 ^ _325860) ^ [_400388] : [-(union(powerset(_400388)) = _400388)], (202 ^ _325860) ^ [_332714, _332716, _332718, _332720] : [-(meet_of_subsets(_332720, _332716) = meet_of_subsets(_332718, _332714)), _332720 = _332718, _332716 = _332714], (2087 ^ _325860) ^ [_398810, _398812] : [-(subset(_398812, set_union2(_398812, _398810)))], (20 ^ _325860) ^ [_326636, _326638, _326640, _326642] : [-(element(_326640, _326636)), element(_326642, _326638), _326642 = _326640, _326638 = _326636], (232 ^ _325860) ^ [_333791, _333793, _333795, _333797] : [-(ordered_pair(_333797, _333793) = ordered_pair(_333795, _333791)), _333797 = _333795, _333793 = _333791], (182 ^ _325860) ^ [_332008, _332010, _332012, _332014, _332016, _332018] : [-(subset_difference(_332018, _332014, _332010) = subset_difference(_332016, _332012, _332008)), _332018 = _332016, _332014 = _332012, _332010 = _332008], (1264 ^ _325860) ^ [_370043, _370045] : [empty(unordered_pair(_370045, _370043))], (1354 ^ _325860) ^ [_373106, _373108] : [disjoint(singleton(_373108), _373106), in(_373108, _373106)], (1799 ^ _325860) ^ [_388876, _388878] : [1800 ^ _325860 : [(1803 ^ _325860) ^ [] : [_388878 = singleton(_388876)], (1801 ^ _325860) ^ [] : [_388878 = empty_set]], -(subset(_388878, singleton(_388876)))], (828 ^ _325860) ^ [_355527, _355529, _355531] : [_355527 = set_difference(_355531, _355529), 831 ^ _325860 : [(840 ^ _325860) ^ [_355971] : [-(in(_355971, _355527)), in(_355971, _355531), -(in(_355971, _355529))], (832 ^ _325860) ^ [_355711] : [in(_355711, _355527), 835 ^ _325860 : [(838 ^ _325860) ^ [] : [in(_355711, _355529)], (836 ^ _325860) ^ [] : [-(in(_355711, _355531))]]]]], (1878 ^ _325860) ^ [_391640] : [relation(_391640), 1881 ^ _325860 : [(1882 ^ _325860) ^ [_391777] : [relation(_391777), -(subset(relation_rng(relation_composition(_391640, _391777)), relation_rng(_391777)))]]], (1807 ^ _325860) ^ [_389141] : [-(set_difference(_389141, empty_set) = _389141)], (1737 ^ _325860) ^ [_386748] : [relation(_386748), 1740 ^ _325860 : [(1743 ^ _325860) ^ [] : [-(relation_dom(_386748) = relation_rng(relation_inverse(_386748)))], (1741 ^ _325860) ^ [] : [-(relation_rng(_386748) = relation_dom(relation_inverse(_386748)))]]], (2035 ^ _325860) ^ [] : [-(relation_dom(empty_set) = empty_set)], (1101 ^ _325860) ^ [] : [true___, -(true___)], (1344 ^ _325860) ^ [_372698, _372700] : [proper_subset(_372700, _372700)], (1789 ^ _325860) ^ [_388616, _388618] : [subset(_388618, singleton(_388616)), -(_388618 = empty_set), -(_388618 = singleton(_388616))], (1479 ^ _325860) ^ [] : [empty(1477 ^ [])], (1133 ^ _325860) ^ [] : [true___, -(true___)], (1848 ^ _325860) ^ [_390652, _390654] : [element(_390652, powerset(_390654)), 1851 ^ _325860 : [(1852 ^ _325860) ^ [_390804] : [element(_390804, powerset(_390654)), 1855 ^ _325860 : [(1862 ^ _325860) ^ [] : [subset(_390652, subset_complement(_390654, _390804)), -(disjoint(_390652, _390804))], (1856 ^ _325860) ^ [] : [disjoint(_390652, _390804), -(subset(_390652, subset_complement(_390654, _390804)))]]]]], (871 ^ _325860) ^ [_357001] : [relation(_357001), 874 ^ _325860 : [(875 ^ _325860) ^ [_357182] : [_357182 = relation_rng(_357001), 878 ^ _325860 : [(886 ^ _325860) ^ [_357606] : [887 ^ _325860 : [(888 ^ _325860) ^ [_357685] : [in(ordered_pair(_357685, _357606), _357001)]], -(in(_357606, _357182))], (879 ^ _325860) ^ [_357362] : [in(_357362, _357182), -(in(ordered_pair(882 ^ [_357001, _357182, _357362], _357362), _357001))]]], (892 ^ _325860) ^ [_357813] : [-(_357813 = relation_rng(_357001)), 896 ^ _325860 : [(899 ^ _325860) ^ [_358076] : [in(ordered_pair(_358076, 893 ^ [_357001, _357813]), _357001)], (897 ^ _325860) ^ [] : [-(in(893 ^ [_357001, _357813], _357813))]], 901 ^ _325860 : [(904 ^ _325860) ^ [] : [in(893 ^ [_357001, _357813], _357813)], (902 ^ _325860) ^ [] : [-(in(ordered_pair(900 ^ [_357001, _357813], 893 ^ [_357001, _357813]), _357001))]]]]], (1209 ^ _325860) ^ [_368196, _368198] : [element(_368196, powerset(powerset(_368198))), -(element(meet_of_subsets(_368198, _368196), powerset(_368198)))], (1464 ^ _325860) ^ [] : [-(relation(1460 ^ []))], (1242 ^ _325860) ^ [] : [-(empty(empty_set))], (1574 ^ _325860) ^ [_381020] : [-(in(_381020, 1572 ^ [_381020]))], (322 ^ _325860) ^ [_337056, _337058] : [-(set_union2(_337058, _337056) = set_union2(_337056, _337058))], (162 ^ _325860) ^ [_331262, _331264, _331266, _331268] : [-(union_of_subsets(_331268, _331264) = union_of_subsets(_331266, _331262)), _331268 = _331266, _331264 = _331262], (2069 ^ _325860) ^ [_398198] : [empty(_398198), -(_398198 = empty_set)], (252 ^ _325860) ^ [_334509, _334511, _334513, _334515] : [-(set_union2(_334515, _334511) = set_union2(_334513, _334509)), _334515 = _334513, _334511 = _334509], (1868 ^ _325860) ^ [_391288] : [relation(_391288), 1871 ^ _325860 : [(1872 ^ _325860) ^ [_391425] : [relation(_391425), -(subset(relation_dom(relation_composition(_391288, _391425)), relation_dom(_391288)))]]], (1592 ^ _325860) ^ [_381647, _381649] : [subset(_381647, 1572 ^ [_381649]), -(are_equipotent(_381647, 1572 ^ [_381649])), -(in(_381647, 1572 ^ [_381649]))], (1632 ^ _325860) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (1272 ^ _325860) ^ [] : [-(empty(empty_set))], (1707 ^ _325860) ^ [_385563] : [-(subset(empty_set, _385563))], (1840 ^ _325860) ^ [_390345] : [subset(_390345, empty_set), -(_390345 = empty_set)], (152 ^ _325860) ^ [_330903, _330905, _330907, _330909] : [-(relation_composition(_330909, _330905) = relation_composition(_330907, _330903)), _330909 = _330907, _330905 = _330903], (1238 ^ _325860) ^ [_369128] : [-(element(1236 ^ [_369128], _369128))], (1745 ^ _325860) ^ [_387076, _387078] : [set_difference(_387078, _387076) = empty_set, -(subset(_387078, _387076))], (1614 ^ _325860) ^ [_382384] : [-(set_union2(_382384, empty_set) = _382384)], (1366 ^ _325860) ^ [_373565, _373567] : [subset(singleton(_373567), _373565), -(in(_373567, _373565))], (1332 ^ _325860) ^ [_372274] : [relation(_372274), -(relation_inverse(relation_inverse(_372274)) = _372274)], (1484 ^ _325860) ^ [_377630] : [-(element(1482 ^ [_377630], powerset(_377630)))], (100 ^ _325860) ^ [_329151, _329153, _329155, _329157] : [-(in(_329155, _329151)), in(_329157, _329153), _329157 = _329155, _329153 = _329151], (744 ^ _325860) ^ [_352228] : [relation(_352228), 747 ^ _325860 : [(748 ^ _325860) ^ [_352409] : [_352409 = relation_dom(_352228), 751 ^ _325860 : [(759 ^ _325860) ^ [_352833] : [760 ^ _325860 : [(761 ^ _325860) ^ [_352912] : [in(ordered_pair(_352833, _352912), _352228)]], -(in(_352833, _352409))], (752 ^ _325860) ^ [_352589] : [in(_352589, _352409), -(in(ordered_pair(_352589, 755 ^ [_352228, _352409, _352589]), _352228))]]], (765 ^ _325860) ^ [_353040] : [-(_353040 = relation_dom(_352228)), 769 ^ _325860 : [(772 ^ _325860) ^ [_353303] : [in(ordered_pair(766 ^ [_352228, _353040], _353303), _352228)], (770 ^ _325860) ^ [] : [-(in(766 ^ [_352228, _353040], _353040))]], 774 ^ _325860 : [(777 ^ _325860) ^ [] : [in(766 ^ [_352228, _353040], _353040)], (775 ^ _325860) ^ [] : [-(in(ordered_pair(766 ^ [_352228, _353040], 773 ^ [_352228, _353040]), _352228))]]]]], (1266 ^ _325860) ^ [_370154, _370156] : [-(empty(_370156)), empty(set_union2(_370154, _370156))], (692 ^ _325860) ^ [_350364, _350366] : [694 ^ _325860 : [(697 ^ _325860) ^ [] : [in(693 ^ [_350364, _350366], _350364)], (695 ^ _325860) ^ [] : [-(in(693 ^ [_350364, _350366], _350366))]], -(subset(_350366, _350364))], (1529 ^ _325860) ^ [_379311, _379313, _379315, _379317] : [-(in(ordered_pair(_379317, _379315), cartesian_product2(_379313, _379311))), in(_379317, _379313), in(_379315, _379311)], (1489 ^ _325860) ^ [] : [empty(1487 ^ [])], (1225 ^ _325860) ^ [_368767, _368769] : [element(_368767, powerset(powerset(_368769))), -(element(complements_of_subsets(_368769, _368767), powerset(powerset(_368769))))], (1322 ^ _325860) ^ [_371853, _371855] : [-(set_union2(_371855, _371855) = _371855)], (1727 ^ _325860) ^ [_386352, _386354, _386356, _386358] : [ordered_pair(_386358, _386356) = ordered_pair(_386354, _386352), 1730 ^ _325860 : [(1733 ^ _325860) ^ [] : [-(_386356 = _386352)], (1731 ^ _325860) ^ [] : [-(_386358 = _386354)]]], (1113 ^ _325860) ^ [] : [true___, -(true___)], (1521 ^ _325860) ^ [_379046, _379048, _379050, _379052] : [in(ordered_pair(_379052, _379050), cartesian_product2(_379048, _379046)), 1524 ^ _325860 : [(1527 ^ _325860) ^ [] : [-(in(_379050, _379046))], (1525 ^ _325860) ^ [] : [-(in(_379052, _379048))]]], (682 ^ _325860) ^ [_350050, _350052] : [subset(_350052, _350050), 685 ^ _325860 : [(686 ^ _325860) ^ [_350187] : [in(_350187, _350052), -(in(_350187, _350050))]]], (1692 ^ _325860) ^ [_385062, _385064] : [-(_385064 = _385062), 1696 ^ _325860 : [(1699 ^ _325860) ^ [] : [in(1693 ^ [_385062, _385064], _385062)], (1697 ^ _325860) ^ [] : [-(in(1693 ^ [_385062, _385064], _385064))]], 1700 ^ _325860 : [(1703 ^ _325860) ^ [] : [in(1693 ^ [_385062, _385064], _385064)], (1701 ^ _325860) ^ [] : [-(in(1693 ^ [_385062, _385064], _385062))]]], (783 ^ _325860) ^ [_353792, _353794] : [_353792 = union(_353794), 786 ^ _325860 : [(796 ^ _325860) ^ [_354300] : [-(in(_354300, _353792)), 797 ^ _325860 : [(798 ^ _325860) ^ [_354398] : [in(_354300, _354398), in(_354398, _353794)]]], (787 ^ _325860) ^ [_353973] : [in(_353973, _353792), 791 ^ _325860 : [(794 ^ _325860) ^ [] : [-(in(790 ^ [_353792, _353794, _353973], _353794))], (792 ^ _325860) ^ [] : [-(in(_353973, 790 ^ [_353792, _353794, _353973]))]]]]], (1338 ^ _325860) ^ [_372484, _372486] : [element(_372484, powerset(powerset(_372486))), -(complements_of_subsets(_372486, complements_of_subsets(_372486, _372484)) = _372484)], (1821 ^ _325860) ^ [_389682, _389684] : [-(disjoint(_389684, _389682)), 1825 ^ _325860 : [(1828 ^ _325860) ^ [] : [-(in(1824 ^ [_389682, _389684], _389682))], (1826 ^ _325860) ^ [] : [-(in(1824 ^ [_389682, _389684], _389684))]]], (1145 ^ _325860) ^ [] : [true___, -(true___)], (1948 ^ _325860) ^ [_394023, _394025] : [element(_394023, powerset(powerset(_394025))), -(_394023 = empty_set), -(union_of_subsets(_394025, complements_of_subsets(_394025, _394023)) = subset_difference(_394025, cast_to_subset(_394025), meet_of_subsets(_394025, _394023)))], (280 ^ _325860) ^ [_335522, _335524, _335526, _335528] : [-(unordered_pair(_335528, _335524) = unordered_pair(_335526, _335522)), _335528 = _335526, _335524 = _335522], (1757 ^ _325860) ^ [_387491, _387493] : [subset(singleton(_387493), _387491), -(in(_387493, _387491))], (2039 ^ _325860) ^ [_397170, _397172] : [subset(_397172, _397170), proper_subset(_397170, _397172)], (1274 ^ _325860) ^ [] : [-(relation(empty_set))], (1348 ^ _325860) ^ [_372886, _372888] : [in(_372888, _372886), -(set_union2(singleton(_372888), _372886) = _372886)], (1515 ^ _325860) ^ [_378779, _378781] : [disjoint(_378781, _378779), -(disjoint(_378779, _378781))], (2037 ^ _325860) ^ [] : [-(relation_rng(empty_set) = empty_set)], (1296 ^ _325860) ^ [_371047] : [empty(relation_rng(_371047)), -(empty(_371047)), relation(_371047)], (1481 ^ _325860) ^ [] : [-(relation(1477 ^ []))], (1125 ^ _325860) ^ [] : [true___, -(true___)], (1187 ^ _325860) ^ [] : [true___, -(true___)], (1602 ^ _325860) ^ [_381972, _381974] : [-(subset(set_intersection2(_381974, _381972), _381974))], (1384 ^ _325860) ^ [_374144, _374146] : [subset(_374146, _374144), -(set_difference(_374146, _374144) = empty_set)], (1918 ^ _325860) ^ [_393004, _393006] : [in(_393006, _393004), -(set_union2(singleton(_393006), _393004) = _393004)], (1346 ^ _325860) ^ [_372777] : [singleton(_372777) = empty_set], (1119 ^ _325860) ^ [] : [true___, -(true___)], (2045 ^ _325860) ^ [_397393, _397395, _397397] : [-(disjoint(_397397, _397393)), subset(_397397, _397395), disjoint(_397395, _397393)], (222 ^ _325860) ^ [_333432, _333434, _333436, _333438] : [-(subset_complement(_333438, _333434) = subset_complement(_333436, _333432)), _333438 = _333436, _333434 = _333432], (1434 ^ _325860) ^ [_375916, _375918, _375920, _375922] : [in(ordered_pair(_375922, _375920), cartesian_product2(_375918, _375916)), 1437 ^ _325860 : [(1440 ^ _325860) ^ [] : [-(in(_375920, _375916))], (1438 ^ _325860) ^ [] : [-(in(_375922, _375918))]]], (62 ^ _325860) ^ [_327940, _327942] : [-(empty(_327940)), _327942 = _327940, empty(_327942)], (1324 ^ _325860) ^ [_371950, _371952] : [-(set_intersection2(_371952, _371952) = _371952)], (1400 ^ _325860) ^ [_374742, _374744, _374746] : [subset(_374746, _374744), -(in(_374742, _374746)), -(subset(_374746, set_difference(_374744, singleton(_374742))))], (262 ^ _325860) ^ [_334840, _334842] : [_334842 = _334840, -(union(_334842) = union(_334840))], (1924 ^ _325860) ^ [_393210] : [relation(_393210), 1927 ^ _325860 : [(1928 ^ _325860) ^ [_393357] : [relation(_393357), subset(relation_dom(_393210), relation_rng(_393357)), -(relation_rng(relation_composition(_393357, _393210)) = relation_rng(_393210))]]], (268 ^ _325860) ^ [_335058, _335060] : [_335060 = _335058, -(powerset(_335060) = powerset(_335058))], (446 ^ _325860) ^ [_341467, _341469] : [-(_341467 = singleton(_341469)), 450 ^ _325860 : [(453 ^ _325860) ^ [] : [447 ^ [_341467, _341469] = _341469], (451 ^ _325860) ^ [] : [-(in(447 ^ [_341467, _341469], _341467))]], 454 ^ _325860 : [(457 ^ _325860) ^ [] : [in(447 ^ [_341467, _341469], _341467)], (455 ^ _325860) ^ [] : [-(447 ^ [_341467, _341469] = _341469)]]], (974 ^ _325860) ^ [_360858] : [relation(_360858), 977 ^ _325860 : [(978 ^ _325860) ^ [_361043] : [relation(_361043), 981 ^ _325860 : [(982 ^ _325860) ^ [_361224] : [relation(_361224), 985 ^ _325860 : [(986 ^ _325860) ^ [] : [_361224 = relation_composition(_360858, _361043), 989 ^ _325860 : [(999 ^ _325860) ^ [_361944, _361946] : [-(in(ordered_pair(_361946, _361944), _361224)), 1000 ^ _325860 : [(1001 ^ _325860) ^ [_362057] : [in(ordered_pair(_361946, _362057), _360858), in(ordered_pair(_362057, _361944), _361043)]]], (990 ^ _325860) ^ [_361559, _361561] : [in(ordered_pair(_361561, _361559), _361224), 994 ^ _325860 : [(997 ^ _325860) ^ [] : [-(in(ordered_pair(993 ^ [_360858, _361043, _361224, _361559, _361561], _361559), _361043))], (995 ^ _325860) ^ [] : [-(in(ordered_pair(_361561, 993 ^ [_360858, _361043, _361224, _361559, _361561]), _360858))]]]]], (1009 ^ _325860) ^ [] : [-(_361224 = relation_composition(_360858, _361043)), 1023 ^ _325860 : [(1028 ^ _325860) ^ [] : [in(ordered_pair(1010 ^ [_360858, _361043, _361224], 1011 ^ [_360858, _361043, _361224]), _361224)], (1026 ^ _325860) ^ [] : [-(in(ordered_pair(1022 ^ [_360858, _361043, _361224], 1011 ^ [_360858, _361043, _361224]), _361043))], (1024 ^ _325860) ^ [] : [-(in(ordered_pair(1010 ^ [_360858, _361043, _361224], 1022 ^ [_360858, _361043, _361224]), _360858))]], 1014 ^ _325860 : [(1017 ^ _325860) ^ [_362688] : [in(ordered_pair(1010 ^ [_360858, _361043, _361224], _362688), _360858), in(ordered_pair(_362688, 1011 ^ [_360858, _361043, _361224]), _361043)], (1015 ^ _325860) ^ [] : [-(in(ordered_pair(1010 ^ [_360858, _361043, _361224], 1011 ^ [_360858, _361043, _361224]), _361224))]]]]]]]]], (1958 ^ _325860) ^ [_394348, _394350] : [-(set_difference(_394350, set_difference(_394350, _394348)) = set_intersection2(_394350, _394348))], (1442 ^ _325860) ^ [_376181, _376183, _376185, _376187] : [-(in(ordered_pair(_376187, _376185), cartesian_product2(_376183, _376181))), in(_376187, _376183), in(_376185, _376181)], (474 ^ _325860) ^ [_342488, _342490] : [_342488 = powerset(_342490), 477 ^ _325860 : [(484 ^ _325860) ^ [_342830] : [subset(_342830, _342490), -(in(_342830, _342488))], (478 ^ _325860) ^ [_342658] : [in(_342658, _342488), -(subset(_342658, _342490))]]], (2148 ^ _325860) ^ [_401056, _401058] : [in(_401056, 2134 ^ [_401058]), 2152 ^ _325860 : [(2155 ^ _325860) ^ [_401368] : [subset(_401368, _401056), -(in(_401368, 2151 ^ [_401056, _401058]))], (2153 ^ _325860) ^ [] : [-(in(2151 ^ [_401056, _401058], 2134 ^ [_401058]))]]], (1830 ^ _325860) ^ [_389996, _389998] : [disjoint(_389998, _389996), 1831 ^ _325860 : [(1832 ^ _325860) ^ [_390088] : [in(_390088, _389998), in(_390088, _389996)]]], (916 ^ _325860) ^ [_358773] : [relation(_358773), -(relation_field(_358773) = set_union2(relation_dom(_358773), relation_rng(_358773)))], (1497 ^ _325860) ^ [_378112, _378114] : [element(_378112, powerset(powerset(_378114))), -(meet_of_subsets(_378114, _378112) = set_meet(_378112))], (314 ^ _325860) ^ [_336771] : [empty(_336771), -(relation(_336771))], (908 ^ _325860) ^ [_358456, _358458] : [element(_358456, powerset(_358458)), -(subset_complement(_358458, _358456) = set_difference(_358458, _358456))], (1215 ^ _325860) ^ [_368438, _368440, _368442] : [-(element(subset_difference(_368442, _368440, _368438), powerset(_368442))), element(_368440, powerset(_368442)), element(_368438, powerset(_368442))], (1846 ^ _325860) ^ [_390534, _390536] : [-(set_difference(set_union2(_390536, _390534), _390534) = set_difference(_390536, _390534))], (290 ^ _325860) ^ [_335853, _335855] : [_335855 = _335853, -(relation_dom(_335855) = relation_dom(_335853))], (968 ^ _325860) ^ [_360654, _360656] : [set_intersection2(_360656, _360654) = empty_set, -(disjoint(_360656, _360654))], (1314 ^ _325860) ^ [_371589] : [empty(_371589), 1317 ^ _325860 : [(1320 ^ _325860) ^ [] : [-(relation(relation_rng(_371589)))], (1318 ^ _325860) ^ [] : [-(empty(relation_rng(_371589)))]]], (308 ^ _325860) ^ [_336574, _336576] : [proper_subset(_336576, _336574), proper_subset(_336574, _336576)], (1390 ^ _325860) ^ [_374362, _374364] : [element(_374362, powerset(_374364)), 1393 ^ _325860 : [(1394 ^ _325860) ^ [_374503] : [in(_374503, _374362), -(in(_374503, _374364))]]], (326 ^ _325860) ^ [_337300, _337302] : [_337302 = _337300, 329 ^ _325860 : [(332 ^ _325860) ^ [] : [-(subset(_337300, _337302))], (330 ^ _325860) ^ [] : [-(subset(_337302, _337300))]]], (296 ^ _325860) ^ [_336051, _336053] : [_336053 = _336051, -(relation_rng(_336053) = relation_rng(_336051))], (1085 ^ _325860) ^ [_365203, _365205] : [-(proper_subset(_365205, _365203)), subset(_365205, _365203), -(_365205 = _365203)], (130 ^ _325860) ^ [_330108, _330110, _330112, _330114] : [-(cartesian_product2(_330114, _330110) = cartesian_product2(_330112, _330108)), _330114 = _330112, _330110 = _330108], (1410 ^ _325860) ^ [_375091, _375093] : [subset(_375093, singleton(_375091)), -(_375093 = empty_set), -(_375093 = singleton(_375091))], (242 ^ _325860) ^ [_334150, _334152, _334154, _334156] : [-(set_difference(_334156, _334152) = set_difference(_334154, _334150)), _334156 = _334154, _334152 = _334150], (1491 ^ _325860) ^ [_377884, _377886] : [element(_377884, powerset(powerset(_377886))), -(union_of_subsets(_377886, _377884) = union(_377884))], (2081 ^ _325860) ^ [_398618, _398620] : [in(_398620, _398618), empty(_398618)], (1181 ^ _325860) ^ [] : [true___, -(true___)], (490 ^ _325860) ^ [_343009, _343011] : [-(_343009 = powerset(_343011)), 494 ^ _325860 : [(497 ^ _325860) ^ [] : [subset(491 ^ [_343009, _343011], _343011)], (495 ^ _325860) ^ [] : [-(in(491 ^ [_343009, _343011], _343009))]], 498 ^ _325860 : [(501 ^ _325860) ^ [] : [in(491 ^ [_343009, _343011], _343009)], (499 ^ _325860) ^ [] : [-(subset(491 ^ [_343009, _343011], _343011))]]], (623 ^ _325860) ^ [_347516, _347518, _347520] : [_347516 = cartesian_product2(_347520, _347518), 626 ^ _325860 : [(639 ^ _325860) ^ [_348277] : [-(in(_348277, _347516)), 640 ^ _325860 : [(641 ^ _325860) ^ [_348407, _348409] : [in(_348409, _347520), in(_348407, _347518), _348277 = ordered_pair(_348409, _348407)]]], (627 ^ _325860) ^ [_347717] : [in(_347717, _347516), 632 ^ _325860 : [(637 ^ _325860) ^ [] : [-(_347717 = ordered_pair(630 ^ [_347516, _347518, _347520, _347717], 631 ^ [_347516, _347518, _347520, _347717]))], (635 ^ _325860) ^ [] : [-(in(631 ^ [_347516, _347518, _347520, _347717], _347518))], (633 ^ _325860) ^ [] : [-(in(630 ^ [_347516, _347518, _347520, _347717], _347520))]]]]], (806 ^ _325860) ^ [_354637, _354639] : [-(_354637 = union(_354639)), 819 ^ _325860 : [(824 ^ _325860) ^ [] : [in(807 ^ [_354637, _354639], _354637)], (822 ^ _325860) ^ [] : [-(in(818 ^ [_354637, _354639], _354639))], (820 ^ _325860) ^ [] : [-(in(807 ^ [_354637, _354639], 818 ^ [_354637, _354639]))]], 810 ^ _325860 : [(813 ^ _325860) ^ [_354920] : [in(807 ^ [_354637, _354639], _354920), in(_354920, _354639)], (811 ^ _325860) ^ [] : [-(in(807 ^ [_354637, _354639], _354637))]]], (302 ^ _325860) ^ [_336363, _336365] : [in(_336365, _336363), in(_336363, _336365)], (914 ^ _325860) ^ [_358667, _358669] : [-(ordered_pair(_358669, _358667) = unordered_pair(unordered_pair(_358669, _358667), singleton(_358669)))], (1258 ^ _325860) ^ [_369843, _369845] : [-(empty(_369845)), empty(set_union2(_369845, _369843))], (2 ^ _325860) ^ [_325984] : [-(_325984 = _325984)], (1888 ^ _325860) ^ [_392006, _392008] : [subset(_392008, _392006), -(_392006 = set_union2(_392008, set_difference(_392006, _392008)))], (320 ^ _325860) ^ [_336956, _336958] : [-(unordered_pair(_336958, _336956) = unordered_pair(_336956, _336958))]], input).
% 46.45/45.83 ncf('1',plain,[-(relation_dom(2176 ^ []) = empty_set), -(relation_rng(2176 ^ []) = empty_set)],start(2180 ^ 0)).
% 46.45/45.83 ncf('1.1',plain,[relation_dom(2176 ^ []) = empty_set, -(empty_set = relation_dom(2176 ^ []))],extension(4 ^ 1,bind([[_326091, _326093], [empty_set, relation_dom(2176 ^ [])]]))).
% 46.45/45.83 ncf('1.1.1',plain,[empty_set = relation_dom(2176 ^ []), 761 : in(ordered_pair(2018 ^ [2176 ^ []], 2019 ^ [2176 ^ []]), 2176 ^ []), 761 : -(in(2018 ^ [2176 ^ []], empty_set)), 748 : relation(2176 ^ [])],extension(744 ^ 2,bind([[_352228, _352409, _352833, _352912], [2176 ^ [], empty_set, 2018 ^ [2176 ^ []], 2019 ^ [2176 ^ []]]]))).
% 46.45/45.83 ncf('1.1.1.1',plain,[-(in(ordered_pair(2018 ^ [2176 ^ []], 2019 ^ [2176 ^ []]), 2176 ^ [])), relation(2176 ^ []), -(2176 ^ [] = empty_set)],extension(2013 ^ 9,bind([[_396320], [2176 ^ []]]))).
% 46.45/45.83 ncf('1.1.1.1.1',plain,[-(relation(2176 ^ []))],extension(2178 ^ 10)).
% 46.45/45.83 ncf('1.1.1.1.2',plain,[2176 ^ [] = empty_set],extension(2186 ^ 10)).
% 46.45/45.83 ncf('1.1.1.2',plain,[in(2018 ^ [2176 ^ []], empty_set), empty(empty_set)],extension(2081 ^ 7,bind([[_398618, _398620], [empty_set, 2018 ^ [2176 ^ []]]]))).
% 46.45/45.83 ncf('1.1.1.2.1',plain,[-(empty(empty_set))],extension(1242 ^ 8)).
% 46.45/45.83 ncf('1.1.1.3',plain,[-(relation(2176 ^ []))],extension(2178 ^ 3)).
% 46.45/45.83 ncf('1.2',plain,[relation_rng(2176 ^ []) = empty_set, -(empty_set = relation_rng(2176 ^ []))],extension(4 ^ 1,bind([[_326091, _326093], [empty_set, relation_rng(2176 ^ [])]]))).
% 46.45/45.83 ncf('1.2.1',plain,[empty_set = relation_rng(2176 ^ []), 888 : in(ordered_pair(2018 ^ [2176 ^ []], 2019 ^ [2176 ^ []]), 2176 ^ []), 888 : -(in(2019 ^ [2176 ^ []], empty_set)), 875 : relation(2176 ^ [])],extension(871 ^ 2,bind([[_357001, _357182, _357606, _357685], [2176 ^ [], empty_set, 2019 ^ [2176 ^ []], 2018 ^ [2176 ^ []]]]))).
% 46.45/45.83 ncf('1.2.1.1',plain,[-(in(ordered_pair(2018 ^ [2176 ^ []], 2019 ^ [2176 ^ []]), 2176 ^ [])), relation(2176 ^ []), -(2176 ^ [] = empty_set)],extension(2013 ^ 9,bind([[_396320], [2176 ^ []]]))).
% 46.45/45.83 ncf('1.2.1.1.1',plain,[-(relation(2176 ^ []))],extension(2178 ^ 10)).
% 46.45/45.83 ncf('1.2.1.1.2',plain,[2176 ^ [] = empty_set],extension(2186 ^ 10)).
% 46.45/45.83 ncf('1.2.1.2',plain,[in(2019 ^ [2176 ^ []], empty_set), empty(empty_set)],extension(2081 ^ 7,bind([[_398618, _398620], [empty_set, 2019 ^ [2176 ^ []]]]))).
% 46.45/45.83 ncf('1.2.1.2.1',plain,[-(empty(empty_set))],extension(1242 ^ 8)).
% 46.45/45.83 ncf('1.2.1.3',plain,[-(relation(2176 ^ []))],extension(2178 ^ 3)).
% 46.45/45.83 %-----------------------------------------------------
% 46.45/45.83 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------