%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU133+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:18 EDT 2023
% Result : Theorem 0.41s 1.38s
% Output : Proof 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU133+2 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n022.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:17:02 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.41/1.38
% 0.41/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.41/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.38 %-----------------------------------------------------
% 0.41/1.38 ncf(matrix, plain, [(516 ^ _70547) ^ [] : [subset(set_difference(513 ^ [], 514 ^ []), 513 ^ [])], (72 ^ _70547) ^ [_72962, _72964, _72966, _72968] : [-(set_intersection2(_72968, _72964) = set_intersection2(_72966, _72962)), _72968 = _72966, _72964 = _72962], (82 ^ _70547) ^ [_73321, _73323, _73325, _73327] : [-(set_union2(_73327, _73323) = set_union2(_73325, _73321)), _73327 = _73325, _73323 = _73321], (92 ^ _70547) ^ [_73660, _73662, _73664, _73666] : [-(set_difference(_73666, _73662) = set_difference(_73664, _73660)), _73666 = _73664, _73662 = _73660], (2 ^ _70547) ^ [_70691] : [-(_70691 = _70691)], (4 ^ _70547) ^ [_70798, _70800] : [_70800 = _70798, -(_70798 = _70800)], (10 ^ _70547) ^ [_71002, _71004, _71006] : [-(_71006 = _71002), _71006 = _71004, _71004 = _71002], (20 ^ _70547) ^ [_71343, _71345, _71347, _71349] : [-(disjoint(_71347, _71343)), disjoint(_71349, _71345), _71349 = _71347, _71345 = _71343], (34 ^ _70547) ^ [_71787, _71789, _71791, _71793] : [-(in(_71791, _71787)), in(_71793, _71789), _71793 = _71791, _71789 = _71787], (48 ^ _70547) ^ [_72203, _72205] : [-(empty(_72203)), _72205 = _72203, empty(_72205)], (58 ^ _70547) ^ [_72506, _72508, _72510, _72512] : [-(subset(_72510, _72506)), subset(_72512, _72508), _72512 = _72510, _72508 = _72506], (102 ^ _70547) ^ [_74001, _74003] : [in(_74003, _74001), in(_74001, _74003)], (108 ^ _70547) ^ [_74197, _74199] : [-(set_union2(_74199, _74197) = set_union2(_74197, _74199))], (110 ^ _70547) ^ [_74297, _74299] : [-(set_intersection2(_74299, _74297) = set_intersection2(_74297, _74299))], (112 ^ _70547) ^ [_74441, _74443] : [_74443 = _74441, 115 ^ _70547 : [(116 ^ _70547) ^ [] : [-(subset(_74443, _74441))], (118 ^ _70547) ^ [] : [-(subset(_74441, _74443))]]], (120 ^ _70547) ^ [_74678, _74680] : [-(_74680 = _74678), subset(_74680, _74678), subset(_74678, _74680)], (130 ^ _70547) ^ [_74994] : [_74994 = empty_set, 133 ^ _70547 : [(134 ^ _70547) ^ [_75107] : [in(_75107, _74994)]]], (136 ^ _70547) ^ [_75173] : [-(in(137 ^ [_75173], _75173)), -(_75173 = empty_set)], (165 ^ _70547) ^ [_76203, _76205, _76207] : [-(_76203 = set_union2(_76207, _76205)), 169 ^ _70547 : [(170 ^ _70547) ^ [] : [-(in(166 ^ [_76203, _76205, _76207], _76203))], (172 ^ _70547) ^ [] : [in(166 ^ [_76203, _76205, _76207], _76207)], (174 ^ _70547) ^ [] : [in(166 ^ [_76203, _76205, _76207], _76205)]], 175 ^ _70547 : [(182 ^ _70547) ^ [] : [in(166 ^ [_76203, _76205, _76207], _76203)], (176 ^ _70547) ^ [] : [-(in(166 ^ [_76203, _76205, _76207], _76207)), -(in(166 ^ [_76203, _76205, _76207], _76205))]]], (143 ^ _70547) ^ [_75478, _75480, _75482] : [_75478 = set_union2(_75482, _75480), 146 ^ _70547 : [(157 ^ _70547) ^ [_75938] : [158 ^ _70547 : [(159 ^ _70547) ^ [] : [in(_75938, _75482)], (161 ^ _70547) ^ [] : [in(_75938, _75480)]], -(in(_75938, _75478))], (147 ^ _70547) ^ [_75660] : [in(_75660, _75478), -(in(_75660, _75482)), -(in(_75660, _75480))]]], (196 ^ _70547) ^ [_77297, _77299] : [198 ^ _70547 : [(199 ^ _70547) ^ [] : [-(in(197 ^ [_77297, _77299], _77299))], (201 ^ _70547) ^ [] : [in(197 ^ [_77297, _77299], _77297)]], -(subset(_77299, _77297))], (186 ^ _70547) ^ [_76983, _76985] : [subset(_76985, _76983), 189 ^ _70547 : [(190 ^ _70547) ^ [_77120] : [in(_77120, _76985), -(in(_77120, _76983))]]], (227 ^ _70547) ^ [_78422, _78424, _78426] : [-(_78422 = set_intersection2(_78426, _78424)), 239 ^ _70547 : [(240 ^ _70547) ^ [] : [-(in(228 ^ [_78422, _78424, _78426], _78426))], (242 ^ _70547) ^ [] : [-(in(228 ^ [_78422, _78424, _78426], _78424))], (244 ^ _70547) ^ [] : [in(228 ^ [_78422, _78424, _78426], _78422)]], 231 ^ _70547 : [(232 ^ _70547) ^ [] : [-(in(228 ^ [_78422, _78424, _78426], _78422))], (234 ^ _70547) ^ [] : [in(228 ^ [_78422, _78424, _78426], _78426), in(228 ^ [_78422, _78424, _78426], _78424)]]], (205 ^ _70547) ^ [_77697, _77699, _77701] : [_77697 = set_intersection2(_77701, _77699), 208 ^ _70547 : [(209 ^ _70547) ^ [_77879] : [in(_77879, _77697), 212 ^ _70547 : [(213 ^ _70547) ^ [] : [-(in(_77879, _77701))], (215 ^ _70547) ^ [] : [-(in(_77879, _77699))]]], (217 ^ _70547) ^ [_78138] : [-(in(_78138, _77697)), in(_78138, _77701), in(_78138, _77699)]]], (270 ^ _70547) ^ [_79949, _79951, _79953] : [-(_79949 = set_difference(_79953, _79951)), 282 ^ _70547 : [(283 ^ _70547) ^ [] : [-(in(271 ^ [_79949, _79951, _79953], _79953))], (285 ^ _70547) ^ [] : [in(271 ^ [_79949, _79951, _79953], _79951)], (287 ^ _70547) ^ [] : [in(271 ^ [_79949, _79951, _79953], _79949)]], 274 ^ _70547 : [(275 ^ _70547) ^ [] : [-(in(271 ^ [_79949, _79951, _79953], _79949))], (277 ^ _70547) ^ [] : [in(271 ^ [_79949, _79951, _79953], _79953), -(in(271 ^ [_79949, _79951, _79953], _79951))]]], (248 ^ _70547) ^ [_79218, _79220, _79222] : [_79218 = set_difference(_79222, _79220), 251 ^ _70547 : [(252 ^ _70547) ^ [_79402] : [in(_79402, _79218), 255 ^ _70547 : [(256 ^ _70547) ^ [] : [-(in(_79402, _79222))], (258 ^ _70547) ^ [] : [in(_79402, _79220)]]], (260 ^ _70547) ^ [_79662] : [-(in(_79662, _79218)), in(_79662, _79222), -(in(_79662, _79220))]]], (291 ^ _70547) ^ [_80735, _80737] : [disjoint(_80737, _80735), -(set_intersection2(_80737, _80735) = empty_set)], (297 ^ _70547) ^ [_80903, _80905] : [set_intersection2(_80905, _80903) = empty_set, -(disjoint(_80905, _80903))], (303 ^ _70547) ^ [] : [true___, -(true___)], (309 ^ _70547) ^ [] : [true___, -(true___)], (315 ^ _70547) ^ [] : [true___, -(true___)], (321 ^ _70547) ^ [] : [true___, -(true___)], (327 ^ _70547) ^ [] : [-(empty(empty_set))], (329 ^ _70547) ^ [_81650, _81652] : [-(empty(_81652)), empty(set_union2(_81652, _81650))], (335 ^ _70547) ^ [_81866, _81868] : [-(empty(_81868)), empty(set_union2(_81866, _81868))], (341 ^ _70547) ^ [_82067, _82069] : [-(set_union2(_82069, _82069) = _82069)], (343 ^ _70547) ^ [_82164, _82166] : [-(set_intersection2(_82166, _82166) = _82166)], (345 ^ _70547) ^ [_82305, _82307] : [set_difference(_82307, _82305) = empty_set, -(subset(_82307, _82305))], (351 ^ _70547) ^ [_82473, _82475] : [subset(_82475, _82473), -(set_difference(_82475, _82473) = empty_set)], (358 ^ _70547) ^ [] : [-(empty(356 ^ []))], (361 ^ _70547) ^ [] : [empty(359 ^ [])], (363 ^ _70547) ^ [_82855, _82857] : [-(subset(_82857, _82857))], (365 ^ _70547) ^ [_82964, _82966] : [disjoint(_82966, _82964), -(disjoint(_82964, _82966))], (371 ^ _70547) ^ [_83174, _83176] : [subset(_83176, _83174), -(set_union2(_83176, _83174) = _83174)], (377 ^ _70547) ^ [_83375, _83377] : [-(subset(set_intersection2(_83377, _83375), _83377))], (379 ^ _70547) ^ [_83501, _83503, _83505] : [-(subset(_83505, set_intersection2(_83503, _83501))), subset(_83505, _83503), subset(_83505, _83501)], (389 ^ _70547) ^ [_83787] : [-(set_union2(_83787, empty_set) = _83787)], (391 ^ _70547) ^ [_83911, _83913, _83915] : [-(subset(_83915, _83911)), subset(_83915, _83913), subset(_83913, _83911)], (401 ^ _70547) ^ [_84234, _84236, _84238] : [subset(_84238, _84236), -(subset(set_intersection2(_84238, _84234), set_intersection2(_84236, _84234)))], (407 ^ _70547) ^ [_84462, _84464] : [subset(_84464, _84462), -(set_intersection2(_84464, _84462) = _84464)], (413 ^ _70547) ^ [_84649] : [-(set_intersection2(_84649, empty_set) = empty_set)], (415 ^ _70547) ^ [_84759, _84761] : [-(_84761 = _84759), 419 ^ _70547 : [(420 ^ _70547) ^ [] : [-(in(416 ^ [_84759, _84761], _84761))], (422 ^ _70547) ^ [] : [in(416 ^ [_84759, _84761], _84759)]], 423 ^ _70547 : [(424 ^ _70547) ^ [] : [-(in(416 ^ [_84759, _84761], _84759))], (426 ^ _70547) ^ [] : [in(416 ^ [_84759, _84761], _84761)]]], (430 ^ _70547) ^ [_85260] : [-(subset(empty_set, _85260))], (432 ^ _70547) ^ [_85381, _85383, _85385] : [subset(_85385, _85383), -(subset(set_difference(_85385, _85381), set_difference(_85383, _85381)))], (438 ^ _70547) ^ [_85580] : [-(set_difference(_85580, empty_set) = _85580)], (440 ^ _70547) ^ [_85710, _85712] : [-(disjoint(_85712, _85710)), 444 ^ _70547 : [(445 ^ _70547) ^ [] : [-(in(443 ^ [_85710, _85712], _85712))], (447 ^ _70547) ^ [] : [-(in(443 ^ [_85710, _85712], _85710))]]], (449 ^ _70547) ^ [_86024, _86026] : [disjoint(_86026, _86024), 450 ^ _70547 : [(451 ^ _70547) ^ [_86116] : [in(_86116, _86026), in(_86116, _86024)]]], (459 ^ _70547) ^ [_86373] : [subset(_86373, empty_set), -(_86373 = empty_set)], (465 ^ _70547) ^ [_86548] : [-(set_difference(empty_set, _86548) = empty_set)], (467 ^ _70547) ^ [_86678, _86680] : [-(disjoint(_86680, _86678)), -(in(470 ^ [_86678, _86680], set_intersection2(_86680, _86678)))], (474 ^ _70547) ^ [_86913, _86915] : [475 ^ _70547 : [(476 ^ _70547) ^ [_86986] : [in(_86986, set_intersection2(_86915, _86913))]], disjoint(_86915, _86913)], (480 ^ _70547) ^ [_87138] : [empty(_87138), -(_87138 = empty_set)], (486 ^ _70547) ^ [_87340, _87342] : [in(_87342, _87340), empty(_87340)], (492 ^ _70547) ^ [_87532, _87534] : [-(subset(_87534, set_union2(_87534, _87532)))], (494 ^ _70547) ^ [_87644, _87646] : [empty(_87646), -(_87646 = _87644), empty(_87644)], (504 ^ _70547) ^ [_87935, _87937, _87939] : [-(subset(set_union2(_87939, _87935), _87937)), subset(_87939, _87937), subset(_87935, _87937)]], input).
% 0.41/1.38 ncf('1',plain,[subset(set_difference(513 ^ [], 514 ^ []), 513 ^ [])],start(516 ^ 0)).
% 0.41/1.38 ncf('1.1',plain,[-(subset(set_difference(513 ^ [], 514 ^ []), 513 ^ [])), 201 : in(197 ^ [513 ^ [], set_difference(513 ^ [], 514 ^ [])], 513 ^ [])],extension(196 ^ 1,bind([[_77297, _77299], [513 ^ [], set_difference(513 ^ [], 514 ^ [])]]))).
% 0.41/1.38 ncf('1.1.1',plain,[-(in(197 ^ [513 ^ [], set_difference(513 ^ [], 514 ^ [])], 513 ^ [])), 252 : in(197 ^ [513 ^ [], set_difference(513 ^ [], 514 ^ [])], set_difference(513 ^ [], 514 ^ [])), 252 : set_difference(513 ^ [], 514 ^ []) = set_difference(513 ^ [], 514 ^ [])],extension(248 ^ 4,bind([[_79218, _79220, _79222, _79402], [set_difference(513 ^ [], 514 ^ []), 514 ^ [], 513 ^ [], 197 ^ [513 ^ [], set_difference(513 ^ [], 514 ^ [])]]]))).
% 0.41/1.38 ncf('1.1.1.1',plain,[-(in(197 ^ [513 ^ [], set_difference(513 ^ [], 514 ^ [])], set_difference(513 ^ [], 514 ^ [])))],extension(199 ^ 7)).
% 0.41/1.38 ncf('1.1.1.2',plain,[-(set_difference(513 ^ [], 514 ^ []) = set_difference(513 ^ [], 514 ^ []))],extension(2 ^ 5,bind([[_70691], [set_difference(513 ^ [], 514 ^ [])]]))).
% 0.41/1.38 %-----------------------------------------------------
% 0.41/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------