%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU295+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:03:02 EDT 2023
% Result : Theorem 0.31s 1.37s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU295+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n012.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:28:47 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.31/1.37
% 0.31/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.31/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 ncf(matrix, plain, [(599 ^ _79421) ^ [] : [-(finite(596 ^ []))], (601 ^ _79421) ^ [] : [finite(set_intersection2(596 ^ [], 597 ^ []))], (162 ^ _79421) ^ [_84481, _84483] : [_84483 = _84481, -(powerset(_84483) = powerset(_84481))], (168 ^ _79421) ^ [_84707, _84709, _84711, _84713] : [-(set_intersection2(_84713, _84709) = set_intersection2(_84711, _84707)), _84713 = _84711, _84709 = _84707], (2 ^ _79421) ^ [_79565] : [-(_79565 = _79565)], (4 ^ _79421) ^ [_79672, _79674] : [_79674 = _79672, -(_79672 = _79674)], (10 ^ _79421) ^ [_79876, _79878, _79880] : [-(_79880 = _79876), _79880 = _79878, _79878 = _79876], (20 ^ _79421) ^ [_80189, _80191] : [-(natural(_80189)), _80191 = _80189, natural(_80191)], (30 ^ _79421) ^ [_80484, _80486] : [-(one_to_one(_80484)), _80486 = _80484, one_to_one(_80486)], (40 ^ _79421) ^ [_80779, _80781] : [-(epsilon_transitive(_80779)), _80781 = _80779, epsilon_transitive(_80781)], (50 ^ _79421) ^ [_81074, _81076] : [-(epsilon_connected(_81074)), _81076 = _81074, epsilon_connected(_81076)], (60 ^ _79421) ^ [_81369, _81371] : [-(ordinal(_81369)), _81371 = _81369, ordinal(_81371)], (70 ^ _79421) ^ [_81664, _81666] : [-(relation(_81664)), _81666 = _81664, relation(_81666)], (80 ^ _79421) ^ [_81959, _81961] : [-(relation_empty_yielding(_81959)), _81961 = _81959, relation_empty_yielding(_81961)], (90 ^ _79421) ^ [_82254, _82256] : [-(function(_82254)), _82256 = _82254, function(_82256)], (100 ^ _79421) ^ [_82577, _82579, _82581, _82583] : [-(subset(_82581, _82577)), subset(_82583, _82579), _82583 = _82581, _82579 = _82577], (114 ^ _79421) ^ [_83021, _83023, _83025, _83027] : [-(element(_83025, _83021)), element(_83027, _83023), _83027 = _83025, _83023 = _83021], (128 ^ _79421) ^ [_83465, _83467, _83469, _83471] : [-(in(_83469, _83465)), in(_83471, _83467), _83471 = _83469, _83467 = _83465], (142 ^ _79421) ^ [_83881, _83883] : [-(empty(_83881)), _83883 = _83881, empty(_83883)], (152 ^ _79421) ^ [_84156, _84158] : [-(finite(_84156)), _84158 = _84156, finite(_84158)], (178 ^ _79421) ^ [_85044, _85046] : [in(_85046, _85044), in(_85044, _85046)], (184 ^ _79421) ^ [_85241] : [ordinal(_85241), 187 ^ _79421 : [(188 ^ _79421) ^ [_85381] : [element(_85381, _85241), 191 ^ _79421 : [(192 ^ _79421) ^ [] : [-(epsilon_transitive(_85381))], (194 ^ _79421) ^ [] : [-(epsilon_connected(_85381))], (196 ^ _79421) ^ [] : [-(ordinal(_85381))]]]]], (198 ^ _79421) ^ [_85727] : [empty(_85727), -(finite(_85727))], (204 ^ _79421) ^ [_85913] : [empty(_85913), -(function(_85913))], (210 ^ _79421) ^ [_86099] : [ordinal(_86099), 213 ^ _79421 : [(214 ^ _79421) ^ [] : [-(epsilon_transitive(_86099))], (216 ^ _79421) ^ [] : [-(epsilon_connected(_86099))]]], (218 ^ _79421) ^ [_86356] : [empty(_86356), -(relation(_86356))], (224 ^ _79421) ^ [_86542] : [231 ^ _79421 : [(232 ^ _79421) ^ [] : [-(epsilon_transitive(_86542))], (234 ^ _79421) ^ [] : [-(epsilon_connected(_86542))], (236 ^ _79421) ^ [] : [-(ordinal(_86542))], (238 ^ _79421) ^ [] : [-(natural(_86542))]], empty(_86542), ordinal(_86542)], (240 ^ _79421) ^ [_87022] : [finite(_87022), 243 ^ _79421 : [(244 ^ _79421) ^ [_87154] : [element(_87154, powerset(_87022)), -(finite(_87154))]]], (250 ^ _79421) ^ [_87359] : [261 ^ _79421 : [(262 ^ _79421) ^ [] : [-(relation(_87359))], (264 ^ _79421) ^ [] : [-(function(_87359))], (266 ^ _79421) ^ [] : [-(one_to_one(_87359))]], relation(_87359), empty(_87359), function(_87359)], (268 ^ _79421) ^ [_87852] : [-(ordinal(_87852)), epsilon_transitive(_87852), epsilon_connected(_87852)], (278 ^ _79421) ^ [_88121] : [empty(_88121), 281 ^ _79421 : [(282 ^ _79421) ^ [] : [-(epsilon_transitive(_88121))], (284 ^ _79421) ^ [] : [-(epsilon_connected(_88121))], (286 ^ _79421) ^ [] : [-(ordinal(_88121))]]], (288 ^ _79421) ^ [_88447, _88449] : [-(set_intersection2(_88449, _88447) = set_intersection2(_88447, _88449))], (290 ^ _79421) ^ [] : [true___, -(true___)], (296 ^ _79421) ^ [] : [true___, -(true___)], (302 ^ _79421) ^ [] : [true___, -(true___)], (308 ^ _79421) ^ [] : [true___, -(true___)], (315 ^ _79421) ^ [_89048] : [-(element(313 ^ [_89048], _89048))], (317 ^ _79421) ^ [_89160, _89162] : [finite(_89160), -(finite(set_intersection2(_89162, _89160)))], (323 ^ _79421) ^ [_89372, _89374] : [finite(_89374), -(finite(set_intersection2(_89374, _89372)))], (329 ^ _79421) ^ [] : [-(empty(empty_set))], (331 ^ _79421) ^ [] : [-(relation(empty_set))], (333 ^ _79421) ^ [] : [-(relation_empty_yielding(empty_set))], (335 ^ _79421) ^ [_89747, _89749] : [-(relation(set_intersection2(_89749, _89747))), relation(_89749), relation(_89747)], (345 ^ _79421) ^ [_90016] : [empty(powerset(_90016))], (347 ^ _79421) ^ [] : [-(empty(empty_set))], (349 ^ _79421) ^ [] : [-(relation(empty_set))], (351 ^ _79421) ^ [] : [-(relation_empty_yielding(empty_set))], (353 ^ _79421) ^ [] : [-(function(empty_set))], (355 ^ _79421) ^ [] : [-(one_to_one(empty_set))], (357 ^ _79421) ^ [] : [-(empty(empty_set))], (359 ^ _79421) ^ [] : [-(epsilon_transitive(empty_set))], (361 ^ _79421) ^ [] : [-(epsilon_connected(empty_set))], (363 ^ _79421) ^ [] : [-(ordinal(empty_set))], (365 ^ _79421) ^ [] : [-(empty(empty_set))], (367 ^ _79421) ^ [] : [-(relation(empty_set))], (369 ^ _79421) ^ [_90708, _90710] : [-(set_intersection2(_90710, _90710) = _90710)], (372 ^ _79421) ^ [] : [empty(370 ^ [])], (374 ^ _79421) ^ [] : [-(epsilon_transitive(370 ^ []))], (376 ^ _79421) ^ [] : [-(epsilon_connected(370 ^ []))], (378 ^ _79421) ^ [] : [-(ordinal(370 ^ []))], (380 ^ _79421) ^ [] : [-(natural(370 ^ []))], (383 ^ _79421) ^ [] : [empty(381 ^ [])], (385 ^ _79421) ^ [] : [-(finite(381 ^ []))], (388 ^ _79421) ^ [] : [-(relation(386 ^ []))], (390 ^ _79421) ^ [] : [-(function(386 ^ []))], (393 ^ _79421) ^ [] : [-(epsilon_transitive(391 ^ []))], (395 ^ _79421) ^ [] : [-(epsilon_connected(391 ^ []))], (397 ^ _79421) ^ [] : [-(ordinal(391 ^ []))], (400 ^ _79421) ^ [] : [-(empty(398 ^ []))], (402 ^ _79421) ^ [] : [-(relation(398 ^ []))], (404 ^ _79421) ^ [_91793] : [-(empty(_91793)), 408 ^ _79421 : [(409 ^ _79421) ^ [] : [-(element(407 ^ [_91793], powerset(_91793)))], (411 ^ _79421) ^ [] : [empty(407 ^ [_91793])]]], (414 ^ _79421) ^ [] : [-(empty(412 ^ []))], (417 ^ _79421) ^ [_92305] : [-(element(415 ^ [_92305], powerset(_92305)))], (419 ^ _79421) ^ [_92376] : [-(empty(415 ^ [_92376]))], (421 ^ _79421) ^ [_92444] : [-(relation(415 ^ [_92444]))], (423 ^ _79421) ^ [_92512] : [-(function(415 ^ [_92512]))], (425 ^ _79421) ^ [_92580] : [-(one_to_one(415 ^ [_92580]))], (427 ^ _79421) ^ [_92648] : [-(epsilon_transitive(415 ^ [_92648]))], (429 ^ _79421) ^ [_92716] : [-(epsilon_connected(415 ^ [_92716]))], (431 ^ _79421) ^ [_92784] : [-(ordinal(415 ^ [_92784]))], (433 ^ _79421) ^ [_92852] : [-(natural(415 ^ [_92852]))], (435 ^ _79421) ^ [_92900] : [-(finite(415 ^ [_92900]))], (438 ^ _79421) ^ [] : [-(relation(436 ^ []))], (440 ^ _79421) ^ [] : [-(empty(436 ^ []))], (442 ^ _79421) ^ [] : [-(function(436 ^ []))], (445 ^ _79421) ^ [] : [-(relation(443 ^ []))], (447 ^ _79421) ^ [] : [-(function(443 ^ []))], (449 ^ _79421) ^ [] : [-(one_to_one(443 ^ []))], (451 ^ _79421) ^ [] : [-(empty(443 ^ []))], (453 ^ _79421) ^ [] : [-(epsilon_transitive(443 ^ []))], (455 ^ _79421) ^ [] : [-(epsilon_connected(443 ^ []))], (457 ^ _79421) ^ [] : [-(ordinal(443 ^ []))], (460 ^ _79421) ^ [] : [empty(458 ^ [])], (462 ^ _79421) ^ [] : [-(relation(458 ^ []))], (465 ^ _79421) ^ [_93874] : [-(element(463 ^ [_93874], powerset(_93874)))], (467 ^ _79421) ^ [_93925] : [-(empty(463 ^ [_93925]))], (470 ^ _79421) ^ [] : [empty(468 ^ [])], (472 ^ _79421) ^ [_94114] : [-(empty(_94114)), 476 ^ _79421 : [(477 ^ _79421) ^ [] : [-(element(475 ^ [_94114], powerset(_94114)))], (479 ^ _79421) ^ [] : [empty(475 ^ [_94114])], (481 ^ _79421) ^ [] : [-(finite(475 ^ [_94114]))]]], (484 ^ _79421) ^ [] : [-(relation(482 ^ []))], (486 ^ _79421) ^ [] : [-(function(482 ^ []))], (488 ^ _79421) ^ [] : [-(one_to_one(482 ^ []))], (491 ^ _79421) ^ [] : [empty(489 ^ [])], (493 ^ _79421) ^ [] : [-(epsilon_transitive(489 ^ []))], (495 ^ _79421) ^ [] : [-(epsilon_connected(489 ^ []))], (497 ^ _79421) ^ [] : [-(ordinal(489 ^ []))], (500 ^ _79421) ^ [] : [-(relation(498 ^ []))], (502 ^ _79421) ^ [] : [-(relation_empty_yielding(498 ^ []))], (505 ^ _79421) ^ [] : [-(relation(503 ^ []))], (507 ^ _79421) ^ [] : [-(relation_empty_yielding(503 ^ []))], (509 ^ _79421) ^ [] : [-(function(503 ^ []))], (511 ^ _79421) ^ [_95362, _95364] : [-(subset(_95364, _95364))], (513 ^ _79421) ^ [_95471, _95473] : [-(finite(_95473)), subset(_95473, _95471), finite(_95471)], (523 ^ _79421) ^ [_95751, _95753] : [-(subset(set_intersection2(_95753, _95751), _95753))], (525 ^ _79421) ^ [_95863, _95865] : [in(_95865, _95863), -(element(_95865, _95863))], (531 ^ _79421) ^ [_96044] : [-(set_intersection2(_96044, empty_set) = empty_set)], (533 ^ _79421) ^ [_96154, _96156] : [element(_96156, _96154), -(empty(_96154)), -(in(_96156, _96154))], (543 ^ _79421) ^ [_96481, _96483] : [element(_96483, powerset(_96481)), -(subset(_96483, _96481))], (549 ^ _79421) ^ [_96647, _96649] : [subset(_96649, _96647), -(element(_96649, powerset(_96647)))], (555 ^ _79421) ^ [_96877, _96879, _96881] : [-(element(_96881, _96877)), in(_96881, _96879), element(_96879, powerset(_96877))], (565 ^ _79421) ^ [_97204, _97206, _97208] : [in(_97208, _97206), element(_97206, powerset(_97204)), empty(_97204)], (575 ^ _79421) ^ [_97500] : [empty(_97500), -(_97500 = empty_set)], (581 ^ _79421) ^ [_97702, _97704] : [in(_97704, _97702), empty(_97702)], (587 ^ _79421) ^ [_97889, _97891] : [empty(_97891), -(_97891 = _97889), empty(_97889)]], input).
% 0.31/1.37 ncf('1',plain,[finite(set_intersection2(596 ^ [], 597 ^ []))],start(601 ^ 0)).
% 0.31/1.37 ncf('1.1',plain,[-(finite(set_intersection2(596 ^ [], 597 ^ []))), finite(596 ^ [])],extension(323 ^ 1,bind([[_89372, _89374], [597 ^ [], 596 ^ []]]))).
% 0.31/1.37 ncf('1.1.1',plain,[-(finite(596 ^ []))],extension(599 ^ 2)).
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------