%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET991+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:56:47 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SET991+1 : TPTP v8.1.2. Released v3.2.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n021.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 19:17:42 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(368 ^ _51061) ^ [] : [-(relation(366 ^ []))], (370 ^ _51061) ^ [] : [-(function(366 ^ []))], (372 ^ _51061) ^ [] : [-(in(365 ^ [], relation_dom(366 ^ [])))], (374 ^ _51061) ^ [] : [in(apply(366 ^ [], 365 ^ []), relation_rng(366 ^ []))], (102 ^ _51061) ^ [_54339, _54341] : [_54341 = _54339, -(powerset(_54341) = powerset(_54339))], (108 ^ _51061) ^ [_54557, _54559] : [_54559 = _54557, -(relation_dom(_54559) = relation_dom(_54557))], (124 ^ _51061) ^ [_55114, _55116] : [_55116 = _55114, -(relation_rng(_55116) = relation_rng(_55114))], (114 ^ _51061) ^ [_54803, _54805, _54807, _54809] : [-(apply(_54809, _54805) = apply(_54807, _54803)), _54809 = _54807, _54805 = _54803], (2 ^ _51061) ^ [_51205] : [-(_51205 = _51205)], (4 ^ _51061) ^ [_51312, _51314] : [_51314 = _51312, -(_51312 = _51314)], (10 ^ _51061) ^ [_51516, _51518, _51520] : [-(_51520 = _51516), _51520 = _51518, _51518 = _51516], (20 ^ _51061) ^ [_51857, _51859, _51861, _51863] : [-(subset(_51861, _51857)), subset(_51863, _51859), _51863 = _51861, _51859 = _51857], (34 ^ _51061) ^ [_52273, _52275] : [-(relation_empty_yielding(_52273)), _52275 = _52273, relation_empty_yielding(_52275)], (44 ^ _51061) ^ [_52596, _52598, _52600, _52602] : [-(element(_52600, _52596)), element(_52602, _52598), _52602 = _52600, _52598 = _52596], (58 ^ _51061) ^ [_53012, _53014] : [-(empty(_53012)), _53014 = _53012, empty(_53014)], (68 ^ _51061) ^ [_53307, _53309] : [-(relation(_53307)), _53309 = _53307, relation(_53309)], (78 ^ _51061) ^ [_53602, _53604] : [-(function(_53602)), _53604 = _53602, function(_53604)], (88 ^ _51061) ^ [_53905, _53907, _53909, _53911] : [-(in(_53909, _53905)), in(_53911, _53907), _53911 = _53909, _53907 = _53905], (130 ^ _51061) ^ [_55331, _55333] : [-(subset(_55333, _55333))], (132 ^ _51061) ^ [] : [-(empty(empty_set))], (134 ^ _51061) ^ [] : [-(relation(empty_set))], (136 ^ _51061) ^ [] : [-(empty(empty_set))], (138 ^ _51061) ^ [] : [-(relation(empty_set))], (140 ^ _51061) ^ [] : [-(relation_empty_yielding(empty_set))], (142 ^ _51061) ^ [] : [-(empty(empty_set))], (145 ^ _51061) ^ [_55774] : [-(element(143 ^ [_55774], _55774))], (147 ^ _51061) ^ [_55872] : [empty(_55872), -(function(_55872))], (153 ^ _51061) ^ [_56042] : [empty(powerset(_56042))], (155 ^ _51061) ^ [_56136] : [empty(relation_dom(_56136)), -(empty(_56136)), relation(_56136)], (165 ^ _51061) ^ [_56413] : [empty(relation_rng(_56413)), -(empty(_56413)), relation(_56413)], (175 ^ _51061) ^ [_56690] : [empty(_56690), 178 ^ _51061 : [(179 ^ _51061) ^ [] : [-(empty(relation_dom(_56690)))], (181 ^ _51061) ^ [] : [-(relation(relation_dom(_56690)))]]], (183 ^ _51061) ^ [_56955] : [empty(_56955), 186 ^ _51061 : [(187 ^ _51061) ^ [] : [-(empty(relation_rng(_56955)))], (189 ^ _51061) ^ [] : [-(relation(relation_rng(_56955)))]]], (191 ^ _51061) ^ [_57220] : [empty(_57220), -(relation(_57220))], (197 ^ _51061) ^ [_57420, _57422] : [element(_57422, _57420), -(empty(_57420)), -(in(_57422, _57420))], (207 ^ _51061) ^ [_57747, _57749] : [element(_57749, powerset(_57747)), -(subset(_57749, _57747))], (213 ^ _51061) ^ [_57913, _57915] : [subset(_57915, _57913), -(element(_57915, powerset(_57913)))], (219 ^ _51061) ^ [_58143, _58145, _58147] : [-(element(_58147, _58143)), in(_58147, _58145), element(_58145, powerset(_58143))], (229 ^ _51061) ^ [_58470, _58472, _58474] : [in(_58474, _58472), element(_58472, powerset(_58470)), empty(_58470)], (239 ^ _51061) ^ [_58766] : [empty(_58766), -(_58766 = empty_set)], (245 ^ _51061) ^ [_58968, _58970] : [empty(_58970), -(_58970 = _58968), empty(_58968)], (255 ^ _51061) ^ [_59265, _59267] : [in(_59267, _59265), in(_59265, _59267)], (262 ^ _51061) ^ [] : [-(relation(260 ^ []))], (264 ^ _51061) ^ [] : [-(function(260 ^ []))], (266 ^ _51061) ^ [_59611] : [-(empty(_59611)), 270 ^ _51061 : [(271 ^ _51061) ^ [] : [-(element(269 ^ [_59611], powerset(_59611)))], (273 ^ _51061) ^ [] : [empty(269 ^ [_59611])]]], (276 ^ _51061) ^ [_59994] : [-(element(274 ^ [_59994], powerset(_59994)))], (278 ^ _51061) ^ [_60045] : [-(empty(274 ^ [_60045]))], (281 ^ _51061) ^ [] : [-(empty(279 ^ []))], (283 ^ _51061) ^ [] : [-(relation(279 ^ []))], (286 ^ _51061) ^ [] : [empty(284 ^ [])], (288 ^ _51061) ^ [] : [-(relation(284 ^ []))], (291 ^ _51061) ^ [] : [-(relation(289 ^ []))], (293 ^ _51061) ^ [] : [-(relation_empty_yielding(289 ^ []))], (296 ^ _51061) ^ [] : [-(empty(294 ^ []))], (299 ^ _51061) ^ [] : [empty(297 ^ [])], (301 ^ _51061) ^ [_60785, _60787] : [in(_60787, _60785), -(element(_60787, _60785))], (307 ^ _51061) ^ [_60995, _60997] : [in(_60997, _60995), empty(_60995)], (313 ^ _51061) ^ [_61168] : [relation(_61168), function(_61168), 320 ^ _51061 : [(344 ^ _51061) ^ [_62322] : [-(_62322 = relation_rng(_61168)), 357 ^ _51061 : [(358 ^ _51061) ^ [] : [-(in(356 ^ [_61168, _62322], relation_dom(_61168)))], (360 ^ _51061) ^ [] : [-(345 ^ [_61168, _62322] = apply(_61168, 356 ^ [_61168, _62322]))], (362 ^ _51061) ^ [] : [in(345 ^ [_61168, _62322], _62322)]], 348 ^ _51061 : [(349 ^ _51061) ^ [] : [-(in(345 ^ [_61168, _62322], _62322))], (351 ^ _51061) ^ [_62617] : [in(_62617, relation_dom(_61168)), 345 ^ [_61168, _62322] = apply(_61168, _62617)]]], (321 ^ _51061) ^ [_61440] : [_61440 = relation_rng(_61168), 324 ^ _51061 : [(325 ^ _51061) ^ [_61628] : [in(_61628, _61440), 329 ^ _51061 : [(330 ^ _51061) ^ [] : [-(in(328 ^ [_61168, _61440, _61628], relation_dom(_61168)))], (332 ^ _51061) ^ [] : [-(_61628 = apply(_61168, 328 ^ [_61168, _61440, _61628]))]]], (334 ^ _51061) ^ [_61970] : [-(in(_61970, _61440)), 335 ^ _51061 : [(336 ^ _51061) ^ [_62073] : [in(_62073, relation_dom(_61168)), _61970 = apply(_61168, _62073)]]]]]]]], input).
% 0.33/1.37 ncf('1',plain,[in(apply(366 ^ [], 365 ^ []), relation_rng(366 ^ []))],start(374 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(in(apply(366 ^ [], 365 ^ []), relation_rng(366 ^ []))), 336 : in(365 ^ [], relation_dom(366 ^ [])), 336 : apply(366 ^ [], 365 ^ []) = apply(366 ^ [], 365 ^ []), 334 : relation_rng(366 ^ []) = relation_rng(366 ^ []), 321 : relation(366 ^ []), 321 : function(366 ^ [])],extension(313 ^ 1,bind([[_61168, _61440, _61970, _62073], [366 ^ [], relation_rng(366 ^ []), apply(366 ^ [], 365 ^ []), 365 ^ []]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(in(365 ^ [], relation_dom(366 ^ [])))],extension(372 ^ 8)).
% 0.33/1.37 ncf('1.1.2',plain,[-(apply(366 ^ [], 365 ^ []) = apply(366 ^ [], 365 ^ []))],extension(2 ^ 8,bind([[_51205], [apply(366 ^ [], 365 ^ [])]]))).
% 0.33/1.37 ncf('1.1.3',plain,[-(relation_rng(366 ^ []) = relation_rng(366 ^ []))],extension(2 ^ 4,bind([[_51205], [relation_rng(366 ^ [])]]))).
% 0.33/1.37 ncf('1.1.4',plain,[-(relation(366 ^ []))],extension(368 ^ 2)).
% 0.33/1.37 ncf('1.1.5',plain,[-(function(366 ^ []))],extension(370 ^ 2)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------