%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU026+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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 101.90s 98.90s
% Output : Proof 101.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU026+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n020.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:37:02 EDT 2023
% 0.12/0.34 % CPUTime :
% 101.90/98.90
% 101.90/98.90 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 101.90/98.90 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.90/98.90 %-----------------------------------------------------
% 101.90/98.90 ncf(matrix, plain, [(472 ^ _71589) ^ [] : [-(relation(470 ^ []))], (474 ^ _71589) ^ [] : [-(function(470 ^ []))], (476 ^ _71589) ^ [] : [-(one_to_one(470 ^ []))], (478 ^ _71589) ^ [] : [relation_dom(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ []), relation_rng(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ [])], (112 ^ _71589) ^ [_75164, _75166] : [_75166 = _75164, -(powerset(_75166) = powerset(_75164))], (118 ^ _71589) ^ [_75382, _75384] : [_75384 = _75382, -(relation_dom(_75384) = relation_dom(_75382))], (124 ^ _71589) ^ [_75628, _75630, _75632, _75634] : [-(relation_composition(_75634, _75630) = relation_composition(_75632, _75628)), _75634 = _75632, _75630 = _75628], (134 ^ _71589) ^ [_75959, _75961] : [_75961 = _75959, -(function_inverse(_75961) = function_inverse(_75959))], (140 ^ _71589) ^ [_76157, _76159] : [_76159 = _76157, -(relation_rng(_76159) = relation_rng(_76157))], (2 ^ _71589) ^ [_71733] : [-(_71733 = _71733)], (4 ^ _71589) ^ [_71840, _71842] : [_71842 = _71840, -(_71840 = _71842)], (10 ^ _71589) ^ [_72044, _72046, _72048] : [-(_72048 = _72044), _72048 = _72046, _72046 = _72044], (20 ^ _71589) ^ [_72357, _72359] : [-(relation_empty_yielding(_72357)), _72359 = _72357, relation_empty_yielding(_72359)], (30 ^ _71589) ^ [_72680, _72682, _72684, _72686] : [-(subset(_72684, _72680)), subset(_72686, _72682), _72686 = _72684, _72682 = _72680], (44 ^ _71589) ^ [_73124, _73126, _73128, _73130] : [-(element(_73128, _73124)), element(_73130, _73126), _73130 = _73128, _73126 = _73124], (58 ^ _71589) ^ [_73568, _73570, _73572, _73574] : [-(in(_73572, _73568)), in(_73574, _73570), _73574 = _73572, _73570 = _73568], (72 ^ _71589) ^ [_73984, _73986] : [-(empty(_73984)), _73986 = _73984, empty(_73986)], (82 ^ _71589) ^ [_74279, _74281] : [-(relation(_74279)), _74281 = _74279, relation(_74281)], (92 ^ _71589) ^ [_74574, _74576] : [-(function(_74574)), _74576 = _74574, function(_74576)], (102 ^ _71589) ^ [_74849, _74851] : [-(one_to_one(_74849)), _74851 = _74849, one_to_one(_74851)], (146 ^ _71589) ^ [_76393, _76395] : [in(_76395, _76393), in(_76393, _76395)], (152 ^ _71589) ^ [_76590] : [empty(_76590), -(function(_76590))], (158 ^ _71589) ^ [_76776] : [empty(_76776), -(relation(_76776))], (164 ^ _71589) ^ [_76962] : [175 ^ _71589 : [(176 ^ _71589) ^ [] : [-(relation(_76962))], (178 ^ _71589) ^ [] : [-(function(_76962))], (180 ^ _71589) ^ [] : [-(one_to_one(_76962))]], relation(_76962), empty(_76962), function(_76962)], (182 ^ _71589) ^ [_77455] : [189 ^ _71589 : [(190 ^ _71589) ^ [] : [-(relation(function_inverse(_77455)))], (192 ^ _71589) ^ [] : [-(function(function_inverse(_77455)))]], relation(_77455), function(_77455)], (194 ^ _71589) ^ [_77817, _77819] : [-(relation(relation_composition(_77819, _77817))), relation(_77819), relation(_77817)], (205 ^ _71589) ^ [_78126] : [-(element(203 ^ [_78126], _78126))], (207 ^ _71589) ^ [_78238, _78240] : [214 ^ _71589 : [(215 ^ _71589) ^ [] : [-(empty(relation_composition(_78238, _78240)))], (217 ^ _71589) ^ [] : [-(relation(relation_composition(_78238, _78240)))]], empty(_78240), relation(_78238)], (219 ^ _71589) ^ [] : [-(empty(empty_set))], (221 ^ _71589) ^ [] : [-(relation(empty_set))], (223 ^ _71589) ^ [] : [-(relation_empty_yielding(empty_set))], (225 ^ _71589) ^ [_78779, _78781] : [240 ^ _71589 : [(241 ^ _71589) ^ [] : [-(relation(relation_composition(_78781, _78779)))], (243 ^ _71589) ^ [] : [-(function(relation_composition(_78781, _78779)))]], relation(_78781), function(_78781), relation(_78779), function(_78779)], (245 ^ _71589) ^ [_79301] : [empty(powerset(_79301))], (247 ^ _71589) ^ [] : [-(empty(empty_set))], (249 ^ _71589) ^ [] : [-(empty(empty_set))], (251 ^ _71589) ^ [] : [-(relation(empty_set))], (253 ^ _71589) ^ [_79556] : [empty(relation_dom(_79556)), -(empty(_79556)), relation(_79556)], (263 ^ _71589) ^ [_79833] : [empty(relation_rng(_79833)), -(empty(_79833)), relation(_79833)], (273 ^ _71589) ^ [_80110] : [empty(_80110), 276 ^ _71589 : [(277 ^ _71589) ^ [] : [-(empty(relation_dom(_80110)))], (279 ^ _71589) ^ [] : [-(relation(relation_dom(_80110)))]]], (281 ^ _71589) ^ [_80375] : [empty(_80375), 284 ^ _71589 : [(285 ^ _71589) ^ [] : [-(empty(relation_rng(_80375)))], (287 ^ _71589) ^ [] : [-(relation(relation_rng(_80375)))]]], (289 ^ _71589) ^ [_80654, _80656] : [296 ^ _71589 : [(297 ^ _71589) ^ [] : [-(empty(relation_composition(_80656, _80654)))], (299 ^ _71589) ^ [] : [-(relation(relation_composition(_80656, _80654)))]], empty(_80656), relation(_80654)], (302 ^ _71589) ^ [] : [-(relation(300 ^ []))], (304 ^ _71589) ^ [] : [-(function(300 ^ []))], (307 ^ _71589) ^ [] : [-(empty(305 ^ []))], (309 ^ _71589) ^ [] : [-(relation(305 ^ []))], (311 ^ _71589) ^ [_81316] : [-(empty(_81316)), 315 ^ _71589 : [(316 ^ _71589) ^ [] : [-(element(314 ^ [_81316], powerset(_81316)))], (318 ^ _71589) ^ [] : [empty(314 ^ [_81316])]]], (321 ^ _71589) ^ [] : [-(empty(319 ^ []))], (324 ^ _71589) ^ [] : [-(relation(322 ^ []))], (326 ^ _71589) ^ [] : [-(empty(322 ^ []))], (328 ^ _71589) ^ [] : [-(function(322 ^ []))], (331 ^ _71589) ^ [] : [empty(329 ^ [])], (333 ^ _71589) ^ [] : [-(relation(329 ^ []))], (336 ^ _71589) ^ [_82147] : [-(element(334 ^ [_82147], powerset(_82147)))], (338 ^ _71589) ^ [_82198] : [-(empty(334 ^ [_82198]))], (341 ^ _71589) ^ [] : [empty(339 ^ [])], (344 ^ _71589) ^ [] : [-(relation(342 ^ []))], (346 ^ _71589) ^ [] : [-(function(342 ^ []))], (348 ^ _71589) ^ [] : [-(one_to_one(342 ^ []))], (351 ^ _71589) ^ [] : [-(relation(349 ^ []))], (353 ^ _71589) ^ [] : [-(relation_empty_yielding(349 ^ []))], (355 ^ _71589) ^ [_82744, _82746] : [-(subset(_82746, _82746))], (357 ^ _71589) ^ [_82853, _82855] : [in(_82855, _82853), -(element(_82855, _82853))], (363 ^ _71589) ^ [_83063, _83065] : [element(_83065, _83063), -(empty(_83063)), -(in(_83065, _83063))], (373 ^ _71589) ^ [_83390, _83392] : [element(_83392, powerset(_83390)), -(subset(_83392, _83390))], (379 ^ _71589) ^ [_83556, _83558] : [subset(_83558, _83556), -(element(_83558, powerset(_83556)))], (385 ^ _71589) ^ [_83758] : [relation(_83758), 388 ^ _71589 : [(389 ^ _71589) ^ [_83905] : [relation(_83905), subset(relation_rng(_83758), relation_dom(_83905)), -(relation_dom(relation_composition(_83758, _83905)) = relation_dom(_83758))]]], (399 ^ _71589) ^ [_84217] : [relation(_84217), 402 ^ _71589 : [(403 ^ _71589) ^ [_84364] : [relation(_84364), subset(relation_dom(_84217), relation_rng(_84364)), -(relation_rng(relation_composition(_84364, _84217)) = relation_rng(_84217))]]], (413 ^ _71589) ^ [_84704, _84706, _84708] : [-(element(_84708, _84704)), in(_84708, _84706), element(_84706, powerset(_84704))], (423 ^ _71589) ^ [_85003] : [relation(_85003), function(_85003), one_to_one(_85003), 434 ^ _71589 : [(435 ^ _71589) ^ [] : [-(relation_rng(_85003) = relation_dom(function_inverse(_85003)))], (437 ^ _71589) ^ [] : [-(relation_dom(_85003) = relation_rng(function_inverse(_85003)))]]], (439 ^ _71589) ^ [_85484, _85486, _85488] : [in(_85488, _85486), element(_85486, powerset(_85484)), empty(_85484)], (449 ^ _71589) ^ [_85780] : [empty(_85780), -(_85780 = empty_set)], (455 ^ _71589) ^ [_85982, _85984] : [in(_85984, _85982), empty(_85982)], (461 ^ _71589) ^ [_86169, _86171] : [empty(_86171), -(_86171 = _86169), empty(_86169)]], input).
% 101.90/98.90 ncf('1',plain,[relation_dom(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ []), relation_rng(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ [])],start(478 ^ 0)).
% 101.90/98.90 ncf('1.1',plain,[-(relation_dom(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ [])), relation_dom(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_dom(function_inverse(470 ^ [])), relation_dom(function_inverse(470 ^ [])) = relation_rng(470 ^ [])],extension(10 ^ 1,bind([[_72044, _72046, _72048], [relation_rng(470 ^ []), relation_dom(function_inverse(470 ^ [])), relation_dom(relation_composition(function_inverse(470 ^ []), 470 ^ []))]]))).
% 101.90/98.90 ncf('1.1.1',plain,[-(relation_dom(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_dom(function_inverse(470 ^ []))), 389 : relation(470 ^ []), 389 : subset(relation_rng(function_inverse(470 ^ [])), relation_dom(470 ^ [])), 389 : relation(function_inverse(470 ^ []))],extension(385 ^ 2,bind([[_83758, _83905], [function_inverse(470 ^ []), 470 ^ []]]))).
% 101.90/98.90 ncf('1.1.1.1',plain,[-(relation(470 ^ []))],extension(472 ^ 5)).
% 101.90/98.90 ncf('1.1.1.2',plain,[-(subset(relation_rng(function_inverse(470 ^ [])), relation_dom(470 ^ []))), subset(relation_dom(470 ^ []), relation_dom(470 ^ [])), relation_dom(470 ^ []) = relation_rng(function_inverse(470 ^ [])), relation_dom(470 ^ []) = relation_dom(470 ^ [])],extension(30 ^ 5,bind([[_72680, _72682, _72684, _72686], [relation_dom(470 ^ []), relation_dom(470 ^ []), relation_rng(function_inverse(470 ^ [])), relation_dom(470 ^ [])]]))).
% 101.90/98.90 ncf('1.1.1.2.1',plain,[-(subset(relation_dom(470 ^ []), relation_dom(470 ^ [])))],extension(355 ^ 6,bind([[_82744, _82746], [_49576, relation_dom(470 ^ [])]]))).
% 101.90/98.90 ncf('1.1.1.2.2',plain,[-(relation_dom(470 ^ []) = relation_rng(function_inverse(470 ^ []))), relation(470 ^ []), function(470 ^ []), one_to_one(470 ^ [])],extension(423 ^ 6,bind([[_85003], [470 ^ []]]))).
% 101.90/98.90 ncf('1.1.1.2.2.1',plain,[-(relation(470 ^ []))],lemmata('[1, 1].x')).
% 101.90/98.90 ncf('1.1.1.2.2.2',plain,[-(function(470 ^ []))],extension(474 ^ 7)).
% 101.90/98.90 ncf('1.1.1.2.2.3',plain,[-(one_to_one(470 ^ []))],extension(476 ^ 7)).
% 101.90/98.90 ncf('1.1.1.2.3',plain,[-(relation_dom(470 ^ []) = relation_dom(470 ^ []))],extension(2 ^ 6,bind([[_71733], [relation_dom(470 ^ [])]]))).
% 101.90/98.90 ncf('1.1.1.3',plain,[-(relation(function_inverse(470 ^ []))), relation(470 ^ []), function(470 ^ [])],extension(182 ^ 3,bind([[_77455], [470 ^ []]]))).
% 101.90/98.90 ncf('1.1.1.3.1',plain,[-(relation(470 ^ []))],extension(472 ^ 4)).
% 101.90/98.90 ncf('1.1.1.3.2',plain,[-(function(470 ^ []))],extension(474 ^ 4)).
% 101.90/98.90 ncf('1.1.2',plain,[-(relation_dom(function_inverse(470 ^ [])) = relation_rng(470 ^ [])), relation_rng(470 ^ []) = relation_dom(function_inverse(470 ^ []))],extension(4 ^ 2,bind([[_71840, _71842], [relation_dom(function_inverse(470 ^ [])), relation_rng(470 ^ [])]]))).
% 101.90/98.90 ncf('1.1.2.1',plain,[-(relation_rng(470 ^ []) = relation_dom(function_inverse(470 ^ []))), relation_rng(470 ^ []) = relation_dom(function_inverse(470 ^ [])), relation_dom(function_inverse(470 ^ [])) = relation_dom(function_inverse(470 ^ []))],extension(10 ^ 3,bind([[_72044, _72046, _72048], [relation_dom(function_inverse(470 ^ [])), relation_dom(function_inverse(470 ^ [])), relation_rng(470 ^ [])]]))).
% 101.90/98.90 ncf('1.1.2.1.1',plain,[-(relation_rng(470 ^ []) = relation_dom(function_inverse(470 ^ []))), relation(470 ^ []), function(470 ^ []), one_to_one(470 ^ [])],extension(423 ^ 4,bind([[_85003], [470 ^ []]]))).
% 101.90/98.90 ncf('1.1.2.1.1.1',plain,[-(relation(470 ^ []))],extension(472 ^ 5)).
% 101.90/98.90 ncf('1.1.2.1.1.2',plain,[-(function(470 ^ []))],extension(474 ^ 5)).
% 101.90/98.90 ncf('1.1.2.1.1.3',plain,[-(one_to_one(470 ^ []))],extension(476 ^ 5)).
% 101.90/98.90 ncf('1.1.2.1.2',plain,[-(relation_dom(function_inverse(470 ^ [])) = relation_dom(function_inverse(470 ^ [])))],extension(2 ^ 4,bind([[_71733], [relation_dom(function_inverse(470 ^ []))]]))).
% 101.90/98.90 ncf('1.2',plain,[-(relation_rng(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ [])), relation_rng(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ []), relation_rng(470 ^ []) = relation_rng(470 ^ [])],extension(10 ^ 1,bind([[_72044, _72046, _72048], [relation_rng(470 ^ []), relation_rng(470 ^ []), relation_rng(relation_composition(function_inverse(470 ^ []), 470 ^ []))]]))).
% 101.90/98.90 ncf('1.2.1',plain,[-(relation_rng(relation_composition(function_inverse(470 ^ []), 470 ^ [])) = relation_rng(470 ^ [])), 403 : relation(function_inverse(470 ^ [])), 403 : subset(relation_dom(470 ^ []), relation_rng(function_inverse(470 ^ []))), 403 : relation(470 ^ [])],extension(399 ^ 2,bind([[_84217, _84364], [470 ^ [], function_inverse(470 ^ [])]]))).
% 101.90/98.90 ncf('1.2.1.1',plain,[-(relation(function_inverse(470 ^ []))), relation(470 ^ []), function(470 ^ [])],extension(182 ^ 5,bind([[_77455], [470 ^ []]]))).
% 101.90/98.90 ncf('1.2.1.1.1',plain,[-(relation(470 ^ []))],extension(472 ^ 6)).
% 101.90/98.90 ncf('1.2.1.1.2',plain,[-(function(470 ^ []))],extension(474 ^ 6)).
% 101.90/98.90 ncf('1.2.1.2',plain,[-(subset(relation_dom(470 ^ []), relation_rng(function_inverse(470 ^ [])))), subset(relation_dom(470 ^ []), relation_dom(470 ^ [])), relation_dom(470 ^ []) = relation_dom(470 ^ []), relation_dom(470 ^ []) = relation_rng(function_inverse(470 ^ []))],extension(30 ^ 5,bind([[_72680, _72682, _72684, _72686], [relation_rng(function_inverse(470 ^ [])), relation_dom(470 ^ []), relation_dom(470 ^ []), relation_dom(470 ^ [])]]))).
% 101.90/98.90 ncf('1.2.1.2.1',plain,[-(subset(relation_dom(470 ^ []), relation_dom(470 ^ [])))],extension(355 ^ 6,bind([[_82744, _82746], [_53376, relation_dom(470 ^ [])]]))).
% 101.90/98.90 ncf('1.2.1.2.2',plain,[-(relation_dom(470 ^ []) = relation_dom(470 ^ []))],extension(2 ^ 6,bind([[_71733], [relation_dom(470 ^ [])]]))).
% 101.90/98.90 ncf('1.2.1.2.3',plain,[-(relation_dom(470 ^ []) = relation_rng(function_inverse(470 ^ []))), relation(470 ^ []), function(470 ^ []), one_to_one(470 ^ [])],extension(423 ^ 6,bind([[_85003], [470 ^ []]]))).
% 101.90/98.90 ncf('1.2.1.2.3.1',plain,[-(relation(470 ^ []))],extension(472 ^ 7)).
% 101.90/98.90 ncf('1.2.1.2.3.2',plain,[-(function(470 ^ []))],extension(474 ^ 7)).
% 101.90/98.90 ncf('1.2.1.2.3.3',plain,[-(one_to_one(470 ^ []))],extension(476 ^ 7)).
% 101.90/98.90 ncf('1.2.1.3',plain,[-(relation(470 ^ []))],extension(472 ^ 3)).
% 101.90/98.90 ncf('1.2.2',plain,[-(relation_rng(470 ^ []) = relation_rng(470 ^ [])), 470 ^ [] = 470 ^ []],extension(140 ^ 2,bind([[_76157, _76159], [470 ^ [], 470 ^ []]]))).
% 101.90/98.90 ncf('1.2.2.1',plain,[-(470 ^ [] = 470 ^ [])],extension(2 ^ 3,bind([[_71733], [470 ^ []]]))).
% 101.90/98.90 %-----------------------------------------------------
% 101.90/98.90 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------