%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM411+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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 11:44:32 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM411+1 : TPTP v8.1.2. Released v3.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n005.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 16:34:38 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(538 ^ _71094) ^ [] : [-(subset(535 ^ [], 536 ^ []))], (541 ^ _71094) ^ [] : [-(transfinite_sequence_of(539 ^ [], 535 ^ []))], (543 ^ _71094) ^ [] : [transfinite_sequence_of(539 ^ [], 536 ^ [])], (198 ^ _71094) ^ [_77319, _77321] : [in(_77321, _77319), in(_77319, _77321)], (204 ^ _71094) ^ [_77516] : [empty(_77516), -(function(_77516))], (210 ^ _71094) ^ [_77702] : [ordinal(_77702), 213 ^ _71094 : [(214 ^ _71094) ^ [] : [-(epsilon_transitive(_77702))], (216 ^ _71094) ^ [] : [-(epsilon_connected(_77702))]]], (218 ^ _71094) ^ [_77959] : [empty(_77959), -(relation(_77959))], (224 ^ _71094) ^ [_78145] : [235 ^ _71094 : [(236 ^ _71094) ^ [] : [-(relation(_78145))], (238 ^ _71094) ^ [] : [-(function(_78145))], (240 ^ _71094) ^ [] : [-(one_to_one(_78145))]], relation(_78145), empty(_78145), function(_78145)], (242 ^ _71094) ^ [_78638] : [-(ordinal(_78638)), epsilon_transitive(_78638), epsilon_connected(_78638)], (252 ^ _71094) ^ [_78907] : [empty(_78907), 255 ^ _71094 : [(256 ^ _71094) ^ [] : [-(epsilon_transitive(_78907))], (258 ^ _71094) ^ [] : [-(epsilon_connected(_78907))], (260 ^ _71094) ^ [] : [-(ordinal(_78907))]]], (262 ^ _71094) ^ [_79248, _79250] : [relation(_79248), function(_79248), transfinite_sequence(_79248), 273 ^ _71094 : [(274 ^ _71094) ^ [] : [transfinite_sequence_of(_79248, _79250), -(subset(relation_rng(_79248), _79250))], (280 ^ _71094) ^ [] : [subset(relation_rng(_79248), _79250), -(transfinite_sequence_of(_79248, _79250))]]], (286 ^ _71094) ^ [_79890, _79892] : [transfinite_sequence_of(_79890, _79892), 289 ^ _71094 : [(290 ^ _71094) ^ [] : [-(relation(_79890))], (292 ^ _71094) ^ [] : [-(function(_79890))], (294 ^ _71094) ^ [] : [-(transfinite_sequence(_79890))]]], (297 ^ _71094) ^ [_80253] : [-(transfinite_sequence_of(295 ^ [_80253], _80253))], (300 ^ _71094) ^ [_80375] : [-(element(298 ^ [_80375], _80375))], (302 ^ _71094) ^ [] : [-(empty(empty_set))], (304 ^ _71094) ^ [] : [-(relation(empty_set))], (306 ^ _71094) ^ [] : [-(relation_empty_yielding(empty_set))], (308 ^ _71094) ^ [] : [-(empty(empty_set))], (310 ^ _71094) ^ [] : [-(relation(empty_set))], (312 ^ _71094) ^ [] : [-(relation_empty_yielding(empty_set))], (314 ^ _71094) ^ [] : [-(function(empty_set))], (316 ^ _71094) ^ [] : [-(one_to_one(empty_set))], (318 ^ _71094) ^ [] : [-(empty(empty_set))], (320 ^ _71094) ^ [] : [-(epsilon_transitive(empty_set))], (322 ^ _71094) ^ [] : [-(epsilon_connected(empty_set))], (324 ^ _71094) ^ [] : [-(ordinal(empty_set))], (326 ^ _71094) ^ [] : [-(empty(empty_set))], (328 ^ _71094) ^ [] : [-(relation(empty_set))], (330 ^ _71094) ^ [_81235] : [-(with_non_empty_elements(relation_rng(_81235))), relation(_81235), relation_non_empty(_81235), function(_81235)], (344 ^ _71094) ^ [_81591] : [empty(relation_rng(_81591)), -(empty(_81591)), relation(_81591)], (354 ^ _71094) ^ [_81868] : [empty(_81868), 357 ^ _71094 : [(358 ^ _71094) ^ [] : [-(empty(relation_rng(_81868)))], (360 ^ _71094) ^ [] : [-(relation(relation_rng(_81868)))]]], (363 ^ _71094) ^ [] : [-(relation(361 ^ []))], (365 ^ _71094) ^ [] : [-(function(361 ^ []))], (368 ^ _71094) ^ [] : [-(epsilon_transitive(366 ^ []))], (370 ^ _71094) ^ [] : [-(epsilon_connected(366 ^ []))], (372 ^ _71094) ^ [] : [-(ordinal(366 ^ []))], (375 ^ _71094) ^ [] : [-(empty(373 ^ []))], (377 ^ _71094) ^ [] : [-(relation(373 ^ []))], (380 ^ _71094) ^ [] : [-(empty(378 ^ []))], (383 ^ _71094) ^ [] : [-(relation(381 ^ []))], (385 ^ _71094) ^ [] : [-(empty(381 ^ []))], (387 ^ _71094) ^ [] : [-(function(381 ^ []))], (390 ^ _71094) ^ [] : [-(relation(388 ^ []))], (392 ^ _71094) ^ [] : [-(function(388 ^ []))], (394 ^ _71094) ^ [] : [-(one_to_one(388 ^ []))], (396 ^ _71094) ^ [] : [-(empty(388 ^ []))], (398 ^ _71094) ^ [] : [-(epsilon_transitive(388 ^ []))], (400 ^ _71094) ^ [] : [-(epsilon_connected(388 ^ []))], (402 ^ _71094) ^ [] : [-(ordinal(388 ^ []))], (405 ^ _71094) ^ [] : [empty(403 ^ [])], (407 ^ _71094) ^ [] : [-(relation(403 ^ []))], (410 ^ _71094) ^ [] : [empty(408 ^ [])], (413 ^ _71094) ^ [] : [-(relation(411 ^ []))], (415 ^ _71094) ^ [] : [-(function(411 ^ []))], (417 ^ _71094) ^ [] : [-(one_to_one(411 ^ []))], (420 ^ _71094) ^ [] : [empty(418 ^ [])], (422 ^ _71094) ^ [] : [-(epsilon_transitive(418 ^ []))], (424 ^ _71094) ^ [] : [-(epsilon_connected(418 ^ []))], (426 ^ _71094) ^ [] : [-(ordinal(418 ^ []))], (429 ^ _71094) ^ [] : [-(relation(427 ^ []))], (431 ^ _71094) ^ [] : [-(relation_empty_yielding(427 ^ []))], (434 ^ _71094) ^ [] : [-(relation(432 ^ []))], (436 ^ _71094) ^ [] : [-(relation_empty_yielding(432 ^ []))], (438 ^ _71094) ^ [] : [-(function(432 ^ []))], (441 ^ _71094) ^ [] : [-(relation(439 ^ []))], (443 ^ _71094) ^ [] : [-(function(439 ^ []))], (445 ^ _71094) ^ [] : [-(transfinite_sequence(439 ^ []))], (448 ^ _71094) ^ [] : [-(relation(446 ^ []))], (450 ^ _71094) ^ [] : [-(relation_non_empty(446 ^ []))], (452 ^ _71094) ^ [] : [-(function(446 ^ []))], (454 ^ _71094) ^ [_84881, _84883] : [-(subset(_84883, _84883))], (456 ^ _71094) ^ [_84990, _84992] : [in(_84992, _84990), -(element(_84992, _84990))], (462 ^ _71094) ^ [_85214, _85216, _85218] : [-(subset(_85218, _85214)), subset(_85218, _85216), subset(_85216, _85214)], (472 ^ _71094) ^ [_85523, _85525] : [element(_85525, _85523), -(empty(_85523)), -(in(_85525, _85523))], (482 ^ _71094) ^ [_85850, _85852] : [element(_85852, powerset(_85850)), -(subset(_85852, _85850))], (488 ^ _71094) ^ [_86016, _86018] : [subset(_86018, _86016), -(element(_86018, powerset(_86016)))], (494 ^ _71094) ^ [_86246, _86248, _86250] : [-(element(_86250, _86246)), in(_86250, _86248), element(_86248, powerset(_86246))], (504 ^ _71094) ^ [_86573, _86575, _86577] : [in(_86577, _86575), element(_86575, powerset(_86573)), empty(_86573)], (514 ^ _71094) ^ [_86869] : [empty(_86869), -(_86869 = empty_set)], (520 ^ _71094) ^ [_87071, _87073] : [in(_87073, _87071), empty(_87071)], (526 ^ _71094) ^ [_87258, _87260] : [empty(_87260), -(_87260 = _87258), empty(_87258)], (186 ^ _71094) ^ [_76897, _76899] : [_76899 = _76897, -(relation_rng(_76899) = relation_rng(_76897))], (192 ^ _71094) ^ [_77095, _77097] : [_77097 = _77095, -(powerset(_77097) = powerset(_77095))], (2 ^ _71094) ^ [_71238] : [-(_71238 = _71238)], (4 ^ _71094) ^ [_71345, _71347] : [_71347 = _71345, -(_71345 = _71347)], (10 ^ _71094) ^ [_71549, _71551, _71553] : [-(_71553 = _71549), _71553 = _71551, _71551 = _71549], (20 ^ _71094) ^ [_71862, _71864] : [-(with_non_empty_elements(_71862)), _71864 = _71862, with_non_empty_elements(_71864)], (30 ^ _71094) ^ [_72157, _72159] : [-(one_to_one(_72157)), _72159 = _72157, one_to_one(_72159)], (40 ^ _71094) ^ [_72452, _72454] : [-(epsilon_transitive(_72452)), _72454 = _72452, epsilon_transitive(_72454)], (50 ^ _71094) ^ [_72747, _72749] : [-(epsilon_connected(_72747)), _72749 = _72747, epsilon_connected(_72749)], (60 ^ _71094) ^ [_73042, _73044] : [-(ordinal(_73042)), _73044 = _73042, ordinal(_73044)], (70 ^ _71094) ^ [_73337, _73339] : [-(relation_empty_yielding(_73337)), _73339 = _73337, relation_empty_yielding(_73339)], (80 ^ _71094) ^ [_73632, _73634] : [-(transfinite_sequence(_73632)), _73634 = _73632, transfinite_sequence(_73634)], (90 ^ _71094) ^ [_73927, _73929] : [-(relation(_73927)), _73929 = _73927, relation(_73929)], (100 ^ _71094) ^ [_74222, _74224] : [-(relation_non_empty(_74222)), _74224 = _74222, relation_non_empty(_74224)], (110 ^ _71094) ^ [_74517, _74519] : [-(function(_74517)), _74519 = _74517, function(_74519)], (120 ^ _71094) ^ [_74840, _74842, _74844, _74846] : [-(element(_74844, _74840)), element(_74846, _74842), _74846 = _74844, _74842 = _74840], (134 ^ _71094) ^ [_75284, _75286, _75288, _75290] : [-(in(_75288, _75284)), in(_75290, _75286), _75290 = _75288, _75286 = _75284], (148 ^ _71094) ^ [_75700, _75702] : [-(empty(_75700)), _75702 = _75700, empty(_75702)], (158 ^ _71094) ^ [_76023, _76025, _76027, _76029] : [-(subset(_76027, _76023)), subset(_76029, _76025), _76029 = _76027, _76025 = _76023], (172 ^ _71094) ^ [_76447, _76449, _76451, _76453] : [-(transfinite_sequence_of(_76451, _76447)), transfinite_sequence_of(_76453, _76449), _76453 = _76451, _76449 = _76447]], input).
% 0.34/1.37 ncf('1',plain,[transfinite_sequence_of(539 ^ [], 536 ^ [])],start(543 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(transfinite_sequence_of(539 ^ [], 536 ^ [])), 280 : subset(relation_rng(539 ^ []), 536 ^ []), 280 : relation(539 ^ []), 280 : function(539 ^ []), 280 : transfinite_sequence(539 ^ [])],extension(262 ^ 1,bind([[_79248, _79250], [539 ^ [], 536 ^ []]]))).
% 0.34/1.37 ncf('1.1.1',plain,[-(subset(relation_rng(539 ^ []), 536 ^ [])), subset(relation_rng(539 ^ []), 535 ^ []), subset(535 ^ [], 536 ^ [])],extension(462 ^ 4,bind([[_85214, _85216, _85218], [536 ^ [], 535 ^ [], relation_rng(539 ^ [])]]))).
% 0.34/1.37 ncf('1.1.1.1',plain,[-(subset(relation_rng(539 ^ []), 535 ^ [])), 274 : transfinite_sequence_of(539 ^ [], 535 ^ []), 274 : relation(539 ^ []), 274 : function(539 ^ []), 274 : transfinite_sequence(539 ^ [])],extension(262 ^ 5,bind([[_79248, _79250], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.1.1.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 8)).
% 0.34/1.37 ncf('1.1.1.1.2',plain,[-(relation(539 ^ [])), transfinite_sequence_of(539 ^ [], 535 ^ [])],extension(286 ^ 6,bind([[_79890, _79892], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.1.1.2.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 7)).
% 0.34/1.37 ncf('1.1.1.1.3',plain,[-(function(539 ^ [])), transfinite_sequence_of(539 ^ [], 535 ^ [])],extension(286 ^ 6,bind([[_79890, _79892], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.1.1.3.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 7)).
% 0.34/1.37 ncf('1.1.1.1.4',plain,[-(transfinite_sequence(539 ^ [])), transfinite_sequence_of(539 ^ [], 535 ^ [])],extension(286 ^ 6,bind([[_79890, _79892], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.1.1.4.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 7)).
% 0.34/1.37 ncf('1.1.1.2',plain,[-(subset(535 ^ [], 536 ^ []))],extension(538 ^ 5)).
% 0.34/1.37 ncf('1.1.2',plain,[-(relation(539 ^ [])), transfinite_sequence_of(539 ^ [], 535 ^ [])],extension(286 ^ 2,bind([[_79890, _79892], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.2.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 3)).
% 0.34/1.37 ncf('1.1.3',plain,[-(function(539 ^ [])), transfinite_sequence_of(539 ^ [], 535 ^ [])],extension(286 ^ 2,bind([[_79890, _79892], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.3.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 3)).
% 0.34/1.37 ncf('1.1.4',plain,[-(transfinite_sequence(539 ^ [])), transfinite_sequence_of(539 ^ [], 535 ^ [])],extension(286 ^ 2,bind([[_79890, _79892], [539 ^ [], 535 ^ []]]))).
% 0.34/1.37 ncf('1.1.4.1',plain,[-(transfinite_sequence_of(539 ^ [], 535 ^ []))],extension(541 ^ 3)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------