%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU134+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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:19 EDT 2023
% Result : Theorem 0.26s 1.39s
% Output : Proof 0.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU134+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 13:08:58 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.26/1.39
% 0.26/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.26/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.26/1.39 %-----------------------------------------------------
% 0.26/1.39 ncf(matrix, plain, [(518 ^ _71842) ^ [] : [519 ^ _71842 : [(520 ^ _71842) ^ [] : [-(set_difference(515 ^ [], 516 ^ []) = empty_set)], (522 ^ _71842) ^ [] : [subset(515 ^ [], 516 ^ [])]], 523 ^ _71842 : [(524 ^ _71842) ^ [] : [-(subset(515 ^ [], 516 ^ []))], (526 ^ _71842) ^ [] : [set_difference(515 ^ [], 516 ^ []) = empty_set]]], (72 ^ _71842) ^ [_74257, _74259, _74261, _74263] : [-(set_intersection2(_74263, _74259) = set_intersection2(_74261, _74257)), _74263 = _74261, _74259 = _74257], (82 ^ _71842) ^ [_74616, _74618, _74620, _74622] : [-(set_union2(_74622, _74618) = set_union2(_74620, _74616)), _74622 = _74620, _74618 = _74616], (92 ^ _71842) ^ [_74955, _74957, _74959, _74961] : [-(set_difference(_74961, _74957) = set_difference(_74959, _74955)), _74961 = _74959, _74957 = _74955], (2 ^ _71842) ^ [_71986] : [-(_71986 = _71986)], (4 ^ _71842) ^ [_72093, _72095] : [_72095 = _72093, -(_72093 = _72095)], (10 ^ _71842) ^ [_72297, _72299, _72301] : [-(_72301 = _72297), _72301 = _72299, _72299 = _72297], (20 ^ _71842) ^ [_72638, _72640, _72642, _72644] : [-(disjoint(_72642, _72638)), disjoint(_72644, _72640), _72644 = _72642, _72640 = _72638], (34 ^ _71842) ^ [_73082, _73084, _73086, _73088] : [-(in(_73086, _73082)), in(_73088, _73084), _73088 = _73086, _73084 = _73082], (48 ^ _71842) ^ [_73498, _73500] : [-(empty(_73498)), _73500 = _73498, empty(_73500)], (58 ^ _71842) ^ [_73801, _73803, _73805, _73807] : [-(subset(_73805, _73801)), subset(_73807, _73803), _73807 = _73805, _73803 = _73801], (102 ^ _71842) ^ [_75296, _75298] : [in(_75298, _75296), in(_75296, _75298)], (108 ^ _71842) ^ [_75492, _75494] : [-(set_union2(_75494, _75492) = set_union2(_75492, _75494))], (110 ^ _71842) ^ [_75592, _75594] : [-(set_intersection2(_75594, _75592) = set_intersection2(_75592, _75594))], (112 ^ _71842) ^ [_75736, _75738] : [_75738 = _75736, 115 ^ _71842 : [(116 ^ _71842) ^ [] : [-(subset(_75738, _75736))], (118 ^ _71842) ^ [] : [-(subset(_75736, _75738))]]], (120 ^ _71842) ^ [_75973, _75975] : [-(_75975 = _75973), subset(_75975, _75973), subset(_75973, _75975)], (130 ^ _71842) ^ [_76289] : [_76289 = empty_set, 133 ^ _71842 : [(134 ^ _71842) ^ [_76402] : [in(_76402, _76289)]]], (136 ^ _71842) ^ [_76468] : [-(in(137 ^ [_76468], _76468)), -(_76468 = empty_set)], (165 ^ _71842) ^ [_77498, _77500, _77502] : [-(_77498 = set_union2(_77502, _77500)), 169 ^ _71842 : [(170 ^ _71842) ^ [] : [-(in(166 ^ [_77498, _77500, _77502], _77498))], (172 ^ _71842) ^ [] : [in(166 ^ [_77498, _77500, _77502], _77502)], (174 ^ _71842) ^ [] : [in(166 ^ [_77498, _77500, _77502], _77500)]], 175 ^ _71842 : [(182 ^ _71842) ^ [] : [in(166 ^ [_77498, _77500, _77502], _77498)], (176 ^ _71842) ^ [] : [-(in(166 ^ [_77498, _77500, _77502], _77502)), -(in(166 ^ [_77498, _77500, _77502], _77500))]]], (143 ^ _71842) ^ [_76773, _76775, _76777] : [_76773 = set_union2(_76777, _76775), 146 ^ _71842 : [(157 ^ _71842) ^ [_77233] : [158 ^ _71842 : [(159 ^ _71842) ^ [] : [in(_77233, _76777)], (161 ^ _71842) ^ [] : [in(_77233, _76775)]], -(in(_77233, _76773))], (147 ^ _71842) ^ [_76955] : [in(_76955, _76773), -(in(_76955, _76777)), -(in(_76955, _76775))]]], (196 ^ _71842) ^ [_78592, _78594] : [198 ^ _71842 : [(199 ^ _71842) ^ [] : [-(in(197 ^ [_78592, _78594], _78594))], (201 ^ _71842) ^ [] : [in(197 ^ [_78592, _78594], _78592)]], -(subset(_78594, _78592))], (186 ^ _71842) ^ [_78278, _78280] : [subset(_78280, _78278), 189 ^ _71842 : [(190 ^ _71842) ^ [_78415] : [in(_78415, _78280), -(in(_78415, _78278))]]], (227 ^ _71842) ^ [_79717, _79719, _79721] : [-(_79717 = set_intersection2(_79721, _79719)), 239 ^ _71842 : [(240 ^ _71842) ^ [] : [-(in(228 ^ [_79717, _79719, _79721], _79721))], (242 ^ _71842) ^ [] : [-(in(228 ^ [_79717, _79719, _79721], _79719))], (244 ^ _71842) ^ [] : [in(228 ^ [_79717, _79719, _79721], _79717)]], 231 ^ _71842 : [(232 ^ _71842) ^ [] : [-(in(228 ^ [_79717, _79719, _79721], _79717))], (234 ^ _71842) ^ [] : [in(228 ^ [_79717, _79719, _79721], _79721), in(228 ^ [_79717, _79719, _79721], _79719)]]], (205 ^ _71842) ^ [_78992, _78994, _78996] : [_78992 = set_intersection2(_78996, _78994), 208 ^ _71842 : [(209 ^ _71842) ^ [_79174] : [in(_79174, _78992), 212 ^ _71842 : [(213 ^ _71842) ^ [] : [-(in(_79174, _78996))], (215 ^ _71842) ^ [] : [-(in(_79174, _78994))]]], (217 ^ _71842) ^ [_79433] : [-(in(_79433, _78992)), in(_79433, _78996), in(_79433, _78994)]]], (270 ^ _71842) ^ [_81244, _81246, _81248] : [-(_81244 = set_difference(_81248, _81246)), 282 ^ _71842 : [(283 ^ _71842) ^ [] : [-(in(271 ^ [_81244, _81246, _81248], _81248))], (285 ^ _71842) ^ [] : [in(271 ^ [_81244, _81246, _81248], _81246)], (287 ^ _71842) ^ [] : [in(271 ^ [_81244, _81246, _81248], _81244)]], 274 ^ _71842 : [(275 ^ _71842) ^ [] : [-(in(271 ^ [_81244, _81246, _81248], _81244))], (277 ^ _71842) ^ [] : [in(271 ^ [_81244, _81246, _81248], _81248), -(in(271 ^ [_81244, _81246, _81248], _81246))]]], (248 ^ _71842) ^ [_80513, _80515, _80517] : [_80513 = set_difference(_80517, _80515), 251 ^ _71842 : [(252 ^ _71842) ^ [_80697] : [in(_80697, _80513), 255 ^ _71842 : [(256 ^ _71842) ^ [] : [-(in(_80697, _80517))], (258 ^ _71842) ^ [] : [in(_80697, _80515)]]], (260 ^ _71842) ^ [_80957] : [-(in(_80957, _80513)), in(_80957, _80517), -(in(_80957, _80515))]]], (291 ^ _71842) ^ [_82030, _82032] : [disjoint(_82032, _82030), -(set_intersection2(_82032, _82030) = empty_set)], (297 ^ _71842) ^ [_82198, _82200] : [set_intersection2(_82200, _82198) = empty_set, -(disjoint(_82200, _82198))], (303 ^ _71842) ^ [] : [true___, -(true___)], (309 ^ _71842) ^ [] : [true___, -(true___)], (315 ^ _71842) ^ [] : [true___, -(true___)], (321 ^ _71842) ^ [] : [true___, -(true___)], (327 ^ _71842) ^ [] : [-(empty(empty_set))], (329 ^ _71842) ^ [_82945, _82947] : [-(empty(_82947)), empty(set_union2(_82947, _82945))], (335 ^ _71842) ^ [_83161, _83163] : [-(empty(_83163)), empty(set_union2(_83161, _83163))], (341 ^ _71842) ^ [_83362, _83364] : [-(set_union2(_83364, _83364) = _83364)], (343 ^ _71842) ^ [_83459, _83461] : [-(set_intersection2(_83461, _83461) = _83461)], (345 ^ _71842) ^ [_83600, _83602] : [set_difference(_83602, _83600) = empty_set, -(subset(_83602, _83600))], (351 ^ _71842) ^ [_83768, _83770] : [subset(_83770, _83768), -(set_difference(_83770, _83768) = empty_set)], (358 ^ _71842) ^ [] : [-(empty(356 ^ []))], (361 ^ _71842) ^ [] : [empty(359 ^ [])], (363 ^ _71842) ^ [_84150, _84152] : [-(subset(_84152, _84152))], (365 ^ _71842) ^ [_84259, _84261] : [disjoint(_84261, _84259), -(disjoint(_84259, _84261))], (371 ^ _71842) ^ [_84469, _84471] : [subset(_84471, _84469), -(set_union2(_84471, _84469) = _84469)], (377 ^ _71842) ^ [_84670, _84672] : [-(subset(set_intersection2(_84672, _84670), _84672))], (379 ^ _71842) ^ [_84796, _84798, _84800] : [-(subset(_84800, set_intersection2(_84798, _84796))), subset(_84800, _84798), subset(_84800, _84796)], (389 ^ _71842) ^ [_85082] : [-(set_union2(_85082, empty_set) = _85082)], (391 ^ _71842) ^ [_85206, _85208, _85210] : [-(subset(_85210, _85206)), subset(_85210, _85208), subset(_85208, _85206)], (401 ^ _71842) ^ [_85529, _85531, _85533] : [subset(_85533, _85531), -(subset(set_intersection2(_85533, _85529), set_intersection2(_85531, _85529)))], (407 ^ _71842) ^ [_85757, _85759] : [subset(_85759, _85757), -(set_intersection2(_85759, _85757) = _85759)], (413 ^ _71842) ^ [_85944] : [-(set_intersection2(_85944, empty_set) = empty_set)], (415 ^ _71842) ^ [_86054, _86056] : [-(_86056 = _86054), 419 ^ _71842 : [(420 ^ _71842) ^ [] : [-(in(416 ^ [_86054, _86056], _86056))], (422 ^ _71842) ^ [] : [in(416 ^ [_86054, _86056], _86054)]], 423 ^ _71842 : [(424 ^ _71842) ^ [] : [-(in(416 ^ [_86054, _86056], _86054))], (426 ^ _71842) ^ [] : [in(416 ^ [_86054, _86056], _86056)]]], (430 ^ _71842) ^ [_86555] : [-(subset(empty_set, _86555))], (432 ^ _71842) ^ [_86676, _86678, _86680] : [subset(_86680, _86678), -(subset(set_difference(_86680, _86676), set_difference(_86678, _86676)))], (438 ^ _71842) ^ [_86889, _86891] : [-(subset(set_difference(_86891, _86889), _86891))], (440 ^ _71842) ^ [_86972] : [-(set_difference(_86972, empty_set) = _86972)], (442 ^ _71842) ^ [_87102, _87104] : [-(disjoint(_87104, _87102)), 446 ^ _71842 : [(447 ^ _71842) ^ [] : [-(in(445 ^ [_87102, _87104], _87104))], (449 ^ _71842) ^ [] : [-(in(445 ^ [_87102, _87104], _87102))]]], (451 ^ _71842) ^ [_87416, _87418] : [disjoint(_87418, _87416), 452 ^ _71842 : [(453 ^ _71842) ^ [_87508] : [in(_87508, _87418), in(_87508, _87416)]]], (461 ^ _71842) ^ [_87765] : [subset(_87765, empty_set), -(_87765 = empty_set)], (467 ^ _71842) ^ [_87940] : [-(set_difference(empty_set, _87940) = empty_set)], (469 ^ _71842) ^ [_88070, _88072] : [-(disjoint(_88072, _88070)), -(in(472 ^ [_88070, _88072], set_intersection2(_88072, _88070)))], (476 ^ _71842) ^ [_88305, _88307] : [477 ^ _71842 : [(478 ^ _71842) ^ [_88378] : [in(_88378, set_intersection2(_88307, _88305))]], disjoint(_88307, _88305)], (482 ^ _71842) ^ [_88530] : [empty(_88530), -(_88530 = empty_set)], (488 ^ _71842) ^ [_88732, _88734] : [in(_88734, _88732), empty(_88732)], (494 ^ _71842) ^ [_88924, _88926] : [-(subset(_88926, set_union2(_88926, _88924)))], (496 ^ _71842) ^ [_89036, _89038] : [empty(_89038), -(_89038 = _89036), empty(_89036)], (506 ^ _71842) ^ [_89327, _89329, _89331] : [-(subset(set_union2(_89331, _89327), _89329)), subset(_89331, _89329), subset(_89327, _89329)]], input).
% 0.26/1.39 ncf('1',plain,[522 : subset(515 ^ [], 516 ^ []), 526 : set_difference(515 ^ [], 516 ^ []) = empty_set],start(518 ^ 0)).
% 0.26/1.39 ncf('1.1',plain,[-(subset(515 ^ [], 516 ^ [])), set_difference(515 ^ [], 516 ^ []) = empty_set],extension(345 ^ 3,bind([[_83600, _83602], [516 ^ [], 515 ^ []]]))).
% 0.26/1.39 ncf('1.1.1',plain,[-(set_difference(515 ^ [], 516 ^ []) = empty_set)],extension(520 ^ 4)).
% 0.26/1.39 ncf('1.2',plain,[-(set_difference(515 ^ [], 516 ^ []) = empty_set), subset(515 ^ [], 516 ^ [])],extension(351 ^ 3,bind([[_83768, _83770], [516 ^ [], 515 ^ []]]))).
% 0.26/1.39 ncf('1.2.1',plain,[-(subset(515 ^ [], 516 ^ []))],extension(524 ^ 4)).
% 0.26/1.39 %-----------------------------------------------------
% 0.26/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------