%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU113+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:14 EDT 2023
% Result : Theorem 0.76s 1.37s
% Output : Proof 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU113+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n023.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:29 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.76/1.37
% 0.76/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.76/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.76/1.37 %-----------------------------------------------------
% 0.76/1.37 ncf(matrix, plain, [(493 ^ _65623) ^ [] : [subset(finite_subsets(491 ^ []), powerset(491 ^ []))], (204 ^ _65623) ^ [_72028, _72030] : [in(_72030, _72028), in(_72028, _72030)], (210 ^ _65623) ^ [_72225] : [empty(_72225), -(finite(_72225))], (216 ^ _65623) ^ [_72411] : [preboolean(_72411), 219 ^ _65623 : [(220 ^ _65623) ^ [] : [-(cup_closed(_72411))], (222 ^ _65623) ^ [] : [-(diff_closed(_72411))]]], (224 ^ _65623) ^ [_72668] : [finite(_72668), 227 ^ _65623 : [(228 ^ _65623) ^ [_72800] : [element(_72800, powerset(_72668)), -(finite(_72800))]]], (234 ^ _65623) ^ [_73005] : [-(preboolean(_73005)), cup_closed(_73005), diff_closed(_73005)], (244 ^ _65623) ^ [_73288, _73290] : [element(_73288, finite_subsets(_73290)), -(finite(_73288))], (260 ^ _65623) ^ [_73843, _73845] : [262 ^ _65623 : [(263 ^ _65623) ^ [] : [-(in(261 ^ [_73843, _73845], _73845))], (265 ^ _65623) ^ [] : [in(261 ^ [_73843, _73845], _73843)]], -(subset(_73845, _73843))], (250 ^ _65623) ^ [_73529, _73531] : [subset(_73531, _73529), 253 ^ _65623 : [(254 ^ _65623) ^ [_73666] : [in(_73666, _73531), -(in(_73666, _73529))]]], (269 ^ _65623) ^ [_74200, _74202] : [preboolean(_74200), 272 ^ _65623 : [(295 ^ _65623) ^ [] : [-(_74200 = finite_subsets(_74202)), 307 ^ _65623 : [(308 ^ _65623) ^ [] : [-(subset(296 ^ [_74200, _74202], _74202))], (310 ^ _65623) ^ [] : [-(finite(296 ^ [_74200, _74202]))], (312 ^ _65623) ^ [] : [in(296 ^ [_74200, _74202], _74200)]], 299 ^ _65623 : [(300 ^ _65623) ^ [] : [-(in(296 ^ [_74200, _74202], _74200))], (302 ^ _65623) ^ [] : [subset(296 ^ [_74200, _74202], _74202), finite(296 ^ [_74200, _74202])]]], (273 ^ _65623) ^ [] : [_74200 = finite_subsets(_74202), 276 ^ _65623 : [(277 ^ _65623) ^ [_74487] : [in(_74487, _74200), 280 ^ _65623 : [(281 ^ _65623) ^ [] : [-(subset(_74487, _74202))], (283 ^ _65623) ^ [] : [-(finite(_74487))]]], (285 ^ _65623) ^ [_74734] : [-(in(_74734, _74200)), subset(_74734, _74202), finite(_74734)]]]]], (316 ^ _65623) ^ [_75640] : [-(preboolean(finite_subsets(_75640)))], (319 ^ _65623) ^ [_75758] : [-(element(317 ^ [_75758], _75758))], (321 ^ _65623) ^ [_75860] : [empty(powerset(_75860))], (323 ^ _65623) ^ [_75925] : [-(cup_closed(powerset(_75925)))], (325 ^ _65623) ^ [_75990] : [-(diff_closed(powerset(_75990)))], (327 ^ _65623) ^ [_76035] : [-(preboolean(powerset(_76035)))], (329 ^ _65623) ^ [_76119] : [empty(powerset(_76119))], (331 ^ _65623) ^ [] : [-(empty(empty_set))], (333 ^ _65623) ^ [_76270] : [empty(finite_subsets(_76270))], (335 ^ _65623) ^ [_76335] : [-(cup_closed(finite_subsets(_76335)))], (337 ^ _65623) ^ [_76400] : [-(diff_closed(finite_subsets(_76400)))], (339 ^ _65623) ^ [_76445] : [-(preboolean(finite_subsets(_76445)))], (342 ^ _65623) ^ [] : [empty(340 ^ [])], (344 ^ _65623) ^ [] : [-(finite(340 ^ []))], (347 ^ _65623) ^ [] : [empty(345 ^ [])], (349 ^ _65623) ^ [] : [-(cup_closed(345 ^ []))], (351 ^ _65623) ^ [] : [-(cap_closed(345 ^ []))], (353 ^ _65623) ^ [] : [-(diff_closed(345 ^ []))], (355 ^ _65623) ^ [] : [-(preboolean(345 ^ []))], (357 ^ _65623) ^ [_77025] : [-(empty(_77025)), 361 ^ _65623 : [(362 ^ _65623) ^ [] : [-(element(360 ^ [_77025], powerset(_77025)))], (364 ^ _65623) ^ [] : [empty(360 ^ [_77025])]]], (367 ^ _65623) ^ [] : [-(empty(365 ^ []))], (370 ^ _65623) ^ [_77537] : [-(element(368 ^ [_77537], powerset(_77537)))], (372 ^ _65623) ^ [_77608] : [-(empty(368 ^ [_77608]))], (374 ^ _65623) ^ [_77676] : [-(relation(368 ^ [_77676]))], (376 ^ _65623) ^ [_77744] : [-(function(368 ^ [_77744]))], (378 ^ _65623) ^ [_77812] : [-(one_to_one(368 ^ [_77812]))], (380 ^ _65623) ^ [_77880] : [-(epsilon_transitive(368 ^ [_77880]))], (382 ^ _65623) ^ [_77948] : [-(epsilon_connected(368 ^ [_77948]))], (384 ^ _65623) ^ [_78016] : [-(ordinal(368 ^ [_78016]))], (386 ^ _65623) ^ [_78084] : [-(natural(368 ^ [_78084]))], (388 ^ _65623) ^ [_78132] : [-(finite(368 ^ [_78132]))], (391 ^ _65623) ^ [_78298] : [-(element(389 ^ [_78298], powerset(_78298)))], (393 ^ _65623) ^ [_78349] : [-(empty(389 ^ [_78349]))], (396 ^ _65623) ^ [] : [empty(394 ^ [])], (398 ^ _65623) ^ [_78538] : [-(empty(_78538)), 402 ^ _65623 : [(403 ^ _65623) ^ [] : [-(element(401 ^ [_78538], powerset(_78538)))], (405 ^ _65623) ^ [] : [empty(401 ^ [_78538])], (407 ^ _65623) ^ [] : [-(finite(401 ^ [_78538]))]]], (409 ^ _65623) ^ [_78950] : [-(empty(_78950)), 413 ^ _65623 : [(414 ^ _65623) ^ [] : [-(element(412 ^ [_78950], powerset(_78950)))], (416 ^ _65623) ^ [] : [empty(412 ^ [_78950])], (418 ^ _65623) ^ [] : [-(finite(412 ^ [_78950]))]]], (420 ^ _65623) ^ [_79361, _79363] : [-(subset(_79363, _79363))], (422 ^ _65623) ^ [_79470, _79472] : [in(_79472, _79470), -(element(_79472, _79470))], (428 ^ _65623) ^ [_79680, _79682] : [element(_79682, _79680), -(empty(_79680)), -(in(_79682, _79680))], (438 ^ _65623) ^ [_80007, _80009] : [element(_80009, powerset(_80007)), -(subset(_80009, _80007))], (444 ^ _65623) ^ [_80173, _80175] : [subset(_80175, _80173), -(element(_80175, powerset(_80173)))], (450 ^ _65623) ^ [_80403, _80405, _80407] : [-(element(_80407, _80403)), in(_80407, _80405), element(_80405, powerset(_80403))], (460 ^ _65623) ^ [_80730, _80732, _80734] : [in(_80734, _80732), element(_80732, powerset(_80730)), empty(_80730)], (470 ^ _65623) ^ [_81026] : [empty(_81026), -(_81026 = empty_set)], (476 ^ _65623) ^ [_81228, _81230] : [in(_81230, _81228), empty(_81228)], (482 ^ _65623) ^ [_81415, _81417] : [empty(_81417), -(_81417 = _81415), empty(_81415)], (192 ^ _65623) ^ [_71574, _71576] : [_71576 = _71574, -(finite_subsets(_71576) = finite_subsets(_71574))], (198 ^ _65623) ^ [_71772, _71774] : [_71774 = _71772, -(powerset(_71774) = powerset(_71772))], (2 ^ _65623) ^ [_65767] : [-(_65767 = _65767)], (4 ^ _65623) ^ [_65874, _65876] : [_65876 = _65874, -(_65874 = _65876)], (10 ^ _65623) ^ [_66078, _66080, _66082] : [-(_66082 = _66078), _66082 = _66080, _66080 = _66078], (20 ^ _65623) ^ [_66391, _66393] : [-(cup_closed(_66391)), _66393 = _66391, cup_closed(_66393)], (30 ^ _65623) ^ [_66686, _66688] : [-(cap_closed(_66686)), _66688 = _66686, cap_closed(_66688)], (40 ^ _65623) ^ [_66981, _66983] : [-(diff_closed(_66981)), _66983 = _66981, diff_closed(_66983)], (50 ^ _65623) ^ [_67276, _67278] : [-(preboolean(_67276)), _67278 = _67276, preboolean(_67278)], (60 ^ _65623) ^ [_67571, _67573] : [-(relation(_67571)), _67573 = _67571, relation(_67573)], (70 ^ _65623) ^ [_67866, _67868] : [-(function(_67866)), _67868 = _67866, function(_67868)], (80 ^ _65623) ^ [_68161, _68163] : [-(one_to_one(_68161)), _68163 = _68161, one_to_one(_68163)], (90 ^ _65623) ^ [_68456, _68458] : [-(epsilon_transitive(_68456)), _68458 = _68456, epsilon_transitive(_68458)], (100 ^ _65623) ^ [_68751, _68753] : [-(epsilon_connected(_68751)), _68753 = _68751, epsilon_connected(_68753)], (110 ^ _65623) ^ [_69046, _69048] : [-(ordinal(_69046)), _69048 = _69046, ordinal(_69048)], (120 ^ _65623) ^ [_69341, _69343] : [-(natural(_69341)), _69343 = _69341, natural(_69343)], (130 ^ _65623) ^ [_69636, _69638] : [-(finite(_69636)), _69638 = _69636, finite(_69638)], (140 ^ _65623) ^ [_69959, _69961, _69963, _69965] : [-(element(_69963, _69959)), element(_69965, _69961), _69965 = _69963, _69961 = _69959], (154 ^ _65623) ^ [_70403, _70405, _70407, _70409] : [-(in(_70407, _70403)), in(_70409, _70405), _70409 = _70407, _70405 = _70403], (168 ^ _65623) ^ [_70819, _70821] : [-(empty(_70819)), _70821 = _70819, empty(_70821)], (178 ^ _65623) ^ [_71122, _71124, _71126, _71128] : [-(subset(_71126, _71122)), subset(_71128, _71124), _71128 = _71126, _71124 = _71122]], input).
% 0.76/1.37 ncf('1',plain,[subset(finite_subsets(491 ^ []), powerset(491 ^ []))],start(493 ^ 0)).
% 0.76/1.37 ncf('1.1',plain,[-(subset(finite_subsets(491 ^ []), powerset(491 ^ []))), 263 : -(in(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], finite_subsets(491 ^ [])))],extension(260 ^ 1,bind([[_73843, _73845], [powerset(491 ^ []), finite_subsets(491 ^ [])]]))).
% 0.76/1.37 ncf('1.1.1',plain,[in(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], finite_subsets(491 ^ [])), 281 : -(subset(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], 491 ^ [])), 277 : finite_subsets(491 ^ []) = finite_subsets(491 ^ []), 273 : preboolean(finite_subsets(491 ^ []))],extension(269 ^ 4,bind([[_74200, _74202, _74487], [finite_subsets(491 ^ []), 491 ^ [], 261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])]]]))).
% 0.76/1.37 ncf('1.1.1.1',plain,[subset(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], 491 ^ []), -(element(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], powerset(491 ^ [])))],extension(444 ^ 11,bind([[_80173, _80175], [491 ^ [], 261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])]]]))).
% 0.76/1.37 ncf('1.1.1.1.1',plain,[element(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], powerset(491 ^ [])), -(empty(powerset(491 ^ []))), -(in(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], powerset(491 ^ [])))],extension(428 ^ 12,bind([[_79680, _79682], [powerset(491 ^ []), 261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])]]]))).
% 0.76/1.37 ncf('1.1.1.1.1.1',plain,[empty(powerset(491 ^ []))],extension(321 ^ 13,bind([[_75860], [491 ^ []]]))).
% 0.76/1.37 ncf('1.1.1.1.1.2',plain,[in(261 ^ [powerset(491 ^ []), finite_subsets(491 ^ [])], powerset(491 ^ []))],extension(265 ^ 13)).
% 0.76/1.37 ncf('1.1.1.2',plain,[-(finite_subsets(491 ^ []) = finite_subsets(491 ^ [])), 491 ^ [] = 491 ^ []],extension(192 ^ 7,bind([[_71574, _71576], [491 ^ [], 491 ^ []]]))).
% 0.76/1.37 ncf('1.1.1.2.1',plain,[-(491 ^ [] = 491 ^ [])],extension(2 ^ 8,bind([[_65767], [491 ^ []]]))).
% 0.76/1.37 ncf('1.1.1.3',plain,[-(preboolean(finite_subsets(491 ^ []))), cup_closed(finite_subsets(491 ^ [])), diff_closed(finite_subsets(491 ^ []))],extension(234 ^ 5,bind([[_73005], [finite_subsets(491 ^ [])]]))).
% 0.76/1.37 ncf('1.1.1.3.1',plain,[-(cup_closed(finite_subsets(491 ^ [])))],extension(335 ^ 6,bind([[_76335], [491 ^ []]]))).
% 0.76/1.37 ncf('1.1.1.3.2',plain,[-(diff_closed(finite_subsets(491 ^ [])))],extension(337 ^ 6,bind([[_76400], [491 ^ []]]))).
% 0.76/1.37 %-----------------------------------------------------
% 0.76/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------