%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU162+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:27 EDT 2023
% Result : Theorem 44.17s 43.80s
% Output : Proof 44.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU162+2 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n013.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 13:18:50 EDT 2023
% 0.13/0.35 % CPUTime :
% 44.17/43.80
% 44.17/43.80 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 44.17/43.80 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.17/43.80 %-----------------------------------------------------
% 44.17/43.80 ncf(matrix, plain, [(1087 ^ _194811) ^ [] : [1088 ^ _194811 : [(1091 ^ _194811) ^ [] : [-(in(1085 ^ [], 1084 ^ []))], (1089 ^ _194811) ^ [] : [-(set_difference(1084 ^ [], singleton(1085 ^ [])) = 1084 ^ [])]], 1092 ^ _194811 : [(1095 ^ _194811) ^ [] : [set_difference(1084 ^ [], singleton(1085 ^ [])) = 1084 ^ []], (1093 ^ _194811) ^ [] : [in(1085 ^ [], 1084 ^ [])]]], !, (1041 ^ _156207) ^ [_192746, _192748] : [disjoint(_192748, _192746), -(set_difference(_192748, _192746) = _192748)], (182 ^ _156207) ^ [_162591, _162593] : [_162593 = _162591, 185 ^ _156207 : [(188 ^ _156207) ^ [] : [-(subset(_162591, _162593))], (186 ^ _156207) ^ [] : [-(subset(_162593, _162591))]]], (200 ^ _156207) ^ [_163158, _163160] : [_163158 = singleton(_163160), 203 ^ _156207 : [(210 ^ _156207) ^ [_163500] : [_163500 = _163160, -(in(_163500, _163158))], (204 ^ _156207) ^ [_163328] : [in(_163328, _163158), -(_163328 = _163160)]]], (1063 ^ _156207) ^ [_193443, _193445, _193447] : [-(subset(set_union2(_193447, _193443), _193445)), subset(_193447, _193445), subset(_193443, _193445)], (907 ^ _156207) ^ [_187947, _187949, _187951] : [subset(unordered_pair(_187951, _187949), _187947), 910 ^ _156207 : [(913 ^ _156207) ^ [] : [-(in(_187949, _187947))], (911 ^ _156207) ^ [] : [-(in(_187951, _187947))]]], (722 ^ _156207) ^ [_181301, _181303] : [subset(_181303, _181301), -(set_difference(_181303, _181301) = empty_set)], (1033 ^ _156207) ^ [_192413, _192415] : [in(_192415, _192413), empty(_192413)], (1047 ^ _156207) ^ [_192914, _192916] : [set_difference(_192916, _192914) = _192916, -(disjoint(_192916, _192914))], (602 ^ _156207) ^ [] : [true___, -(true___)], (2 ^ _156207) ^ [_156331] : [-(_156331 = _156331)], (672 ^ _156207) ^ [_179461, _179463] : [-(empty(_179463)), empty(set_union2(_179461, _179463))], (1003 ^ _156207) ^ [_191392, _191394] : [subset(_191394, _191392), proper_subset(_191392, _191394)], (86 ^ _156207) ^ [_159020, _159022] : [_159022 = _159020, -(union(_159022) = union(_159020))], (391 ^ _156207) ^ [_170095, _170097, _170099] : [-(_170095 = cartesian_product2(_170099, _170097)), 409 ^ _156207 : [(412 ^ _156207) ^ [] : [-(in(408 ^ [_170095, _170097, _170099], _170097))], (414 ^ _156207) ^ [] : [-(392 ^ [_170095, _170097, _170099] = ordered_pair(407 ^ [_170095, _170097, _170099], 408 ^ [_170095, _170097, _170099]))], (416 ^ _156207) ^ [] : [in(392 ^ [_170095, _170097, _170099], _170095)], (410 ^ _156207) ^ [] : [-(in(407 ^ [_170095, _170097, _170099], _170099))]], 395 ^ _156207 : [(398 ^ _156207) ^ [_170433, _170435] : [in(_170435, _170099), in(_170433, _170097), 392 ^ [_170095, _170097, _170099] = ordered_pair(_170435, _170433)], (396 ^ _156207) ^ [] : [-(in(392 ^ [_170095, _170097, _170099], _170095))]]], (883 ^ _156207) ^ [_187107, _187109] : [set_difference(_187109, _187107) = empty_set, -(subset(_187109, _187107))], (180 ^ _156207) ^ [_162447, _162449] : [-(set_intersection2(_162449, _162447) = set_intersection2(_162447, _162449))], (108 ^ _156207) ^ [_159843, _159845, _159847, _159849] : [-(ordered_pair(_159849, _159845) = ordered_pair(_159847, _159843)), _159849 = _159847, _159845 = _159843], (231 ^ _156207) ^ [_164230] : [_164230 = empty_set, 234 ^ _156207 : [(235 ^ _156207) ^ [_164343] : [in(_164343, _164230)]]], (72 ^ _156207) ^ [_158590, _158592, _158594, _158596] : [-(in(_158594, _158590)), in(_158596, _158592), _158596 = _158594, _158592 = _158590], (974 ^ _156207) ^ [_190272, _190274] : [subset(_190274, _190272), -(_190272 = set_union2(_190274, set_difference(_190272, _190274)))], (578 ^ _156207) ^ [_177118, _177120] : [set_intersection2(_177120, _177118) = empty_set, -(disjoint(_177120, _177118))], (118 ^ _156207) ^ [_160202, _160204, _160206, _160208] : [-(set_intersection2(_160208, _160204) = set_intersection2(_160206, _160202)), _160208 = _160206, _160204 = _160202], (626 ^ _156207) ^ [] : [true___, -(true___)], (784 ^ _156207) ^ [] : [empty(782 ^ [])], (1039 ^ _156207) ^ [_192605, _192607] : [-(subset(_192607, set_union2(_192607, _192605)))], (666 ^ _156207) ^ [_179245, _179247] : [-(empty(_179247)), empty(set_union2(_179247, _179245))], (318 ^ _156207) ^ [_167319, _167321, _167323] : [_167319 = set_union2(_167323, _167321), 321 ^ _156207 : [(322 ^ _156207) ^ [_167501] : [in(_167501, _167319), -(in(_167501, _167323)), -(in(_167501, _167321))], (332 ^ _156207) ^ [_167779] : [333 ^ _156207 : [(336 ^ _156207) ^ [] : [in(_167779, _167321)], (334 ^ _156207) ^ [] : [in(_167779, _167323)]], -(in(_167779, _167319))]]], (915 ^ _156207) ^ [_188198, _188200, _188202] : [-(subset(unordered_pair(_188202, _188200), _188198)), in(_188202, _188198), in(_188200, _188198)], (128 ^ _156207) ^ [_160561, _160563, _160565, _160567] : [-(set_union2(_160567, _160563) = set_union2(_160565, _160561)), _160567 = _160565, _160563 = _160561], (698 ^ _156207) ^ [_180476, _180478] : [-(in(_180478, _180476)), -(disjoint(singleton(_180478), _180476))], (138 ^ _156207) ^ [_160920, _160922, _160924, _160926] : [-(unordered_pair(_160926, _160922) = unordered_pair(_160924, _160920)), _160926 = _160924, _160922 = _160920], (834 ^ _156207) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (986 ^ _156207) ^ [_190699, _190701] : [-(set_difference(_190701, set_difference(_190701, _190699)) = set_intersection2(_190701, _190699))], (710 ^ _156207) ^ [_180888, _180890] : [in(_180890, _180888), -(subset(singleton(_180890), _180888))], (505 ^ _156207) ^ [_174438, _174440] : [-(_174438 = union(_174440)), 518 ^ _156207 : [(523 ^ _156207) ^ [] : [in(506 ^ [_174438, _174440], _174438)], (521 ^ _156207) ^ [] : [-(in(517 ^ [_174438, _174440], _174440))], (519 ^ _156207) ^ [] : [-(in(506 ^ [_174438, _174440], 517 ^ [_174438, _174440]))]], 509 ^ _156207 : [(512 ^ _156207) ^ [_174721] : [in(506 ^ [_174438, _174440], _174721), in(_174721, _174440)], (510 ^ _156207) ^ [] : [-(in(506 ^ [_174438, _174440], _174438))]]], (190 ^ _156207) ^ [_162828, _162830] : [-(_162830 = _162828), subset(_162830, _162828), subset(_162828, _162830)], (738 ^ _156207) ^ [_181882, _181884] : [subset(_181884, singleton(_181882)), -(_181884 = empty_set), -(_181884 = singleton(_181882))], (824 ^ _156207) ^ [_184889, _184891, _184893] : [-(subset(_184893, _184889)), subset(_184893, _184891), subset(_184891, _184889)], (972 ^ _156207) ^ [_190154, _190156] : [-(set_difference(set_union2(_190156, _190154), _190154) = set_difference(_190156, _190154))], (430 ^ _156207) ^ [_171686, _171688] : [432 ^ _156207 : [(435 ^ _156207) ^ [] : [in(431 ^ [_171686, _171688], _171686)], (433 ^ _156207) ^ [] : [-(in(431 ^ [_171686, _171688], _171688))]], -(subset(_171688, _171686))], (680 ^ _156207) ^ [_179759, _179761] : [-(set_intersection2(_179761, _179761) = _179761)], (1019 ^ _156207) ^ [_191895] : [-(unordered_pair(_191895, _191895) = singleton(_191895))], (781 ^ _156207) ^ [] : [-(empty(779 ^ []))], (716 ^ _156207) ^ [_181133, _181135] : [set_difference(_181135, _181133) = empty_set, -(subset(_181135, _181133))], (842 ^ _156207) ^ [_185493, _185495] : [subset(_185495, _185493), -(set_intersection2(_185495, _185493) = _185495)], (549 ^ _156207) ^ [_176059, _176061, _176063] : [-(_176059 = set_difference(_176063, _176061)), 561 ^ _156207 : [(566 ^ _156207) ^ [] : [in(550 ^ [_176059, _176061, _176063], _176059)], (564 ^ _156207) ^ [] : [in(550 ^ [_176059, _176061, _176063], _176061)], (562 ^ _156207) ^ [] : [-(in(550 ^ [_176059, _176061, _176063], _176063))]], 553 ^ _156207 : [(556 ^ _156207) ^ [] : [in(550 ^ [_176059, _176061, _176063], _176063), -(in(550 ^ [_176059, _176061, _176063], _176061))], (554 ^ _156207) ^ [] : [-(in(550 ^ [_176059, _176061, _176063], _176059))]]], (260 ^ _156207) ^ [_165221, _165223] : [-(_165221 = powerset(_165223)), 264 ^ _156207 : [(267 ^ _156207) ^ [] : [subset(261 ^ [_165221, _165223], _165223)], (265 ^ _156207) ^ [] : [-(in(261 ^ [_165221, _165223], _165221))]], 268 ^ _156207 : [(271 ^ _156207) ^ [] : [in(261 ^ [_165221, _165223], _165221)], (269 ^ _156207) ^ [] : [-(subset(261 ^ [_165221, _165223], _165223))]]], (275 ^ _156207) ^ [_165800, _165802, _165804] : [_165800 = unordered_pair(_165804, _165802), 278 ^ _156207 : [(279 ^ _156207) ^ [_165982] : [in(_165982, _165800), -(_165982 = _165804), -(_165982 = _165802)], (289 ^ _156207) ^ [_166260] : [290 ^ _156207 : [(293 ^ _156207) ^ [] : [_166260 = _165802], (291 ^ _156207) ^ [] : [_166260 = _165804]], -(in(_166260, _165800))]]], (684 ^ _156207) ^ [_179934] : [singleton(_179934) = empty_set], (927 ^ _156207) ^ [_188647, _188649] : [subset(_188649, singleton(_188647)), -(_188649 = empty_set), -(_188649 = singleton(_188647))], (980 ^ _156207) ^ [_190494, _190496] : [in(_190496, _190494), -(set_union2(singleton(_190496), _190494) = _190494)], (297 ^ _156207) ^ [_166525, _166527, _166529] : [-(_166525 = unordered_pair(_166529, _166527)), 301 ^ _156207 : [(306 ^ _156207) ^ [] : [298 ^ [_166525, _166527, _166529] = _166527], (304 ^ _156207) ^ [] : [298 ^ [_166525, _166527, _166529] = _166529], (302 ^ _156207) ^ [] : [-(in(298 ^ [_166525, _166527, _166529], _166525))]], 307 ^ _156207 : [(308 ^ _156207) ^ [] : [-(298 ^ [_166525, _166527, _166529] = _166529), -(298 ^ [_166525, _166527, _166529] = _166527)], (314 ^ _156207) ^ [] : [in(298 ^ [_166525, _166527, _166529], _166525)]]], (1053 ^ _156207) ^ [_193132, _193134] : [empty(_193134), -(_193134 = _193132), empty(_193132)], (873 ^ _156207) ^ [_186668, _186670, _186672, _186674] : [ordered_pair(_186674, _186672) = ordered_pair(_186670, _186668), 876 ^ _156207 : [(879 ^ _156207) ^ [] : [-(_186672 = _186668)], (877 ^ _156207) ^ [] : [-(_186674 = _186670)]]], (158 ^ _156207) ^ [_161590, _161592] : [_161592 = _161590, -(singleton(_161592) = singleton(_161590))], (1021 ^ _156207) ^ [_191993] : [empty(_191993), -(_191993 = empty_set)], (686 ^ _156207) ^ [_180043, _180045] : [in(_180045, _180043), -(set_union2(singleton(_180045), _180043) = _180043)], (762 ^ _156207) ^ [_182707, _182709, _182711, _182713] : [in(ordered_pair(_182713, _182711), cartesian_product2(_182709, _182707)), 765 ^ _156207 : [(768 ^ _156207) ^ [] : [-(in(_182711, _182707))], (766 ^ _156207) ^ [] : [-(in(_182713, _182709))]]], (461 ^ _156207) ^ [_172811, _172813, _172815] : [-(_172811 = set_intersection2(_172815, _172813)), 473 ^ _156207 : [(478 ^ _156207) ^ [] : [in(462 ^ [_172811, _172813, _172815], _172811)], (476 ^ _156207) ^ [] : [-(in(462 ^ [_172811, _172813, _172815], _172813))], (474 ^ _156207) ^ [] : [-(in(462 ^ [_172811, _172813, _172815], _172815))]], 465 ^ _156207 : [(468 ^ _156207) ^ [] : [in(462 ^ [_172811, _172813, _172815], _172815), in(462 ^ [_172811, _172813, _172815], _172813)], (466 ^ _156207) ^ [] : [-(in(462 ^ [_172811, _172813, _172815], _172811))]]], (988 ^ _156207) ^ [_190788] : [-(set_difference(empty_set, _190788) = empty_set)], (102 ^ _156207) ^ [_159597, _159599] : [_159599 = _159597, -(powerset(_159599) = powerset(_159597))], (810 ^ _156207) ^ [_184353, _184355] : [-(subset(set_intersection2(_184355, _184353), _184355))], (244 ^ _156207) ^ [_164700, _164702] : [_164700 = powerset(_164702), 247 ^ _156207 : [(254 ^ _156207) ^ [_165042] : [subset(_165042, _164702), -(in(_165042, _164700))], (248 ^ _156207) ^ [_164870] : [in(_164870, _164700), -(subset(_164870, _164702))]]], (572 ^ _156207) ^ [_176950, _176952] : [disjoint(_176952, _176950), -(set_intersection2(_176952, _176950) = empty_set)], (728 ^ _156207) ^ [_181533, _181535, _181537] : [subset(_181537, _181535), -(in(_181533, _181537)), -(subset(_181537, set_difference(_181535, singleton(_181533))))], (756 ^ _156207) ^ [_182436, _182438] : [in(_182438, _182436), -(subset(_182438, union(_182436)))], (682 ^ _156207) ^ [_179855, _179857] : [proper_subset(_179857, _179857)], (788 ^ _156207) ^ [_183578, _183580] : [disjoint(_183580, _183578), -(disjoint(_183578, _183580))], (1027 ^ _156207) ^ [_192195, _192197] : [subset(singleton(_192197), singleton(_192195)), -(_192197 = _192195)], (178 ^ _156207) ^ [_162347, _162349] : [-(set_union2(_162349, _162347) = set_union2(_162347, _162349))], (650 ^ _156207) ^ [] : [true___, -(true___)], (867 ^ _156207) ^ [_186412, _186414, _186416] : [subset(_186416, _186414), -(subset(set_difference(_186416, _186412), set_difference(_186414, _186412)))], (966 ^ _156207) ^ [_189965] : [subset(_189965, empty_set), -(_189965 = empty_set)], (176 ^ _156207) ^ [_162247, _162249] : [-(unordered_pair(_162249, _162247) = unordered_pair(_162247, _162249))], (237 ^ _156207) ^ [_164409] : [-(in(238 ^ [_164409], _164409)), -(_164409 = empty_set)], (170 ^ _156207) ^ [_162051, _162053] : [proper_subset(_162053, _162051), proper_subset(_162051, _162053)], (10 ^ _156207) ^ [_156642, _156644, _156646] : [-(_156646 = _156642), _156646 = _156644, _156644 = _156642], (748 ^ _156207) ^ [_182142, _182144] : [749 ^ _156207 : [(752 ^ _156207) ^ [] : [_182144 = singleton(_182142)], (750 ^ _156207) ^ [] : [_182144 = empty_set]], -(subset(_182144, singleton(_182142)))], (786 ^ _156207) ^ [_183469, _183471] : [-(subset(_183471, _183471))], (956 ^ _156207) ^ [_189616, _189618] : [disjoint(_189618, _189616), 957 ^ _156207 : [(958 ^ _156207) ^ [_189708] : [in(_189708, _189618), in(_189708, _189616)]]], (997 ^ _156207) ^ [_191153, _191155] : [998 ^ _156207 : [(999 ^ _156207) ^ [_191226] : [in(_191226, set_intersection2(_191155, _191153))]], disjoint(_191155, _191153)], (812 ^ _156207) ^ [_184479, _184481, _184483] : [-(subset(_184483, set_intersection2(_184481, _184479))), subset(_184483, _184481), subset(_184483, _184479)], (925 ^ _156207) ^ [_188500, _188502] : [-(set_union2(_188502, set_difference(_188500, _188502)) = set_union2(_188502, _188500))], (804 ^ _156207) ^ [_184152, _184154] : [subset(_184154, _184152), -(set_union2(_184154, _184152) = _184152)], (704 ^ _156207) ^ [_180722, _180724] : [subset(singleton(_180724), _180722), -(in(_180724, _180722))], (570 ^ _156207) ^ [_176801, _176803] : [-(ordered_pair(_176803, _176801) = unordered_pair(unordered_pair(_176803, _176801), singleton(_176803)))], (527 ^ _156207) ^ [_175328, _175330, _175332] : [_175328 = set_difference(_175332, _175330), 530 ^ _156207 : [(539 ^ _156207) ^ [_175772] : [-(in(_175772, _175328)), in(_175772, _175332), -(in(_175772, _175330))], (531 ^ _156207) ^ [_175512] : [in(_175512, _175328), 534 ^ _156207 : [(537 ^ _156207) ^ [] : [in(_175512, _175330)], (535 ^ _156207) ^ [] : [-(in(_175512, _175332))]]]]], (692 ^ _156207) ^ [_180263, _180265] : [disjoint(singleton(_180265), _180263), in(_180265, _180263)], (58 ^ _156207) ^ [_158166, _158168, _158170, _158172] : [-(subset(_158170, _158166)), subset(_158172, _158168), _158172 = _158170, _158168 = _158166], (608 ^ _156207) ^ [] : [true___, -(true___)], (937 ^ _156207) ^ [_188907, _188909] : [938 ^ _156207 : [(941 ^ _156207) ^ [] : [_188909 = singleton(_188907)], (939 ^ _156207) ^ [] : [_188909 = empty_set]], -(subset(_188909, singleton(_188907)))], (770 ^ _156207) ^ [_182972, _182974, _182976, _182978] : [-(in(ordered_pair(_182978, _182976), cartesian_product2(_182974, _182972))), in(_182978, _182974), in(_182976, _182972)], (420 ^ _156207) ^ [_171372, _171374] : [subset(_171374, _171372), 423 ^ _156207 : [(424 ^ _156207) ^ [_171509] : [in(_171509, _171374), -(in(_171509, _171372))]]], (439 ^ _156207) ^ [_172086, _172088, _172090] : [_172086 = set_intersection2(_172090, _172088), 442 ^ _156207 : [(451 ^ _156207) ^ [_172527] : [-(in(_172527, _172086)), in(_172527, _172090), in(_172527, _172088)], (443 ^ _156207) ^ [_172268] : [in(_172268, _172086), 446 ^ _156207 : [(449 ^ _156207) ^ [] : [-(in(_172268, _172088))], (447 ^ _156207) ^ [] : [-(in(_172268, _172090))]]]]], (901 ^ _156207) ^ [_187688, _187690] : [in(_187690, _187688), -(subset(singleton(_187690), _187688))], (822 ^ _156207) ^ [_184765] : [-(set_union2(_184765, empty_set) = _184765)], (216 ^ _156207) ^ [_163679, _163681] : [-(_163679 = singleton(_163681)), 220 ^ _156207 : [(223 ^ _156207) ^ [] : [217 ^ [_163679, _163681] = _163681], (221 ^ _156207) ^ [] : [-(in(217 ^ [_163679, _163681], _163679))]], 224 ^ _156207 : [(227 ^ _156207) ^ [] : [in(217 ^ [_163679, _163681], _163679)], (225 ^ _156207) ^ [] : [-(217 ^ [_163679, _163681] = _163681)]]], (34 ^ _156207) ^ [_157427, _157429, _157431, _157433] : [-(disjoint(_157431, _157427)), disjoint(_157433, _157429), _157433 = _157431, _157429 = _157427], (678 ^ _156207) ^ [_179662, _179664] : [-(set_union2(_179664, _179664) = _179664)], (947 ^ _156207) ^ [_189302, _189304] : [-(disjoint(_189304, _189302)), 951 ^ _156207 : [(954 ^ _156207) ^ [] : [-(in(950 ^ [_189302, _189304], _189302))], (952 ^ _156207) ^ [] : [-(in(950 ^ [_189302, _189304], _189304))]]], (836 ^ _156207) ^ [_185265, _185267, _185269] : [subset(_185269, _185267), -(subset(set_intersection2(_185269, _185265), set_intersection2(_185267, _185265)))], (1079 ^ _156207) ^ [_193992, _193994, _193996] : [singleton(_193996) = unordered_pair(_193994, _193992), -(_193994 = _193992)], (895 ^ _156207) ^ [_187522, _187524] : [subset(singleton(_187524), _187522), -(in(_187524, _187522))], (794 ^ _156207) ^ [_183816, _183818, _183820, _183822] : [unordered_pair(_183822, _183820) = unordered_pair(_183818, _183816), -(_183822 = _183818), -(_183822 = _183816)], (848 ^ _156207) ^ [_185680] : [-(set_intersection2(_185680, empty_set) = empty_set)], (482 ^ _156207) ^ [_173593, _173595] : [_173593 = union(_173595), 485 ^ _156207 : [(495 ^ _156207) ^ [_174101] : [-(in(_174101, _173593)), 496 ^ _156207 : [(497 ^ _156207) ^ [_174199] : [in(_174101, _174199), in(_174199, _173595)]]], (486 ^ _156207) ^ [_173774] : [in(_173774, _173593), 490 ^ _156207 : [(493 ^ _156207) ^ [] : [-(in(489 ^ [_173593, _173595, _173774], _173595))], (491 ^ _156207) ^ [] : [-(in(_173774, 489 ^ [_173593, _173595, _173774]))]]]]], (92 ^ _156207) ^ [_159266, _159268, _159270, _159272] : [-(cartesian_product2(_159272, _159268) = cartesian_product2(_159270, _159266)), _159272 = _159270, _159268 = _159266], (164 ^ _156207) ^ [_161840, _161842] : [in(_161842, _161840), in(_161840, _161842)], (850 ^ _156207) ^ [_185790, _185792] : [-(_185792 = _185790), 854 ^ _156207 : [(857 ^ _156207) ^ [] : [in(851 ^ [_185790, _185792], _185790)], (855 ^ _156207) ^ [] : [-(in(851 ^ [_185790, _185792], _185792))]], 858 ^ _156207 : [(861 ^ _156207) ^ [] : [in(851 ^ [_185790, _185792], _185792)], (859 ^ _156207) ^ [] : [-(in(851 ^ [_185790, _185792], _185790))]]], (584 ^ _156207) ^ [_177365, _177367] : [proper_subset(_177367, _177365), 587 ^ _156207 : [(590 ^ _156207) ^ [] : [_177367 = _177365], (588 ^ _156207) ^ [] : [-(subset(_177367, _177365))]]], (638 ^ _156207) ^ [] : [true___, -(true___)], (662 ^ _156207) ^ [] : [-(empty(empty_set))], (148 ^ _156207) ^ [_161279, _161281, _161283, _161285] : [-(set_difference(_161285, _161281) = set_difference(_161283, _161279)), _161285 = _161283, _161281 = _161279], (340 ^ _156207) ^ [_168044, _168046, _168048] : [-(_168044 = set_union2(_168048, _168046)), 344 ^ _156207 : [(349 ^ _156207) ^ [] : [in(341 ^ [_168044, _168046, _168048], _168046)], (347 ^ _156207) ^ [] : [in(341 ^ [_168044, _168046, _168048], _168048)], (345 ^ _156207) ^ [] : [-(in(341 ^ [_168044, _168046, _168048], _168044))]], 350 ^ _156207 : [(351 ^ _156207) ^ [] : [-(in(341 ^ [_168044, _168046, _168048], _168048)), -(in(341 ^ [_168044, _168046, _168048], _168046))], (357 ^ _156207) ^ [] : [in(341 ^ [_168044, _168046, _168048], _168044)]]], (865 ^ _156207) ^ [_186291] : [-(subset(empty_set, _186291))], (1073 ^ _156207) ^ [_193772, _193774, _193776] : [singleton(_193776) = unordered_pair(_193774, _193772), -(_193776 = _193774)], (614 ^ _156207) ^ [] : [true___, -(true___)], (1009 ^ _156207) ^ [_191615, _191617, _191619] : [-(disjoint(_191619, _191615)), subset(_191619, _191617), disjoint(_191617, _191615)], (990 ^ _156207) ^ [_190918, _190920] : [-(disjoint(_190920, _190918)), -(in(993 ^ [_190918, _190920], set_intersection2(_190920, _190918)))], (881 ^ _156207) ^ [_186966, _186968] : [-(subset(set_difference(_186968, _186966), _186968))], (632 ^ _156207) ^ [] : [true___, -(true___)], (48 ^ _156207) ^ [_157843, _157845] : [-(empty(_157843)), _157845 = _157843, empty(_157845)], (664 ^ _156207) ^ [_179134, _179136] : [empty(ordered_pair(_179136, _179134))], (620 ^ _156207) ^ [] : [true___, -(true___)], (20 ^ _156207) ^ [_156983, _156985, _156987, _156989] : [-(proper_subset(_156987, _156983)), proper_subset(_156989, _156985), _156989 = _156987, _156985 = _156983], (4 ^ _156207) ^ [_156438, _156440] : [_156440 = _156438, -(_156438 = _156440)], (945 ^ _156207) ^ [_189172] : [-(set_difference(_189172, empty_set) = _189172)], (644 ^ _156207) ^ [] : [true___, -(true___)], (592 ^ _156207) ^ [_177603, _177605] : [-(proper_subset(_177605, _177603)), subset(_177605, _177603), -(_177605 = _177603)], (656 ^ _156207) ^ [] : [true___, -(true___)], (361 ^ _156207) ^ [_168838, _168840, _168842] : [_168838 = cartesian_product2(_168842, _168840), 364 ^ _156207 : [(377 ^ _156207) ^ [_169599] : [-(in(_169599, _168838)), 378 ^ _156207 : [(379 ^ _156207) ^ [_169729, _169731] : [in(_169731, _168842), in(_169729, _168840), _169599 = ordered_pair(_169731, _169729)]]], (365 ^ _156207) ^ [_169039] : [in(_169039, _168838), 370 ^ _156207 : [(375 ^ _156207) ^ [] : [-(_169039 = ordered_pair(368 ^ [_168838, _168840, _168842, _169039], 369 ^ [_168838, _168840, _168842, _169039]))], (373 ^ _156207) ^ [] : [-(in(369 ^ [_168838, _168840, _168842, _169039], _168840))], (371 ^ _156207) ^ [] : [-(in(368 ^ [_168838, _168840, _168842, _169039], _168842))]]]]], (889 ^ _156207) ^ [_187275, _187277] : [subset(_187277, _187275), -(set_difference(_187277, _187275) = empty_set)]], input).
% 44.17/43.80 ncf('1',plain,[1091 : -(in(1085 ^ [], 1084 ^ [])), 1095 : set_difference(1084 ^ [], singleton(1085 ^ [])) = 1084 ^ []],start(1087 ^ 0)).
% 44.17/43.80 ncf('1.1',plain,[in(1085 ^ [], 1084 ^ []), disjoint(singleton(1085 ^ []), 1084 ^ [])],extension(692 ^ 3,bind([[_180263, _180265], [1084 ^ [], 1085 ^ []]]))).
% 44.17/43.80 ncf('1.1.1',plain,[-(disjoint(singleton(1085 ^ []), 1084 ^ [])), disjoint(1084 ^ [], singleton(1085 ^ []))],extension(788 ^ 4,bind([[_183578, _183580], [singleton(1085 ^ []), 1084 ^ []]]))).
% 44.17/43.80 ncf('1.1.1.1',plain,[-(disjoint(1084 ^ [], singleton(1085 ^ []))), set_difference(1084 ^ [], singleton(1085 ^ [])) = 1084 ^ []],extension(1047 ^ 5,bind([[_192914, _192916], [singleton(1085 ^ []), 1084 ^ []]]))).
% 44.17/43.80 ncf('1.1.1.1.1',plain,[-(set_difference(1084 ^ [], singleton(1085 ^ [])) = 1084 ^ [])],extension(1089 ^ 6)).
% 44.17/43.80 ncf('1.2',plain,[-(set_difference(1084 ^ [], singleton(1085 ^ [])) = 1084 ^ []), disjoint(1084 ^ [], singleton(1085 ^ []))],extension(1041 ^ 3,bind([[_192746, _192748], [singleton(1085 ^ []), 1084 ^ []]]))).
% 44.17/43.80 ncf('1.2.1',plain,[-(disjoint(1084 ^ [], singleton(1085 ^ []))), disjoint(singleton(1085 ^ []), 1084 ^ [])],extension(788 ^ 4,bind([[_183578, _183580], [1084 ^ [], singleton(1085 ^ [])]]))).
% 44.17/43.80 ncf('1.2.1.1',plain,[-(disjoint(singleton(1085 ^ []), 1084 ^ [])), -(in(1085 ^ [], 1084 ^ []))],extension(698 ^ 5,bind([[_180476, _180478], [1084 ^ [], 1085 ^ []]]))).
% 44.17/43.80 ncf('1.2.1.1.1',plain,[in(1085 ^ [], 1084 ^ [])],extension(1093 ^ 6)).
% 44.17/43.80 %-----------------------------------------------------
% 44.17/43.80 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------