%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU031+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:06 EDT 2023
% Result : Theorem 0.37s 1.32s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.09 % Problem : SEU031+1 : TPTP v8.1.2. Released v3.2.0.
% 0.09/0.09 % Command : nanocop.sh %s %d
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Thu May 18 13:16:19 EDT 2023
% 0.09/0.28 % CPUTime :
% 0.37/1.32
% 0.37/1.32 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.32 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.32 %-----------------------------------------------------
% 0.37/1.32 ncf(matrix, plain, [(510 ^ _75492) ^ [] : [-(relation(508 ^ []))], (512 ^ _75492) ^ [] : [-(function(508 ^ []))], (515 ^ _75492) ^ [] : [-(relation(513 ^ []))], (517 ^ _75492) ^ [] : [-(function(513 ^ []))], (519 ^ _75492) ^ [] : [-(one_to_one(508 ^ []))], (521 ^ _75492) ^ [] : [-(relation_rng(513 ^ []) = relation_dom(508 ^ []))], (523 ^ _75492) ^ [] : [-(relation_composition(513 ^ [], 508 ^ []) = identity_relation(relation_rng(508 ^ [])))], (525 ^ _75492) ^ [] : [513 ^ [] = function_inverse(508 ^ [])], (112 ^ _75492) ^ [_79067, _79069] : [_79069 = _79067, -(powerset(_79069) = powerset(_79067))], (118 ^ _75492) ^ [_79285, _79287] : [_79287 = _79285, -(relation_dom(_79287) = relation_dom(_79285))], (124 ^ _75492) ^ [_79531, _79533, _79535, _79537] : [-(relation_composition(_79537, _79533) = relation_composition(_79535, _79531)), _79537 = _79535, _79533 = _79531], (134 ^ _75492) ^ [_79862, _79864] : [_79864 = _79862, -(identity_relation(_79864) = identity_relation(_79862))], (140 ^ _75492) ^ [_80080, _80082] : [_80082 = _80080, -(relation_rng(_80082) = relation_rng(_80080))], (146 ^ _75492) ^ [_80278, _80280] : [_80280 = _80278, -(function_inverse(_80280) = function_inverse(_80278))], (2 ^ _75492) ^ [_75636] : [-(_75636 = _75636)], (4 ^ _75492) ^ [_75743, _75745] : [_75745 = _75743, -(_75743 = _75745)], (10 ^ _75492) ^ [_75947, _75949, _75951] : [-(_75951 = _75947), _75951 = _75949, _75949 = _75947], (20 ^ _75492) ^ [_76260, _76262] : [-(relation_empty_yielding(_76260)), _76262 = _76260, relation_empty_yielding(_76262)], (30 ^ _75492) ^ [_76583, _76585, _76587, _76589] : [-(subset(_76587, _76583)), subset(_76589, _76585), _76589 = _76587, _76585 = _76583], (44 ^ _75492) ^ [_77027, _77029, _77031, _77033] : [-(element(_77031, _77027)), element(_77033, _77029), _77033 = _77031, _77029 = _77027], (58 ^ _75492) ^ [_77471, _77473, _77475, _77477] : [-(in(_77475, _77471)), in(_77477, _77473), _77477 = _77475, _77473 = _77471], (72 ^ _75492) ^ [_77887, _77889] : [-(empty(_77887)), _77889 = _77887, empty(_77889)], (82 ^ _75492) ^ [_78182, _78184] : [-(relation(_78182)), _78184 = _78182, relation(_78184)], (92 ^ _75492) ^ [_78477, _78479] : [-(function(_78477)), _78479 = _78477, function(_78479)], (102 ^ _75492) ^ [_78752, _78754] : [-(one_to_one(_78752)), _78754 = _78752, one_to_one(_78754)], (152 ^ _75492) ^ [_80518, _80520] : [in(_80520, _80518), in(_80518, _80520)], (158 ^ _75492) ^ [_80715] : [empty(_80715), -(function(_80715))], (164 ^ _75492) ^ [_80901] : [empty(_80901), -(relation(_80901))], (170 ^ _75492) ^ [_81087] : [181 ^ _75492 : [(182 ^ _75492) ^ [] : [-(relation(_81087))], (184 ^ _75492) ^ [] : [-(function(_81087))], (186 ^ _75492) ^ [] : [-(one_to_one(_81087))]], relation(_81087), empty(_81087), function(_81087)], (188 ^ _75492) ^ [_81580] : [195 ^ _75492 : [(196 ^ _75492) ^ [] : [-(relation(function_inverse(_81580)))], (198 ^ _75492) ^ [] : [-(function(function_inverse(_81580)))]], relation(_81580), function(_81580)], (200 ^ _75492) ^ [_81942, _81944] : [-(relation(relation_composition(_81944, _81942))), relation(_81944), relation(_81942)], (210 ^ _75492) ^ [_82212] : [-(relation(identity_relation(_82212)))], (213 ^ _75492) ^ [_82330] : [-(element(211 ^ [_82330], _82330))], (215 ^ _75492) ^ [_82442, _82444] : [222 ^ _75492 : [(223 ^ _75492) ^ [] : [-(empty(relation_composition(_82442, _82444)))], (225 ^ _75492) ^ [] : [-(relation(relation_composition(_82442, _82444)))]], empty(_82444), relation(_82442)], (227 ^ _75492) ^ [] : [-(empty(empty_set))], (229 ^ _75492) ^ [] : [-(relation(empty_set))], (231 ^ _75492) ^ [] : [-(relation_empty_yielding(empty_set))], (233 ^ _75492) ^ [_82983, _82985] : [248 ^ _75492 : [(249 ^ _75492) ^ [] : [-(relation(relation_composition(_82985, _82983)))], (251 ^ _75492) ^ [] : [-(function(relation_composition(_82985, _82983)))]], relation(_82985), function(_82985), relation(_82983), function(_82983)], (253 ^ _75492) ^ [_83505] : [empty(powerset(_83505))], (255 ^ _75492) ^ [] : [-(empty(empty_set))], (257 ^ _75492) ^ [_83657] : [-(relation(identity_relation(_83657)))], (259 ^ _75492) ^ [_83702] : [-(function(identity_relation(_83702)))], (261 ^ _75492) ^ [] : [-(empty(empty_set))], (263 ^ _75492) ^ [] : [-(relation(empty_set))], (265 ^ _75492) ^ [_83906] : [empty(relation_dom(_83906)), -(empty(_83906)), relation(_83906)], (275 ^ _75492) ^ [_84183] : [empty(relation_rng(_84183)), -(empty(_84183)), relation(_84183)], (285 ^ _75492) ^ [_84460] : [empty(_84460), 288 ^ _75492 : [(289 ^ _75492) ^ [] : [-(empty(relation_dom(_84460)))], (291 ^ _75492) ^ [] : [-(relation(relation_dom(_84460)))]]], (293 ^ _75492) ^ [_84725] : [empty(_84725), 296 ^ _75492 : [(297 ^ _75492) ^ [] : [-(empty(relation_rng(_84725)))], (299 ^ _75492) ^ [] : [-(relation(relation_rng(_84725)))]]], (301 ^ _75492) ^ [_85004, _85006] : [308 ^ _75492 : [(309 ^ _75492) ^ [] : [-(empty(relation_composition(_85006, _85004)))], (311 ^ _75492) ^ [] : [-(relation(relation_composition(_85006, _85004)))]], empty(_85006), relation(_85004)], (313 ^ _75492) ^ [_85382, _85384] : [relation(_85382), function(_85382), 320 ^ _75492 : [(321 ^ _75492) ^ [_85655] : [relation(_85655), function(_85655), 328 ^ _75492 : [(329 ^ _75492) ^ [_85925] : [relation(_85925), function(_85925), -(_85925 = _85382), relation_rng(_85382) = _85384, relation_composition(_85382, _85655) = identity_relation(relation_dom(_85925)), relation_composition(_85655, _85925) = identity_relation(_85384)]]]]], (352 ^ _75492) ^ [] : [-(relation(350 ^ []))], (354 ^ _75492) ^ [] : [-(function(350 ^ []))], (357 ^ _75492) ^ [] : [-(empty(355 ^ []))], (359 ^ _75492) ^ [] : [-(relation(355 ^ []))], (361 ^ _75492) ^ [_86865] : [-(empty(_86865)), 365 ^ _75492 : [(366 ^ _75492) ^ [] : [-(element(364 ^ [_86865], powerset(_86865)))], (368 ^ _75492) ^ [] : [empty(364 ^ [_86865])]]], (371 ^ _75492) ^ [] : [-(empty(369 ^ []))], (374 ^ _75492) ^ [] : [-(relation(372 ^ []))], (376 ^ _75492) ^ [] : [-(empty(372 ^ []))], (378 ^ _75492) ^ [] : [-(function(372 ^ []))], (381 ^ _75492) ^ [] : [empty(379 ^ [])], (383 ^ _75492) ^ [] : [-(relation(379 ^ []))], (386 ^ _75492) ^ [_87696] : [-(element(384 ^ [_87696], powerset(_87696)))], (388 ^ _75492) ^ [_87747] : [-(empty(384 ^ [_87747]))], (391 ^ _75492) ^ [] : [empty(389 ^ [])], (394 ^ _75492) ^ [] : [-(relation(392 ^ []))], (396 ^ _75492) ^ [] : [-(function(392 ^ []))], (398 ^ _75492) ^ [] : [-(one_to_one(392 ^ []))], (401 ^ _75492) ^ [] : [-(relation(399 ^ []))], (403 ^ _75492) ^ [] : [-(relation_empty_yielding(399 ^ []))], (405 ^ _75492) ^ [_88293, _88295] : [-(subset(_88295, _88295))], (407 ^ _75492) ^ [_88402, _88404] : [in(_88404, _88402), -(element(_88404, _88402))], (413 ^ _75492) ^ [_88612, _88614] : [element(_88614, _88612), -(empty(_88612)), -(in(_88614, _88612))], (423 ^ _75492) ^ [_88939, _88941] : [element(_88941, powerset(_88939)), -(subset(_88941, _88939))], (429 ^ _75492) ^ [_89105, _89107] : [subset(_89107, _89105), -(element(_89107, powerset(_89105)))], (435 ^ _75492) ^ [_89335, _89337, _89339] : [-(element(_89339, _89335)), in(_89339, _89337), element(_89337, powerset(_89335))], (445 ^ _75492) ^ [_89634] : [relation(_89634), function(_89634), one_to_one(_89634), 456 ^ _75492 : [(457 ^ _75492) ^ [] : [-(relation_rng(_89634) = relation_dom(function_inverse(_89634)))], (459 ^ _75492) ^ [] : [-(relation_dom(_89634) = relation_rng(function_inverse(_89634)))]]], (461 ^ _75492) ^ [_90115, _90117, _90119] : [in(_90119, _90117), element(_90117, powerset(_90115)), empty(_90115)], (471 ^ _75492) ^ [_90411] : [relation(_90411), function(_90411), one_to_one(_90411), 482 ^ _75492 : [(483 ^ _75492) ^ [] : [-(relation_composition(_90411, function_inverse(_90411)) = identity_relation(relation_dom(_90411)))], (485 ^ _75492) ^ [] : [-(relation_composition(function_inverse(_90411), _90411) = identity_relation(relation_rng(_90411)))]]], (487 ^ _75492) ^ [_90876] : [empty(_90876), -(_90876 = empty_set)], (493 ^ _75492) ^ [_91078, _91080] : [in(_91080, _91078), empty(_91078)], (499 ^ _75492) ^ [_91265, _91267] : [empty(_91267), -(_91267 = _91265), empty(_91265)]], input).
% 0.37/1.32 ncf('1',plain,[513 ^ [] = function_inverse(508 ^ [])],start(525 ^ 0)).
% 0.37/1.32 ncf('1.1',plain,[-(513 ^ [] = function_inverse(508 ^ [])), function_inverse(508 ^ []) = 513 ^ []],extension(4 ^ 1,bind([[_75743, _75745], [513 ^ [], function_inverse(508 ^ [])]]))).
% 0.37/1.32 ncf('1.1.1',plain,[-(function_inverse(508 ^ []) = 513 ^ []), 329 : relation(function_inverse(508 ^ [])), 329 : function(function_inverse(508 ^ [])), 329 : relation_rng(513 ^ []) = relation_dom(508 ^ []), 329 : relation_composition(513 ^ [], 508 ^ []) = identity_relation(relation_dom(function_inverse(508 ^ []))), 329 : relation_composition(508 ^ [], function_inverse(508 ^ [])) = identity_relation(relation_dom(508 ^ [])), 329 : relation(508 ^ []), 329 : function(508 ^ []), 321 : relation(513 ^ []), 321 : function(513 ^ [])],extension(313 ^ 2,bind([[_85382, _85384, _85655, _85925], [513 ^ [], relation_dom(508 ^ []), 508 ^ [], function_inverse(508 ^ [])]]))).
% 0.37/1.32 ncf('1.1.1.1',plain,[-(relation(function_inverse(508 ^ []))), relation(508 ^ []), function(508 ^ [])],extension(188 ^ 7,bind([[_81580], [508 ^ []]]))).
% 0.37/1.32 ncf('1.1.1.1.1',plain,[-(relation(508 ^ []))],extension(510 ^ 8)).
% 0.37/1.32 ncf('1.1.1.1.2',plain,[-(function(508 ^ []))],extension(512 ^ 8)).
% 0.37/1.32 ncf('1.1.1.2',plain,[-(function(function_inverse(508 ^ []))), relation(508 ^ []), function(508 ^ [])],extension(188 ^ 7,bind([[_81580], [508 ^ []]]))).
% 0.37/1.32 ncf('1.1.1.2.1',plain,[-(relation(508 ^ []))],extension(510 ^ 8)).
% 0.37/1.32 ncf('1.1.1.2.2',plain,[-(function(508 ^ []))],extension(512 ^ 8)).
% 0.37/1.32 ncf('1.1.1.3',plain,[-(relation_rng(513 ^ []) = relation_dom(508 ^ []))],extension(521 ^ 7)).
% 0.37/1.32 ncf('1.1.1.4',plain,[-(relation_composition(513 ^ [], 508 ^ []) = identity_relation(relation_dom(function_inverse(508 ^ [])))), relation_composition(513 ^ [], 508 ^ []) = identity_relation(relation_rng(508 ^ [])), identity_relation(relation_rng(508 ^ [])) = identity_relation(relation_dom(function_inverse(508 ^ [])))],extension(10 ^ 7,bind([[_75947, _75949, _75951], [identity_relation(relation_dom(function_inverse(508 ^ []))), identity_relation(relation_rng(508 ^ [])), relation_composition(513 ^ [], 508 ^ [])]]))).
% 0.37/1.32 ncf('1.1.1.4.1',plain,[-(relation_composition(513 ^ [], 508 ^ []) = identity_relation(relation_rng(508 ^ [])))],extension(523 ^ 8)).
% 0.37/1.32 ncf('1.1.1.4.2',plain,[-(identity_relation(relation_rng(508 ^ [])) = identity_relation(relation_dom(function_inverse(508 ^ [])))), relation_rng(508 ^ []) = relation_dom(function_inverse(508 ^ []))],extension(134 ^ 8,bind([[_79862, _79864], [relation_dom(function_inverse(508 ^ [])), relation_rng(508 ^ [])]]))).
% 0.37/1.32 ncf('1.1.1.4.2.1',plain,[-(relation_rng(508 ^ []) = relation_dom(function_inverse(508 ^ []))), relation(508 ^ []), function(508 ^ []), one_to_one(508 ^ [])],extension(445 ^ 9,bind([[_89634], [508 ^ []]]))).
% 0.37/1.32 ncf('1.1.1.4.2.1.1',plain,[-(relation(508 ^ []))],extension(510 ^ 10)).
% 0.37/1.32 ncf('1.1.1.4.2.1.2',plain,[-(function(508 ^ []))],extension(512 ^ 10)).
% 0.37/1.32 ncf('1.1.1.4.2.1.3',plain,[-(one_to_one(508 ^ []))],extension(519 ^ 10)).
% 0.37/1.32 ncf('1.1.1.5',plain,[-(relation_composition(508 ^ [], function_inverse(508 ^ [])) = identity_relation(relation_dom(508 ^ []))), relation(508 ^ []), function(508 ^ []), one_to_one(508 ^ [])],extension(471 ^ 7,bind([[_90411], [508 ^ []]]))).
% 0.37/1.32 ncf('1.1.1.5.1',plain,[-(relation(508 ^ []))],extension(510 ^ 8)).
% 0.37/1.32 ncf('1.1.1.5.2',plain,[-(function(508 ^ []))],extension(512 ^ 8)).
% 0.37/1.32 ncf('1.1.1.5.3',plain,[-(one_to_one(508 ^ []))],extension(519 ^ 8)).
% 0.37/1.32 ncf('1.1.1.6',plain,[-(relation(508 ^ []))],extension(510 ^ 5)).
% 0.37/1.32 ncf('1.1.1.7',plain,[-(function(508 ^ []))],extension(512 ^ 5)).
% 0.37/1.32 ncf('1.1.1.8',plain,[-(relation(513 ^ []))],extension(515 ^ 3)).
% 0.37/1.32 ncf('1.1.1.9',plain,[-(function(513 ^ []))],extension(517 ^ 3)).
% 0.37/1.32 %-----------------------------------------------------
% 0.37/1.32 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------