%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU153+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:24 EDT 2023
% Result : Theorem 46.63s 45.89s
% Output : Proof 46.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU153+2 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 13:06:37 EDT 2023
% 0.12/0.33 % CPUTime :
% 46.63/45.89
% 46.63/45.89 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 46.63/45.89 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.63/45.89 %-----------------------------------------------------
% 46.63/45.89 ncf(matrix, plain, [(839 ^ _152150) ^ [] : [-(in(834 ^ [], 835 ^ []))], (837 ^ _152150) ^ [] : [-(disjoint(singleton(834 ^ []), 835 ^ []))], !, (747 ^ _122954) ^ [_148663, _148665] : [748 ^ _122954 : [(749 ^ _122954) ^ [_148736] : [in(_148736, set_intersection2(_148665, _148663))]], disjoint(_148665, _148663)], (528 ^ _122954) ^ [_140734, _140736] : [-(set_intersection2(_140736, _140736) = _140736)], (470 ^ _122954) ^ [] : [true___, -(true___)], (598 ^ _122954) ^ [_143145, _143147] : [-(subset(_143147, _143147))], (558 ^ _122954) ^ [_141846, _141848] : [subset(_141848, _141846), -(set_difference(_141848, _141846) = empty_set)], (648 ^ _122954) ^ [_144941, _144943, _144945] : [subset(_144945, _144943), -(subset(set_intersection2(_144945, _144941), set_intersection2(_144943, _144941)))], (532 ^ _122954) ^ [_140909] : [singleton(_140909) = empty_set], (144 ^ _122954) ^ [_127852, _127854] : [proper_subset(_127854, _127852), proper_subset(_127852, _127854)], (520 ^ _122954) ^ [_140436, _140438] : [-(empty(_140438)), empty(set_union2(_140436, _140438))], (574 ^ _122954) ^ [_142427, _142429] : [subset(_142429, singleton(_142427)), -(_142429 = empty_set), -(_142429 = singleton(_142427))], (132 ^ _122954) ^ [_127401, _127403] : [_127403 = _127401, -(singleton(_127403) = singleton(_127401))], (397 ^ _122954) ^ [_136860, _136862, _136864] : [_136860 = set_difference(_136864, _136862), 400 ^ _122954 : [(409 ^ _122954) ^ [_137304] : [-(in(_137304, _136860)), in(_137304, _136864), -(in(_137304, _136862))], (401 ^ _122954) ^ [_137044] : [in(_137044, _136860), 404 ^ _122954 : [(407 ^ _122954) ^ [] : [in(_137044, _136862)], (405 ^ _122954) ^ [] : [-(in(_137044, _136864))]]]]], (314 ^ _122954) ^ [_133845, _133847, _133849] : [-(_133845 = set_union2(_133849, _133847)), 318 ^ _122954 : [(323 ^ _122954) ^ [] : [in(315 ^ [_133845, _133847, _133849], _133847)], (321 ^ _122954) ^ [] : [in(315 ^ [_133845, _133847, _133849], _133849)], (319 ^ _122954) ^ [] : [-(in(315 ^ [_133845, _133847, _133849], _133845))]], 324 ^ _122954 : [(325 ^ _122954) ^ [] : [-(in(315 ^ [_133845, _133847, _133849], _133849)), -(in(315 ^ [_133845, _133847, _133849], _133847))], (331 ^ _122954) ^ [] : [in(315 ^ [_133845, _133847, _133849], _133845)]]], (345 ^ _122954) ^ [_134939, _134941] : [347 ^ _122954 : [(350 ^ _122954) ^ [] : [in(346 ^ [_134939, _134941], _134939)], (348 ^ _122954) ^ [] : [-(in(346 ^ [_134939, _134941], _134941))]], -(subset(_134941, _134939))], (803 ^ _122954) ^ [_150642, _150644] : [empty(_150644), -(_150644 = _150642), empty(_150642)], (596 ^ _122954) ^ [] : [empty(594 ^ [])], (4 ^ _122954) ^ [_123185, _123187] : [_123187 = _123185, -(_123185 = _123187)], (512 ^ _122954) ^ [] : [-(empty(empty_set))], (102 ^ _122954) ^ [_126372, _126374, _126376, _126378] : [-(set_difference(_126378, _126374) = set_difference(_126376, _126372)), _126378 = _126376, _126374 = _126372], (677 ^ _122954) ^ [_145967] : [-(subset(empty_set, _145967))], (34 ^ _122954) ^ [_124146, _124148] : [-(empty(_124146)), _124148 = _124146, empty(_124148)], (271 ^ _122954) ^ [_132326, _132328, _132330] : [-(_132326 = unordered_pair(_132330, _132328)), 275 ^ _122954 : [(280 ^ _122954) ^ [] : [272 ^ [_132326, _132328, _132330] = _132328], (278 ^ _122954) ^ [] : [272 ^ [_132326, _132328, _132330] = _132330], (276 ^ _122954) ^ [] : [-(in(272 ^ [_132326, _132328, _132330], _132326))]], 281 ^ _122954 : [(282 ^ _122954) ^ [] : [-(272 ^ [_132326, _132328, _132330] = _132330), -(272 ^ [_132326, _132328, _132330] = _132328)], (288 ^ _122954) ^ [] : [in(272 ^ [_132326, _132328, _132330], _132326)]]], (2 ^ _122954) ^ [_123078] : [-(_123078 = _123078)], (234 ^ _122954) ^ [_131022, _131024] : [-(_131022 = powerset(_131024)), 238 ^ _122954 : [(241 ^ _122954) ^ [] : [subset(235 ^ [_131022, _131024], _131024)], (239 ^ _122954) ^ [] : [-(in(235 ^ [_131022, _131024], _131022))]], 242 ^ _122954 : [(245 ^ _122954) ^ [] : [in(235 ^ [_131022, _131024], _131022)], (243 ^ _122954) ^ [] : [-(subset(235 ^ [_131022, _131024], _131024))]]], (292 ^ _122954) ^ [_133120, _133122, _133124] : [_133120 = set_union2(_133124, _133122), 295 ^ _122954 : [(296 ^ _122954) ^ [_133302] : [in(_133302, _133120), -(in(_133302, _133124)), -(in(_133302, _133122))], (306 ^ _122954) ^ [_133580] : [307 ^ _122954 : [(310 ^ _122954) ^ [] : [in(_133580, _133122)], (308 ^ _122954) ^ [] : [in(_133580, _133124)]], -(in(_133580, _133120))]]], (211 ^ _122954) ^ [_130210] : [-(in(212 ^ [_130210], _130210)), -(_130210 = empty_set)], (335 ^ _122954) ^ [_134625, _134627] : [subset(_134627, _134625), 338 ^ _122954 : [(339 ^ _122954) ^ [_134762] : [in(_134762, _134627), -(in(_134762, _134625))]]], (546 ^ _122954) ^ [_141433, _141435] : [in(_141435, _141433), -(subset(singleton(_141435), _141433))], (759 ^ _122954) ^ [_149125, _149127, _149129] : [-(disjoint(_149129, _149125)), subset(_149129, _149127), disjoint(_149127, _149125)], (622 ^ _122954) ^ [_144029, _144031] : [-(subset(set_intersection2(_144031, _144029), _144031))], (791 ^ _122954) ^ [_150256, _150258] : [disjoint(_150258, _150256), -(set_difference(_150258, _150256) = _150258)], (419 ^ _122954) ^ [_137591, _137593, _137595] : [-(_137591 = set_difference(_137595, _137593)), 431 ^ _122954 : [(436 ^ _122954) ^ [] : [in(420 ^ [_137591, _137593, _137595], _137591)], (434 ^ _122954) ^ [] : [in(420 ^ [_137591, _137593, _137595], _137593)], (432 ^ _122954) ^ [] : [-(in(420 ^ [_137591, _137593, _137595], _137595))]], 423 ^ _122954 : [(426 ^ _122954) ^ [] : [in(420 ^ [_137591, _137593, _137595], _137595), -(in(420 ^ [_137591, _137593, _137595], _137593))], (424 ^ _122954) ^ [] : [-(in(420 ^ [_137591, _137593, _137595], _137591))]]], (738 ^ _122954) ^ [_148298] : [-(set_difference(empty_set, _148298) = empty_set)], (783 ^ _122954) ^ [_149923, _149925] : [in(_149925, _149923), empty(_149923)], (753 ^ _122954) ^ [_148902, _148904] : [subset(_148904, _148902), proper_subset(_148902, _148904)], (829 ^ _122954) ^ [_151502, _151504, _151506] : [singleton(_151506) = unordered_pair(_151504, _151502), -(_151504 = _151502)], (460 ^ _122954) ^ [_139030, _139032] : [-(proper_subset(_139032, _139030)), subset(_139032, _139030), -(_139032 = _139030)], (506 ^ _122954) ^ [] : [true___, -(true___)], (728 ^ _122954) ^ [_147884, _147886] : [-(set_difference(set_union2(_147886, _147884), _147884) = set_difference(_147886, _147884))], (86 ^ _122954) ^ [_125767, _125769] : [_125769 = _125767, -(powerset(_125769) = powerset(_125767))], (488 ^ _122954) ^ [] : [true___, -(true___)], (92 ^ _122954) ^ [_126013, _126015, _126017, _126019] : [-(set_intersection2(_126019, _126015) = set_intersection2(_126017, _126013)), _126019 = _126017, _126015 = _126013], (205 ^ _122954) ^ [_130031] : [_130031 = empty_set, 208 ^ _122954 : [(209 ^ _122954) ^ [_130144] : [in(_130144, _130031)]]], (552 ^ _122954) ^ [_141678, _141680] : [set_difference(_141680, _141678) = empty_set, -(subset(_141680, _141678))], (190 ^ _122954) ^ [_129480, _129482] : [-(_129480 = singleton(_129482)), 194 ^ _122954 : [(197 ^ _122954) ^ [] : [191 ^ [_129480, _129482] = _129482], (195 ^ _122954) ^ [] : [-(in(191 ^ [_129480, _129482], _129480))]], 198 ^ _122954 : [(201 ^ _122954) ^ [] : [in(191 ^ [_129480, _129482], _129480)], (199 ^ _122954) ^ [] : [-(191 ^ [_129480, _129482] = _129482)]]], (584 ^ _122954) ^ [_142687, _142689] : [585 ^ _122954 : [(588 ^ _122954) ^ [] : [_142689 = singleton(_142687)], (586 ^ _122954) ^ [] : [_142689 = empty_set]], -(subset(_142689, singleton(_142687)))], (606 ^ _122954) ^ [_143492, _143494, _143496, _143498] : [unordered_pair(_143498, _143496) = unordered_pair(_143494, _143492), -(_143498 = _143494), -(_143498 = _143492)], (44 ^ _122954) ^ [_124469, _124471, _124473, _124475] : [-(subset(_124473, _124469)), subset(_124475, _124471), _124475 = _124473, _124471 = _124469], (740 ^ _122954) ^ [_148428, _148430] : [-(disjoint(_148430, _148428)), -(in(743 ^ [_148428, _148430], set_intersection2(_148430, _148428)))], (660 ^ _122954) ^ [_145356] : [-(set_intersection2(_145356, empty_set) = empty_set)], (376 ^ _122954) ^ [_136064, _136066, _136068] : [-(_136064 = set_intersection2(_136068, _136066)), 388 ^ _122954 : [(393 ^ _122954) ^ [] : [in(377 ^ [_136064, _136066, _136068], _136064)], (391 ^ _122954) ^ [] : [-(in(377 ^ [_136064, _136066, _136068], _136066))], (389 ^ _122954) ^ [] : [-(in(377 ^ [_136064, _136066, _136068], _136068))]], 380 ^ _122954 : [(383 ^ _122954) ^ [] : [in(377 ^ [_136064, _136066, _136068], _136068), in(377 ^ [_136064, _136066, _136068], _136066)], (381 ^ _122954) ^ [] : [-(in(377 ^ [_136064, _136066, _136068], _136064))]]], (152 ^ _122954) ^ [_128148, _128150] : [-(set_union2(_128150, _128148) = set_union2(_128148, _128150))], (164 ^ _122954) ^ [_128629, _128631] : [-(_128631 = _128629), subset(_128631, _128629), subset(_128629, _128631)], (530 ^ _122954) ^ [_140830, _140832] : [proper_subset(_140832, _140832)], (514 ^ _122954) ^ [_140220, _140222] : [-(empty(_140222)), empty(set_union2(_140222, _140220))], (636 ^ _122954) ^ [_144565, _144567, _144569] : [-(subset(_144569, _144565)), subset(_144569, _144567), subset(_144567, _144565)], (440 ^ _122954) ^ [_138377, _138379] : [disjoint(_138379, _138377), -(set_intersection2(_138379, _138377) = empty_set)], (218 ^ _122954) ^ [_130501, _130503] : [_130501 = powerset(_130503), 221 ^ _122954 : [(228 ^ _122954) ^ [_130843] : [subset(_130843, _130503), -(in(_130843, _130501))], (222 ^ _122954) ^ [_130671] : [in(_130671, _130501), -(subset(_130671, _130503))]]], (771 ^ _122954) ^ [_149503] : [empty(_149503), -(_149503 = empty_set)], (685 ^ _122954) ^ [_146301, _146303] : [-(subset(set_difference(_146303, _146301), _146303))], (122 ^ _122954) ^ [_127090, _127092, _127094, _127096] : [-(unordered_pair(_127096, _127092) = unordered_pair(_127094, _127090)), _127096 = _127094, _127092 = _127090], (249 ^ _122954) ^ [_131601, _131603, _131605] : [_131601 = unordered_pair(_131605, _131603), 252 ^ _122954 : [(253 ^ _122954) ^ [_131783] : [in(_131783, _131601), -(_131783 = _131605), -(_131783 = _131603)], (263 ^ _122954) ^ [_132061] : [264 ^ _122954 : [(267 ^ _122954) ^ [] : [_132061 = _131603], (265 ^ _122954) ^ [] : [_132061 = _131605]], -(in(_132061, _131601))]]], (703 ^ _122954) ^ [_147032, _147034] : [-(disjoint(_147034, _147032)), 707 ^ _122954 : [(710 ^ _122954) ^ [] : [-(in(706 ^ [_147032, _147034], _147032))], (708 ^ _122954) ^ [] : [-(in(706 ^ [_147032, _147034], _147034))]]], (174 ^ _122954) ^ [_128959, _128961] : [_128959 = singleton(_128961), 177 ^ _122954 : [(184 ^ _122954) ^ [_129301] : [_129301 = _128961, -(in(_129301, _128959))], (178 ^ _122954) ^ [_129129] : [in(_129129, _128959), -(_129129 = _128961)]]], (730 ^ _122954) ^ [_148002, _148004] : [subset(_148004, _148002), -(_148002 = set_union2(_148004, set_difference(_148002, _148004)))], (736 ^ _122954) ^ [_148209, _148211] : [-(set_difference(_148211, set_difference(_148211, _148209)) = set_intersection2(_148211, _148209))], (662 ^ _122954) ^ [_145466, _145468] : [-(_145468 = _145466), 666 ^ _122954 : [(669 ^ _122954) ^ [] : [in(663 ^ [_145466, _145468], _145466)], (667 ^ _122954) ^ [] : [-(in(663 ^ [_145466, _145468], _145468))]], 670 ^ _122954 : [(673 ^ _122954) ^ [] : [in(663 ^ [_145466, _145468], _145468)], (671 ^ _122954) ^ [] : [-(in(663 ^ [_145466, _145468], _145466))]]], (10 ^ _122954) ^ [_123389, _123391, _123393] : [-(_123393 = _123389), _123393 = _123391, _123391 = _123389], (679 ^ _122954) ^ [_146088, _146090, _146092] : [subset(_146092, _146090), -(subset(set_difference(_146092, _146088), set_difference(_146090, _146088)))], (564 ^ _122954) ^ [_142078, _142080, _142082] : [subset(_142082, _142080), -(in(_142078, _142082)), -(subset(_142082, set_difference(_142080, singleton(_142078))))], (482 ^ _122954) ^ [] : [true___, -(true___)], (446 ^ _122954) ^ [_138545, _138547] : [set_intersection2(_138547, _138545) = empty_set, -(disjoint(_138547, _138545))], (526 ^ _122954) ^ [_140637, _140639] : [-(set_union2(_140639, _140639) = _140639)], (687 ^ _122954) ^ [_146442, _146444] : [set_difference(_146444, _146442) = empty_set, -(subset(_146444, _146442))], (20 ^ _122954) ^ [_123730, _123732, _123734, _123736] : [-(proper_subset(_123734, _123730)), proper_subset(_123736, _123732), _123736 = _123734, _123732 = _123730], (777 ^ _122954) ^ [_149705, _149707] : [subset(singleton(_149707), singleton(_149705)), -(_149707 = _149705)], (150 ^ _122954) ^ [_128048, _128050] : [-(unordered_pair(_128050, _128048) = unordered_pair(_128048, _128050))], (354 ^ _122954) ^ [_135339, _135341, _135343] : [_135339 = set_intersection2(_135343, _135341), 357 ^ _122954 : [(366 ^ _122954) ^ [_135780] : [-(in(_135780, _135339)), in(_135780, _135343), in(_135780, _135341)], (358 ^ _122954) ^ [_135521] : [in(_135521, _135339), 361 ^ _122954 : [(364 ^ _122954) ^ [] : [-(in(_135521, _135341))], (362 ^ _122954) ^ [] : [-(in(_135521, _135343))]]]]], (540 ^ _122954) ^ [_141267, _141269] : [subset(singleton(_141269), _141267), -(in(_141269, _141267))], (500 ^ _122954) ^ [] : [true___, -(true___)], (693 ^ _122954) ^ [_146610, _146612] : [subset(_146612, _146610), -(set_difference(_146612, _146610) = empty_set)], (722 ^ _122954) ^ [_147695] : [subset(_147695, empty_set), -(_147695 = empty_set)], (138 ^ _122954) ^ [_127641, _127643] : [in(_127643, _127641), in(_127641, _127643)], (476 ^ _122954) ^ [] : [true___, -(true___)], (154 ^ _122954) ^ [_128248, _128250] : [-(set_intersection2(_128250, _128248) = set_intersection2(_128248, _128250))], (452 ^ _122954) ^ [_138792, _138794] : [proper_subset(_138794, _138792), 455 ^ _122954 : [(458 ^ _122954) ^ [] : [_138794 = _138792], (456 ^ _122954) ^ [] : [-(subset(_138794, _138792))]]], (769 ^ _122954) ^ [_149405] : [-(unordered_pair(_149405, _149405) = singleton(_149405))], (654 ^ _122954) ^ [_145169, _145171] : [subset(_145171, _145169), -(set_intersection2(_145171, _145169) = _145171)], (616 ^ _122954) ^ [_143828, _143830] : [subset(_143830, _143828), -(set_union2(_143830, _143828) = _143828)], (797 ^ _122954) ^ [_150424, _150426] : [set_difference(_150426, _150424) = _150426, -(disjoint(_150426, _150424))], (156 ^ _122954) ^ [_128392, _128394] : [_128394 = _128392, 159 ^ _122954 : [(162 ^ _122954) ^ [] : [-(subset(_128392, _128394))], (160 ^ _122954) ^ [] : [-(subset(_128394, _128392))]]], (494 ^ _122954) ^ [] : [true___, -(true___)], (701 ^ _122954) ^ [_146902] : [-(set_difference(_146902, empty_set) = _146902)], (534 ^ _122954) ^ [_141018, _141020] : [in(_141020, _141018), -(set_union2(singleton(_141020), _141018) = _141018)], (646 ^ _122954) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (699 ^ _122954) ^ [_146813, _146815] : [-(set_union2(_146815, set_difference(_146813, _146815)) = set_union2(_146815, _146813))], (112 ^ _122954) ^ [_126731, _126733, _126735, _126737] : [-(set_union2(_126737, _126733) = set_union2(_126735, _126731)), _126737 = _126735, _126733 = _126731], (823 ^ _122954) ^ [_151282, _151284, _151286] : [singleton(_151286) = unordered_pair(_151284, _151282), -(_151286 = _151284)], (593 ^ _122954) ^ [] : [-(empty(591 ^ []))], (72 ^ _122954) ^ [_125337, _125339, _125341, _125343] : [-(in(_125341, _125337)), in(_125343, _125339), _125343 = _125341, _125339 = _125337], (624 ^ _122954) ^ [_144155, _144157, _144159] : [-(subset(_144159, set_intersection2(_144157, _144155))), subset(_144159, _144157), subset(_144159, _144155)], (634 ^ _122954) ^ [_144441] : [-(set_union2(_144441, empty_set) = _144441)], (712 ^ _122954) ^ [_147346, _147348] : [disjoint(_147348, _147346), 713 ^ _122954 : [(714 ^ _122954) ^ [_147438] : [in(_147438, _147348), in(_147438, _147346)]]], (58 ^ _122954) ^ [_124913, _124915, _124917, _124919] : [-(disjoint(_124917, _124913)), disjoint(_124919, _124915), _124919 = _124917, _124915 = _124913], (600 ^ _122954) ^ [_143254, _143256] : [disjoint(_143256, _143254), -(disjoint(_143254, _143256))], (813 ^ _122954) ^ [_150953, _150955, _150957] : [-(subset(set_union2(_150957, _150953), _150955)), subset(_150957, _150955), subset(_150953, _150955)], (789 ^ _122954) ^ [_150115, _150117] : [-(subset(_150117, set_union2(_150117, _150115)))]], input).
% 46.63/45.89 ncf('1',plain,[-(in(834 ^ [], 835 ^ []))],start(839 ^ 0)).
% 46.63/45.89 ncf('1.1',plain,[in(834 ^ [], 835 ^ []), -(subset(singleton(834 ^ []), 835 ^ []))],extension(546 ^ 1,bind([[_141433, _141435], [835 ^ [], 834 ^ []]]))).
% 46.63/45.89 ncf('1.1.1',plain,[subset(singleton(834 ^ []), 835 ^ []), -(set_intersection2(singleton(834 ^ []), 835 ^ []) = singleton(834 ^ []))],extension(654 ^ 2,bind([[_145169, _145171], [835 ^ [], singleton(834 ^ [])]]))).
% 46.63/45.89 ncf('1.1.1.1',plain,[set_intersection2(singleton(834 ^ []), 835 ^ []) = singleton(834 ^ []), 184 : set_intersection2(834 ^ [], 834 ^ []) = 834 ^ [], 184 : -(in(set_intersection2(834 ^ [], 834 ^ []), set_intersection2(singleton(834 ^ []), 835 ^ [])))],extension(174 ^ 3,bind([[_128959, _128961, _129301], [set_intersection2(singleton(834 ^ []), 835 ^ []), 834 ^ [], set_intersection2(834 ^ [], 834 ^ [])]]))).
% 46.63/45.89 ncf('1.1.1.1.1',plain,[-(set_intersection2(834 ^ [], 834 ^ []) = 834 ^ [])],extension(528 ^ 6,bind([[_140734, _140736], [_93992, 834 ^ []]]))).
% 46.63/45.89 ncf('1.1.1.1.2',plain,[in(set_intersection2(834 ^ [], 834 ^ []), set_intersection2(singleton(834 ^ []), 835 ^ [])), disjoint(singleton(834 ^ []), 835 ^ [])],extension(747 ^ 6,bind([[_148663, _148665, _148736], [835 ^ [], singleton(834 ^ []), set_intersection2(834 ^ [], 834 ^ [])]]))).
% 46.63/45.89 ncf('1.1.1.1.2.1',plain,[-(disjoint(singleton(834 ^ []), 835 ^ []))],extension(837 ^ 7)).
% 46.63/45.89 %-----------------------------------------------------
% 46.63/45.89 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------