%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU220+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:43 EDT 2023
% Result : Theorem 215.00s 207.38s
% Output : Proof 215.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU220+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n031.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:47:25 EDT 2023
% 0.12/0.33 % CPUTime :
% 215.00/207.38
% 215.00/207.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 215.00/207.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 215.00/207.38 %-----------------------------------------------------
% 215.00/207.38 ncf(matrix, plain, [(521 ^ _99237) ^ [] : [-(function(517 ^ []))], (523 ^ _99237) ^ [] : [-(one_to_one(517 ^ []))], (525 ^ _99237) ^ [] : [-(in(516 ^ [], relation_rng(517 ^ [])))], (527 ^ _99237) ^ [] : [516 ^ [] = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])), 516 ^ [] = apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ [])], (519 ^ _99237) ^ [] : [-(relation(517 ^ []))], !, (241 ^ _82989) ^ [] : [-(relation(empty_set))], (154 ^ _82989) ^ [_88037] : [165 ^ _82989 : [(170 ^ _82989) ^ [] : [-(one_to_one(_88037))], (168 ^ _82989) ^ [] : [-(function(_88037))], (166 ^ _82989) ^ [] : [-(relation(_88037))]], relation(_88037), empty(_88037), function(_88037)], (352 ^ _82989) ^ [] : [-(one_to_one(346 ^ []))], (245 ^ _82989) ^ [_90449, _90451] : [260 ^ _82989 : [(263 ^ _82989) ^ [] : [-(function(relation_composition(_90451, _90449)))], (261 ^ _82989) ^ [] : [-(relation(relation_composition(_90451, _90449)))]], relation(_90451), function(_90451), relation(_90449), function(_90449)], (2 ^ _82989) ^ [_83113] : [-(_83113 = _83113)], (74 ^ _82989) ^ [_85361, _85363] : [-(one_to_one(_85361)), _85363 = _85361, one_to_one(_85363)], (44 ^ _82989) ^ [_84476, _84478] : [-(empty(_84476)), _84478 = _84476, empty(_84478)], (355 ^ _82989) ^ [] : [-(relation(353 ^ []))], (218 ^ _82989) ^ [] : [true___, -(true___)], (202 ^ _82989) ^ [] : [true___, -(true___)], (507 ^ _82989) ^ [_98664, _98666] : [empty(_98666), -(_98666 = _98664), empty(_98664)], (136 ^ _82989) ^ [_87468, _87470] : [in(_87470, _87468), in(_87468, _87470)], (307 ^ _82989) ^ [_92246, _92248] : [314 ^ _82989 : [(317 ^ _82989) ^ [] : [-(relation(relation_composition(_92248, _92246)))], (315 ^ _82989) ^ [] : [-(empty(relation_composition(_92248, _92246)))]], empty(_92248), relation(_92246)], (337 ^ _82989) ^ [] : [-(function(331 ^ []))], (98 ^ _82989) ^ [_86098, _86100] : [_86100 = _86098, -(relation_dom(_86100) = relation_dom(_86098))], (267 ^ _82989) ^ [] : [-(empty(empty_set))], (495 ^ _82989) ^ [_98275] : [empty(_98275), -(_98275 = empty_set)], (281 ^ _82989) ^ [_91425] : [empty(relation_rng(_91425)), -(empty(_91425)), relation(_91425)], (142 ^ _82989) ^ [_87665] : [empty(_87665), -(function(_87665))], (501 ^ _82989) ^ [_98477, _98479] : [in(_98479, _98477), empty(_98477)], (172 ^ _82989) ^ [] : [true___, -(true___)], (345 ^ _82989) ^ [] : [empty(343 ^ [])], (387 ^ _82989) ^ [_94713, _94715] : [element(_94715, _94713), -(empty(_94713)), -(in(_94715, _94713))], (130 ^ _82989) ^ [_87232, _87234] : [_87234 = _87232, -(function_inverse(_87234) = function_inverse(_87232))], (227 ^ _82989) ^ [_89908, _89910] : [234 ^ _82989 : [(237 ^ _82989) ^ [] : [-(relation(relation_composition(_89908, _89910)))], (235 ^ _82989) ^ [] : [-(empty(relation_composition(_89908, _89910)))]], empty(_89910), relation(_89908)], (348 ^ _82989) ^ [] : [-(relation(346 ^ []))], (320 ^ _82989) ^ [] : [-(relation(318 ^ []))], (104 ^ _82989) ^ [_86316, _86318] : [_86318 = _86316, -(relation_rng(_86318) = relation_rng(_86316))], (30 ^ _82989) ^ [_84060, _84062, _84064, _84066] : [-(element(_84064, _84060)), element(_84066, _84062), _84066 = _84064, _84062 = _84060], (64 ^ _82989) ^ [_85066, _85068] : [-(function(_85066)), _85068 = _85066, function(_85068)], (322 ^ _82989) ^ [] : [-(function(318 ^ []))], (479 ^ _82989) ^ [_97822] : [relation(_97822), function(_97822), one_to_one(_97822), 490 ^ _82989 : [(493 ^ _82989) ^ [] : [-(relation_dom(_97822) = relation_rng(function_inverse(_97822)))], (491 ^ _82989) ^ [] : [-(relation_rng(_97822) = relation_dom(function_inverse(_97822)))]]], (184 ^ _82989) ^ [] : [true___, -(true___)], (239 ^ _82989) ^ [] : [-(empty(empty_set))], (10 ^ _82989) ^ [_83424, _83426, _83428] : [-(_83428 = _83424), _83428 = _83426, _83426 = _83424], (271 ^ _82989) ^ [_91148] : [empty(relation_dom(_91148)), -(empty(_91148)), relation(_91148)], (54 ^ _82989) ^ [_84771, _84773] : [-(relation(_84771)), _84773 = _84771, relation(_84773)], (178 ^ _82989) ^ [] : [true___, -(true___)], (333 ^ _82989) ^ [] : [-(relation(331 ^ []))], (269 ^ _82989) ^ [] : [-(relation(empty_set))], (84 ^ _82989) ^ [_85664, _85666, _85668, _85670] : [-(in(_85668, _85664)), in(_85670, _85666), _85670 = _85668, _85666 = _85664], (359 ^ _82989) ^ [_93818, _93820] : [in(_93820, _93818), -(element(_93820, _93818))], (357 ^ _82989) ^ [] : [-(relation_empty_yielding(353 ^ []))], (110 ^ _82989) ^ [_86562, _86564, _86566, _86568] : [-(apply(_86568, _86564) = apply(_86566, _86562)), _86568 = _86566, _86564 = _86562], (340 ^ _82989) ^ [] : [empty(338 ^ [])], (365 ^ _82989) ^ [_94028, _94030] : [relation(_94028), function(_94028), 372 ^ _82989 : [(373 ^ _82989) ^ [_94274] : [relation(_94274), function(_94274), in(_94030, relation_dom(_94028)), -(apply(relation_composition(_94028, _94274), _94030) = apply(_94274, apply(_94028, _94030)))]]], (20 ^ _82989) ^ [_83737, _83739] : [-(relation_empty_yielding(_83737)), _83739 = _83737, relation_empty_yielding(_83739)], (299 ^ _82989) ^ [_91967] : [empty(_91967), 302 ^ _82989 : [(305 ^ _82989) ^ [] : [-(relation(relation_rng(_91967)))], (303 ^ _82989) ^ [] : [-(empty(relation_rng(_91967)))]]], (190 ^ _82989) ^ [_88887] : [197 ^ _82989 : [(200 ^ _82989) ^ [] : [-(function(function_inverse(_88887)))], (198 ^ _82989) ^ [] : [-(relation(function_inverse(_88887)))]], relation(_88887), function(_88887)], (397 ^ _82989) ^ [_94997] : [relation(_94997), function(_94997), one_to_one(_94997), 408 ^ _82989 : [(409 ^ _82989) ^ [_95384] : [relation(_95384), function(_95384), 416 ^ _82989 : [(417 ^ _82989) ^ [] : [_95384 = function_inverse(_94997), 420 ^ _82989 : [(435 ^ _82989) ^ [_96275, _96277] : [442 ^ _82989 : [(445 ^ _82989) ^ [] : [-(_96275 = apply(_95384, _96277))], (443 ^ _82989) ^ [] : [-(in(_96277, relation_rng(_94997)))]], in(_96275, relation_dom(_94997)), _96277 = apply(_94997, _96275)], (423 ^ _82989) ^ [_95901, _95903] : [430 ^ _82989 : [(433 ^ _82989) ^ [] : [-(_95903 = apply(_94997, _95901))], (431 ^ _82989) ^ [] : [-(in(_95901, relation_dom(_94997)))]], in(_95903, relation_rng(_94997)), _95901 = apply(_95384, _95903)], (421 ^ _82989) ^ [] : [-(relation_dom(_95384) = relation_rng(_94997))]]], (447 ^ _82989) ^ [] : [-(_95384 = function_inverse(_94997)), relation_dom(_95384) = relation_rng(_94997), 456 ^ _82989 : [(461 ^ _82989) ^ [] : [in(453 ^ [_94997, _95384], relation_dom(_94997)), 452 ^ [_94997, _95384] = apply(_94997, 453 ^ [_94997, _95384])], (459 ^ _82989) ^ [] : [-(453 ^ [_94997, _95384] = apply(_95384, 452 ^ [_94997, _95384]))], (457 ^ _82989) ^ [] : [-(in(452 ^ [_94997, _95384], relation_rng(_94997)))]], 466 ^ _82989 : [(471 ^ _82989) ^ [] : [in(452 ^ [_94997, _95384], relation_rng(_94997)), 453 ^ [_94997, _95384] = apply(_95384, 452 ^ [_94997, _95384])], (469 ^ _82989) ^ [] : [-(452 ^ [_94997, _95384] = apply(_94997, 453 ^ [_94997, _95384]))], (467 ^ _82989) ^ [] : [-(in(453 ^ [_94997, _95384], relation_dom(_94997)))]]]]]]], (225 ^ _82989) ^ [_89796] : [-(element(223 ^ [_89796], _89796))], (342 ^ _82989) ^ [] : [-(relation(338 ^ []))], (148 ^ _82989) ^ [_87851] : [empty(_87851), -(relation(_87851))], (335 ^ _82989) ^ [] : [-(empty(331 ^ []))], (327 ^ _82989) ^ [] : [-(relation(323 ^ []))], (330 ^ _82989) ^ [] : [-(empty(328 ^ []))], (350 ^ _82989) ^ [] : [-(function(346 ^ []))], (4 ^ _82989) ^ [_83220, _83222] : [_83222 = _83220, -(_83220 = _83222)], (120 ^ _82989) ^ [_86921, _86923, _86925, _86927] : [-(relation_composition(_86927, _86923) = relation_composition(_86925, _86921)), _86927 = _86925, _86923 = _86921], (208 ^ _82989) ^ [_89368, _89370] : [-(relation(relation_composition(_89370, _89368))), relation(_89370), relation(_89368)], (265 ^ _82989) ^ [] : [-(empty(empty_set))], (325 ^ _82989) ^ [] : [-(empty(323 ^ []))], (243 ^ _82989) ^ [] : [-(relation_empty_yielding(empty_set))], (291 ^ _82989) ^ [_91702] : [empty(_91702), 294 ^ _82989 : [(297 ^ _82989) ^ [] : [-(relation(relation_dom(_91702)))], (295 ^ _82989) ^ [] : [-(empty(relation_dom(_91702)))]]]], input).
% 215.00/207.38 ncf('1',plain,[-(function(517 ^ []))],start(521 ^ 0)).
% 215.00/207.38 ncf('1.1',plain,[function(517 ^ []), 373 : relation(517 ^ []), 373 : in(516 ^ [], relation_dom(function_inverse(517 ^ []))), 373 : -(apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []) = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ []))), 373 : relation(function_inverse(517 ^ [])), 373 : function(function_inverse(517 ^ []))],extension(365 ^ 1,bind([[_94028, _94030, _94274], [function_inverse(517 ^ []), 516 ^ [], 517 ^ []]]))).
% 215.00/207.38 ncf('1.1.1',plain,[-(relation(517 ^ []))],extension(519 ^ 4)).
% 215.00/207.38 ncf('1.1.2',plain,[-(in(516 ^ [], relation_dom(function_inverse(517 ^ [])))), element(516 ^ [], relation_dom(function_inverse(517 ^ []))), -(empty(relation_dom(function_inverse(517 ^ []))))],extension(387 ^ 4,bind([[_94713, _94715], [relation_dom(function_inverse(517 ^ [])), 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1',plain,[-(element(516 ^ [], relation_dom(function_inverse(517 ^ [])))), element(516 ^ [], relation_rng(517 ^ [])), 516 ^ [] = 516 ^ [], relation_rng(517 ^ []) = relation_dom(function_inverse(517 ^ []))],extension(30 ^ 5,bind([[_84060, _84062, _84064, _84066], [relation_dom(function_inverse(517 ^ [])), relation_rng(517 ^ []), 516 ^ [], 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1.1',plain,[-(element(516 ^ [], relation_rng(517 ^ []))), element(516 ^ [], relation_rng(517 ^ [])), 516 ^ [] = 516 ^ [], relation_rng(517 ^ []) = relation_rng(517 ^ [])],extension(30 ^ 6,bind([[_84060, _84062, _84064, _84066], [relation_rng(517 ^ []), relation_rng(517 ^ []), 516 ^ [], 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1.1.1',plain,[-(element(516 ^ [], relation_rng(517 ^ []))), in(516 ^ [], relation_rng(517 ^ []))],extension(359 ^ 7,bind([[_93818, _93820], [relation_rng(517 ^ []), 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1.1.1.1',plain,[-(in(516 ^ [], relation_rng(517 ^ [])))],extension(525 ^ 8)).
% 215.00/207.38 ncf('1.1.2.1.1.2',plain,[-(516 ^ [] = 516 ^ [])],extension(2 ^ 7,bind([[_83113], [516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1.1.3',plain,[-(relation_rng(517 ^ []) = relation_rng(517 ^ []))],extension(2 ^ 7,bind([[_83113], [relation_rng(517 ^ [])]]))).
% 215.00/207.38 ncf('1.1.2.1.2',plain,[-(516 ^ [] = 516 ^ [])],extension(2 ^ 6,bind([[_83113], [516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1.3',plain,[-(relation_rng(517 ^ []) = relation_dom(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ []), one_to_one(517 ^ [])],extension(479 ^ 6,bind([[_97822], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.1.3.1',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.2.1.3.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.2.1.3.3',plain,[-(one_to_one(517 ^ []))],extension(523 ^ 7)).
% 215.00/207.38 ncf('1.1.2.2',plain,[empty(relation_dom(function_inverse(517 ^ []))), -(empty(relation_rng(517 ^ []))), relation_dom(function_inverse(517 ^ [])) = relation_rng(517 ^ [])],extension(44 ^ 5,bind([[_84476, _84478], [relation_rng(517 ^ []), relation_dom(function_inverse(517 ^ []))]]))).
% 215.00/207.38 ncf('1.1.2.2.1',plain,[empty(relation_rng(517 ^ [])), -(empty(relation_rng(517 ^ []))), relation_rng(517 ^ []) = relation_rng(517 ^ [])],extension(44 ^ 6,bind([[_84476, _84478], [relation_rng(517 ^ []), relation_rng(517 ^ [])]]))).
% 215.00/207.38 ncf('1.1.2.2.1.1',plain,[empty(relation_rng(517 ^ [])), in(516 ^ [], relation_rng(517 ^ []))],extension(501 ^ 7,bind([[_98477, _98479], [relation_rng(517 ^ []), 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.2.1.1.1',plain,[-(in(516 ^ [], relation_rng(517 ^ [])))],extension(525 ^ 8)).
% 215.00/207.38 ncf('1.1.2.2.1.2',plain,[-(relation_rng(517 ^ []) = relation_rng(517 ^ []))],extension(2 ^ 7,bind([[_83113], [relation_rng(517 ^ [])]]))).
% 215.00/207.38 ncf('1.1.2.2.2',plain,[-(relation_dom(function_inverse(517 ^ [])) = relation_rng(517 ^ [])), 417 : function_inverse(517 ^ []) = function_inverse(517 ^ []), 417 : relation(function_inverse(517 ^ [])), 417 : function(function_inverse(517 ^ [])), 409 : relation(517 ^ []), 409 : function(517 ^ []), 409 : one_to_one(517 ^ [])],extension(397 ^ 6,bind([[_94997, _95384], [517 ^ [], function_inverse(517 ^ [])]]))).
% 215.00/207.38 ncf('1.1.2.2.2.1',plain,[-(function_inverse(517 ^ []) = function_inverse(517 ^ []))],extension(2 ^ 11,bind([[_83113], [function_inverse(517 ^ [])]]))).
% 215.00/207.38 ncf('1.1.2.2.2.2',plain,[-(relation(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ [])],extension(190 ^ 9,bind([[_88887], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.2.2.2.1',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.2.2.2.2.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.2.2.2.3',plain,[-(function(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ [])],extension(190 ^ 9,bind([[_88887], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.2.2.2.3.1',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.2.2.2.3.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.2.2.2.4',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.2.2.2.5',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.2.2.2.6',plain,[-(one_to_one(517 ^ []))],extension(523 ^ 7)).
% 215.00/207.38 ncf('1.1.3',plain,[apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []) = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])), -(apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []) = 516 ^ []), apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])) = 516 ^ []],extension(10 ^ 4,bind([[_83424, _83426, _83428], [516 ^ [], apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])), apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ [])]]))).
% 215.00/207.38 ncf('1.1.3.1',plain,[apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []) = 516 ^ [], -(516 ^ [] = apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []))],extension(4 ^ 5,bind([[_83220, _83222], [516 ^ [], apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ [])]]))).
% 215.00/207.38 ncf('1.1.3.1.1',plain,[516 ^ [] = apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []), 516 ^ [] = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ []))],extension(527 ^ 6)).
% 215.00/207.38 ncf('1.1.3.1.1.1',plain,[-(516 ^ [] = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ []))), 516 ^ [] = apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []), apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []) = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ []))],extension(10 ^ 7,bind([[_83424, _83426, _83428], [apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])), apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []), 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.3.1.1.1.1',plain,[-(516 ^ [] = apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []))],reduction('1.1.3.1')).
% 215.00/207.38 ncf('1.1.3.1.1.1.2',plain,[-(apply(relation_composition(function_inverse(517 ^ []), 517 ^ []), 516 ^ []) = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])))],reduction('1.1')).
% 215.00/207.38 ncf('1.1.3.2',plain,[-(apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])) = 516 ^ []), 516 ^ [] = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ []))],extension(4 ^ 5,bind([[_83220, _83222], [apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ [])), 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.3.2.1',plain,[-(516 ^ [] = apply(517 ^ [], apply(function_inverse(517 ^ []), 516 ^ []))), 423 : in(516 ^ [], relation_rng(517 ^ [])), 423 : apply(function_inverse(517 ^ []), 516 ^ []) = apply(function_inverse(517 ^ []), 516 ^ []), 423 : function_inverse(517 ^ []) = function_inverse(517 ^ []), 417 : relation(function_inverse(517 ^ [])), 417 : function(function_inverse(517 ^ [])), 409 : relation(517 ^ []), 409 : function(517 ^ []), 409 : one_to_one(517 ^ [])],extension(397 ^ 6,bind([[_94997, _95384, _95901, _95903], [517 ^ [], function_inverse(517 ^ []), apply(function_inverse(517 ^ []), 516 ^ []), 516 ^ []]]))).
% 215.00/207.38 ncf('1.1.3.2.1.1',plain,[-(in(516 ^ [], relation_rng(517 ^ [])))],extension(525 ^ 13)).
% 215.00/207.38 ncf('1.1.3.2.1.2',plain,[-(apply(function_inverse(517 ^ []), 516 ^ []) = apply(function_inverse(517 ^ []), 516 ^ []))],extension(2 ^ 13,bind([[_83113], [apply(function_inverse(517 ^ []), 516 ^ [])]]))).
% 215.00/207.38 ncf('1.1.3.2.1.3',plain,[-(function_inverse(517 ^ []) = function_inverse(517 ^ []))],extension(2 ^ 11,bind([[_83113], [function_inverse(517 ^ [])]]))).
% 215.00/207.38 ncf('1.1.3.2.1.4',plain,[-(relation(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ [])],extension(190 ^ 9,bind([[_88887], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.3.2.1.4.1',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.3.2.1.4.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.3.2.1.5',plain,[-(function(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ [])],extension(190 ^ 9,bind([[_88887], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.3.2.1.5.1',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.3.2.1.5.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.3.2.1.6',plain,[-(relation(517 ^ []))],lemmata('[1].x')).
% 215.00/207.38 ncf('1.1.3.2.1.7',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.3.2.1.8',plain,[-(one_to_one(517 ^ []))],extension(523 ^ 7)).
% 215.00/207.38 ncf('1.1.4',plain,[-(relation(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ [])],extension(190 ^ 2,bind([[_88887], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.4.1',plain,[-(relation(517 ^ []))],extension(519 ^ 3)).
% 215.00/207.38 ncf('1.1.4.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 ncf('1.1.5',plain,[-(function(function_inverse(517 ^ []))), relation(517 ^ []), function(517 ^ [])],extension(190 ^ 2,bind([[_88887], [517 ^ []]]))).
% 215.00/207.38 ncf('1.1.5.1',plain,[-(relation(517 ^ []))],extension(519 ^ 3)).
% 215.00/207.38 ncf('1.1.5.2',plain,[-(function(517 ^ []))],reduction('1')).
% 215.00/207.38 %-----------------------------------------------------
% 215.00/207.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------