%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU101+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:12 EDT 2023
% Result : Theorem 0.59s 1.37s
% Output : Proof 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU101+1 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n024.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:19:36 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.59/1.37
% 0.59/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.59/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/1.37 %-----------------------------------------------------
% 0.59/1.37 ncf(matrix, plain, [(525 ^ _79705) ^ [] : [526 ^ _79705 : [(527 ^ _79705) ^ [] : [-(preboolean(523 ^ []))], (531 ^ _79705) ^ [] : [-(in(528 ^ [], 523 ^ []))], (533 ^ _79705) ^ [] : [-(in(529 ^ [], 523 ^ []))], (535 ^ _79705) ^ [] : [in(set_union2(528 ^ [], 529 ^ []), 523 ^ []), in(set_difference(528 ^ [], 529 ^ []), 523 ^ [])]], 540 ^ _79705 : [(553 ^ _79705) ^ [] : [preboolean(523 ^ [])], (541 ^ _79705) ^ [_97813, _97815] : [548 ^ _79705 : [(549 ^ _79705) ^ [] : [-(in(set_union2(_97815, _97813), 523 ^ []))], (551 ^ _79705) ^ [] : [-(in(set_difference(_97815, _97813), 523 ^ []))]], in(_97815, 523 ^ []), in(_97813, 523 ^ [])]]], (192 ^ _79705) ^ [_85656, _85658] : [_85658 = _85656, -(powerset(_85658) = powerset(_85656))], (198 ^ _79705) ^ [_85902, _85904, _85906, _85908] : [-(set_union2(_85908, _85904) = set_union2(_85906, _85902)), _85908 = _85906, _85904 = _85902], (208 ^ _79705) ^ [_86241, _86243, _86245, _86247] : [-(set_difference(_86247, _86243) = set_difference(_86245, _86241)), _86247 = _86245, _86243 = _86241], (2 ^ _79705) ^ [_79849] : [-(_79849 = _79849)], (4 ^ _79705) ^ [_79956, _79958] : [_79958 = _79956, -(_79956 = _79958)], (10 ^ _79705) ^ [_80160, _80162, _80164] : [-(_80164 = _80160), _80164 = _80162, _80162 = _80160], (20 ^ _79705) ^ [_80473, _80475] : [-(cup_closed(_80473)), _80475 = _80473, cup_closed(_80475)], (30 ^ _79705) ^ [_80768, _80770] : [-(cap_closed(_80768)), _80770 = _80768, cap_closed(_80770)], (40 ^ _79705) ^ [_81063, _81065] : [-(diff_closed(_81063)), _81065 = _81063, diff_closed(_81065)], (50 ^ _79705) ^ [_81358, _81360] : [-(relation(_81358)), _81360 = _81358, relation(_81360)], (60 ^ _79705) ^ [_81653, _81655] : [-(function(_81653)), _81655 = _81653, function(_81655)], (70 ^ _79705) ^ [_81948, _81950] : [-(one_to_one(_81948)), _81950 = _81948, one_to_one(_81950)], (80 ^ _79705) ^ [_82243, _82245] : [-(epsilon_transitive(_82243)), _82245 = _82243, epsilon_transitive(_82245)], (90 ^ _79705) ^ [_82538, _82540] : [-(epsilon_connected(_82538)), _82540 = _82538, epsilon_connected(_82540)], (100 ^ _79705) ^ [_82833, _82835] : [-(ordinal(_82833)), _82835 = _82833, ordinal(_82835)], (110 ^ _79705) ^ [_83128, _83130] : [-(natural(_83128)), _83130 = _83128, natural(_83130)], (120 ^ _79705) ^ [_83423, _83425] : [-(finite(_83423)), _83425 = _83423, finite(_83425)], (130 ^ _79705) ^ [_83746, _83748, _83750, _83752] : [-(subset(_83750, _83746)), subset(_83752, _83748), _83752 = _83750, _83748 = _83746], (144 ^ _79705) ^ [_84190, _84192, _84194, _84196] : [-(element(_84194, _84190)), element(_84196, _84192), _84196 = _84194, _84192 = _84190], (158 ^ _79705) ^ [_84606, _84608] : [-(empty(_84606)), _84608 = _84606, empty(_84608)], (168 ^ _79705) ^ [_84901, _84903] : [-(preboolean(_84901)), _84903 = _84901, preboolean(_84903)], (178 ^ _79705) ^ [_85204, _85206, _85208, _85210] : [-(in(_85208, _85204)), in(_85210, _85206), _85210 = _85208, _85206 = _85204], (218 ^ _79705) ^ [_86614, _86616] : [in(_86616, _86614), in(_86614, _86616)], (224 ^ _79705) ^ [_86811] : [empty(_86811), -(finite(_86811))], (230 ^ _79705) ^ [_86997] : [preboolean(_86997), 233 ^ _79705 : [(234 ^ _79705) ^ [] : [-(cup_closed(_86997))], (236 ^ _79705) ^ [] : [-(diff_closed(_86997))]]], (238 ^ _79705) ^ [_87254] : [finite(_87254), 241 ^ _79705 : [(242 ^ _79705) ^ [_87386] : [element(_87386, powerset(_87254)), -(finite(_87386))]]], (248 ^ _79705) ^ [_87591] : [-(preboolean(_87591)), cup_closed(_87591), diff_closed(_87591)], (258 ^ _79705) ^ [_87859, _87861] : [-(set_union2(_87861, _87859) = set_union2(_87859, _87861))], (274 ^ _79705) ^ [_88422] : [277 ^ _79705 : [(278 ^ _79705) ^ [] : [-(in(275 ^ [_88422], _88422))], (280 ^ _79705) ^ [] : [-(in(276 ^ [_88422], _88422))], (282 ^ _79705) ^ [] : [in(set_union2(275 ^ [_88422], 276 ^ [_88422]), _88422)]], -(cup_closed(_88422))], (260 ^ _79705) ^ [_87989] : [cup_closed(_87989), 263 ^ _79705 : [(264 ^ _79705) ^ [_88148, _88150] : [-(in(set_union2(_88150, _88148), _87989)), in(_88150, _87989), in(_88148, _87989)]]], (300 ^ _79705) ^ [_89384] : [303 ^ _79705 : [(304 ^ _79705) ^ [] : [-(in(301 ^ [_89384], _89384))], (306 ^ _79705) ^ [] : [-(in(302 ^ [_89384], _89384))], (308 ^ _79705) ^ [] : [in(set_difference(301 ^ [_89384], 302 ^ [_89384]), _89384)]], -(diff_closed(_89384))], (286 ^ _79705) ^ [_88951] : [diff_closed(_88951), 289 ^ _79705 : [(290 ^ _79705) ^ [_89110, _89112] : [-(in(set_difference(_89112, _89110), _88951)), in(_89112, _88951), in(_89110, _88951)]]], (312 ^ _79705) ^ [_89913] : [preboolean(_89913), 315 ^ _79705 : [(316 ^ _79705) ^ [] : [-(cup_closed(_89913))], (318 ^ _79705) ^ [] : [-(diff_closed(_89913))]]], (320 ^ _79705) ^ [_90136] : [-(preboolean(_90136)), cup_closed(_90136), diff_closed(_90136)], (331 ^ _79705) ^ [_90431] : [-(element(329 ^ [_90431], _90431))], (333 ^ _79705) ^ [_90543, _90545] : [finite(_90545), -(finite(set_difference(_90545, _90543)))], (339 ^ _79705) ^ [_90725] : [empty(powerset(_90725))], (341 ^ _79705) ^ [] : [-(empty(empty_set))], (343 ^ _79705) ^ [_90886, _90888] : [-(empty(_90888)), empty(set_union2(_90888, _90886))], (349 ^ _79705) ^ [_91102, _91104] : [-(empty(_91104)), empty(set_union2(_91102, _91104))], (355 ^ _79705) ^ [_91318, _91320] : [-(finite(set_union2(_91320, _91318))), finite(_91320), finite(_91318)], (365 ^ _79705) ^ [_91602, _91604] : [-(set_union2(_91604, _91604) = _91604)], (368 ^ _79705) ^ [] : [empty(366 ^ [])], (370 ^ _79705) ^ [] : [-(finite(366 ^ []))], (373 ^ _79705) ^ [] : [empty(371 ^ [])], (375 ^ _79705) ^ [] : [-(cup_closed(371 ^ []))], (377 ^ _79705) ^ [] : [-(cap_closed(371 ^ []))], (379 ^ _79705) ^ [] : [-(diff_closed(371 ^ []))], (381 ^ _79705) ^ [] : [-(preboolean(371 ^ []))], (383 ^ _79705) ^ [_92180] : [-(empty(_92180)), 387 ^ _79705 : [(388 ^ _79705) ^ [] : [-(element(386 ^ [_92180], powerset(_92180)))], (390 ^ _79705) ^ [] : [empty(386 ^ [_92180])]]], (393 ^ _79705) ^ [] : [-(empty(391 ^ []))], (396 ^ _79705) ^ [_92692] : [-(element(394 ^ [_92692], powerset(_92692)))], (398 ^ _79705) ^ [_92763] : [-(empty(394 ^ [_92763]))], (400 ^ _79705) ^ [_92831] : [-(relation(394 ^ [_92831]))], (402 ^ _79705) ^ [_92899] : [-(function(394 ^ [_92899]))], (404 ^ _79705) ^ [_92967] : [-(one_to_one(394 ^ [_92967]))], (406 ^ _79705) ^ [_93035] : [-(epsilon_transitive(394 ^ [_93035]))], (408 ^ _79705) ^ [_93103] : [-(epsilon_connected(394 ^ [_93103]))], (410 ^ _79705) ^ [_93171] : [-(ordinal(394 ^ [_93171]))], (412 ^ _79705) ^ [_93239] : [-(natural(394 ^ [_93239]))], (414 ^ _79705) ^ [_93287] : [-(finite(394 ^ [_93287]))], (417 ^ _79705) ^ [_93453] : [-(element(415 ^ [_93453], powerset(_93453)))], (419 ^ _79705) ^ [_93504] : [-(empty(415 ^ [_93504]))], (422 ^ _79705) ^ [] : [empty(420 ^ [])], (424 ^ _79705) ^ [_93693] : [-(empty(_93693)), 428 ^ _79705 : [(429 ^ _79705) ^ [] : [-(element(427 ^ [_93693], powerset(_93693)))], (431 ^ _79705) ^ [] : [empty(427 ^ [_93693])], (433 ^ _79705) ^ [] : [-(finite(427 ^ [_93693]))]]], (435 ^ _79705) ^ [_94105] : [-(empty(_94105)), 439 ^ _79705 : [(440 ^ _79705) ^ [] : [-(element(438 ^ [_94105], powerset(_94105)))], (442 ^ _79705) ^ [] : [empty(438 ^ [_94105])], (444 ^ _79705) ^ [] : [-(finite(438 ^ [_94105]))]]], (446 ^ _79705) ^ [_94516, _94518] : [-(subset(_94518, _94518))], (448 ^ _79705) ^ [_94596] : [-(set_union2(_94596, empty_set) = _94596)], (450 ^ _79705) ^ [_94706, _94708] : [in(_94708, _94706), -(element(_94708, _94706))], (456 ^ _79705) ^ [_94916, _94918] : [element(_94918, _94916), -(empty(_94916)), -(in(_94918, _94916))], (466 ^ _79705) ^ [_95185] : [-(set_difference(_95185, empty_set) = _95185)], (468 ^ _79705) ^ [_95324, _95326] : [element(_95326, powerset(_95324)), -(subset(_95326, _95324))], (474 ^ _79705) ^ [_95490, _95492] : [subset(_95492, _95490), -(element(_95492, powerset(_95490)))], (480 ^ _79705) ^ [_95677] : [-(set_difference(empty_set, _95677) = empty_set)], (482 ^ _79705) ^ [_95801, _95803, _95805] : [-(element(_95805, _95801)), in(_95805, _95803), element(_95803, powerset(_95801))], (492 ^ _79705) ^ [_96128, _96130, _96132] : [in(_96132, _96130), element(_96130, powerset(_96128)), empty(_96128)], (502 ^ _79705) ^ [_96424] : [empty(_96424), -(_96424 = empty_set)], (508 ^ _79705) ^ [_96626, _96628] : [in(_96628, _96626), empty(_96626)], (514 ^ _79705) ^ [_96813, _96815] : [empty(_96815), -(_96815 = _96813), empty(_96813)]], input).
% 0.59/1.37 ncf('1',plain,[535 : in(set_union2(528 ^ [], 529 ^ []), 523 ^ []), 535 : in(set_difference(528 ^ [], 529 ^ []), 523 ^ []), 553 : preboolean(523 ^ [])],start(525 ^ 0)).
% 0.59/1.37 ncf('1.1',plain,[-(in(set_union2(528 ^ [], 529 ^ []), 523 ^ [])), 264 : in(528 ^ [], 523 ^ []), 264 : in(529 ^ [], 523 ^ []), 264 : cup_closed(523 ^ [])],extension(260 ^ 3,bind([[_87989, _88148, _88150], [523 ^ [], 529 ^ [], 528 ^ []]]))).
% 0.59/1.37 ncf('1.1.1',plain,[-(in(528 ^ [], 523 ^ []))],extension(531 ^ 6)).
% 0.59/1.37 ncf('1.1.2',plain,[-(in(529 ^ [], 523 ^ []))],extension(533 ^ 6)).
% 0.59/1.37 ncf('1.1.3',plain,[-(cup_closed(523 ^ [])), preboolean(523 ^ [])],extension(230 ^ 4,bind([[_86997], [523 ^ []]]))).
% 0.59/1.37 ncf('1.1.3.1',plain,[-(preboolean(523 ^ []))],extension(527 ^ 5)).
% 0.59/1.37 ncf('1.2',plain,[-(in(set_difference(528 ^ [], 529 ^ []), 523 ^ [])), 290 : in(528 ^ [], 523 ^ []), 290 : in(529 ^ [], 523 ^ []), 290 : diff_closed(523 ^ [])],extension(286 ^ 3,bind([[_88951, _89110, _89112], [523 ^ [], 529 ^ [], 528 ^ []]]))).
% 0.59/1.37 ncf('1.2.1',plain,[-(in(528 ^ [], 523 ^ []))],extension(531 ^ 6)).
% 0.59/1.37 ncf('1.2.2',plain,[-(in(529 ^ [], 523 ^ []))],extension(533 ^ 6)).
% 0.59/1.37 ncf('1.2.3',plain,[-(diff_closed(523 ^ [])), preboolean(523 ^ [])],extension(230 ^ 4,bind([[_86997], [523 ^ []]]))).
% 0.59/1.37 ncf('1.2.3.1',plain,[-(preboolean(523 ^ []))],extension(527 ^ 5)).
% 0.59/1.37 ncf('1.3',plain,[-(preboolean(523 ^ [])), cup_closed(523 ^ []), diff_closed(523 ^ [])],extension(248 ^ 3,bind([[_87591], [523 ^ []]]))).
% 0.59/1.37 ncf('1.3.1',plain,[-(cup_closed(523 ^ [])), 278 : -(in(275 ^ [523 ^ []], 523 ^ []))],extension(274 ^ 4,bind([[_88422], [523 ^ []]]))).
% 0.59/1.37 ncf('1.3.1.1',plain,[in(275 ^ [523 ^ []], 523 ^ []), 549 : -(in(set_union2(275 ^ [523 ^ []], 276 ^ [523 ^ []]), 523 ^ [])), 549 : in(276 ^ [523 ^ []], 523 ^ [])],extension(541 ^ 7,bind([[_97813, _97815], [276 ^ [523 ^ []], 275 ^ [523 ^ []]]]))).
% 0.59/1.37 ncf('1.3.1.1.1',plain,[in(set_union2(275 ^ [523 ^ []], 276 ^ [523 ^ []]), 523 ^ [])],extension(282 ^ 10)).
% 0.59/1.37 ncf('1.3.1.1.2',plain,[-(in(276 ^ [523 ^ []], 523 ^ []))],extension(280 ^ 8)).
% 0.59/1.37 ncf('1.3.2',plain,[-(diff_closed(523 ^ [])), 304 : -(in(301 ^ [523 ^ []], 523 ^ []))],extension(300 ^ 4,bind([[_89384], [523 ^ []]]))).
% 0.59/1.37 ncf('1.3.2.1',plain,[in(301 ^ [523 ^ []], 523 ^ []), 551 : -(in(set_difference(301 ^ [523 ^ []], 302 ^ [523 ^ []]), 523 ^ [])), 551 : in(302 ^ [523 ^ []], 523 ^ [])],extension(541 ^ 7,bind([[_97813, _97815], [302 ^ [523 ^ []], 301 ^ [523 ^ []]]]))).
% 0.59/1.37 ncf('1.3.2.1.1',plain,[in(set_difference(301 ^ [523 ^ []], 302 ^ [523 ^ []]), 523 ^ [])],extension(308 ^ 10)).
% 0.59/1.37 ncf('1.3.2.1.2',plain,[-(in(302 ^ [523 ^ []], 523 ^ []))],extension(306 ^ 8)).
% 0.59/1.37 %-----------------------------------------------------
% 0.59/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------