%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU040+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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:07 EDT 2023
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU040+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n008.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 12:30:24 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(399 ^ _57764) ^ [] : [-(relation(397 ^ []))], (401 ^ _57764) ^ [] : [-(function(397 ^ []))], (403 ^ _57764) ^ [] : [subset(relation_dom(relation_dom_restriction(397 ^ [], 396 ^ [])), relation_dom(397 ^ [])), subset(relation_rng(relation_dom_restriction(397 ^ [], 396 ^ [])), relation_rng(397 ^ []))], (112 ^ _57764) ^ [_61339, _61341] : [_61341 = _61339, -(powerset(_61341) = powerset(_61339))], (118 ^ _57764) ^ [_61557, _61559] : [_61559 = _61557, -(relation_dom(_61559) = relation_dom(_61557))], (134 ^ _57764) ^ [_62114, _62116] : [_62116 = _62114, -(relation_rng(_62116) = relation_rng(_62114))], (124 ^ _57764) ^ [_61803, _61805, _61807, _61809] : [-(relation_dom_restriction(_61809, _61805) = relation_dom_restriction(_61807, _61803)), _61809 = _61807, _61805 = _61803], (2 ^ _57764) ^ [_57908] : [-(_57908 = _57908)], (4 ^ _57764) ^ [_58015, _58017] : [_58017 = _58015, -(_58015 = _58017)], (10 ^ _57764) ^ [_58219, _58221, _58223] : [-(_58223 = _58219), _58223 = _58221, _58221 = _58219], (20 ^ _57764) ^ [_58560, _58562, _58564, _58566] : [-(in(_58564, _58560)), in(_58566, _58562), _58566 = _58564, _58562 = _58560], (34 ^ _57764) ^ [_58976, _58978] : [-(one_to_one(_58976)), _58978 = _58976, one_to_one(_58978)], (44 ^ _57764) ^ [_59271, _59273] : [-(relation_empty_yielding(_59271)), _59273 = _59271, relation_empty_yielding(_59273)], (54 ^ _57764) ^ [_59566, _59568] : [-(empty(_59566)), _59568 = _59566, empty(_59568)], (64 ^ _57764) ^ [_59889, _59891, _59893, _59895] : [-(element(_59893, _59889)), element(_59895, _59891), _59895 = _59893, _59891 = _59889], (78 ^ _57764) ^ [_60305, _60307] : [-(relation(_60305)), _60307 = _60305, relation(_60307)], (88 ^ _57764) ^ [_60600, _60602] : [-(function(_60600)), _60602 = _60600, function(_60602)], (98 ^ _57764) ^ [_60903, _60905, _60907, _60909] : [-(subset(_60907, _60903)), subset(_60909, _60905), _60909 = _60907, _60905 = _60903], (140 ^ _57764) ^ [_62346, _62348] : [in(_62348, _62346), in(_62346, _62348)], (146 ^ _57764) ^ [] : [-(empty(empty_set))], (148 ^ _57764) ^ [] : [-(relation(empty_set))], (150 ^ _57764) ^ [] : [-(empty(empty_set))], (152 ^ _57764) ^ [] : [-(relation(empty_set))], (154 ^ _57764) ^ [] : [-(relation_empty_yielding(empty_set))], (156 ^ _57764) ^ [] : [-(empty(empty_set))], (158 ^ _57764) ^ [_62881, _62883] : [in(_62883, _62881), -(element(_62883, _62881))], (164 ^ _57764) ^ [_63105, _63107, _63109] : [-(element(_63109, _63105)), in(_63109, _63107), element(_63107, powerset(_63105))], (174 ^ _57764) ^ [_63432, _63434, _63436] : [in(_63436, _63434), element(_63434, powerset(_63432)), empty(_63432)], (184 ^ _57764) ^ [_63742, _63744] : [empty(_63744), -(_63744 = _63742), empty(_63742)], (195 ^ _57764) ^ [_64049] : [-(element(193 ^ [_64049], _64049))], (197 ^ _57764) ^ [_64147] : [empty(_64147), -(function(_64147))], (203 ^ _57764) ^ [_64333] : [214 ^ _57764 : [(215 ^ _57764) ^ [] : [-(relation(_64333))], (217 ^ _57764) ^ [] : [-(function(_64333))], (219 ^ _57764) ^ [] : [-(one_to_one(_64333))]], relation(_64333), empty(_64333), function(_64333)], (221 ^ _57764) ^ [_64810] : [empty(powerset(_64810))], (223 ^ _57764) ^ [_64904] : [empty(relation_dom(_64904)), -(empty(_64904)), relation(_64904)], (233 ^ _57764) ^ [_65181] : [empty(relation_rng(_65181)), -(empty(_65181)), relation(_65181)], (243 ^ _57764) ^ [_65458] : [empty(_65458), 246 ^ _57764 : [(247 ^ _57764) ^ [] : [-(empty(relation_dom(_65458)))], (249 ^ _57764) ^ [] : [-(relation(relation_dom(_65458)))]]], (251 ^ _57764) ^ [_65723] : [empty(_65723), 254 ^ _57764 : [(255 ^ _57764) ^ [] : [-(empty(relation_rng(_65723)))], (257 ^ _57764) ^ [] : [-(relation(relation_rng(_65723)))]]], (259 ^ _57764) ^ [_66002, _66004] : [266 ^ _57764 : [(267 ^ _57764) ^ [] : [-(relation(relation_dom_restriction(_66004, _66002)))], (269 ^ _57764) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_66004, _66002)))]], relation(_66004), relation_empty_yielding(_66004)], (271 ^ _57764) ^ [_66366] : [empty(_66366), -(relation(_66366))], (277 ^ _57764) ^ [_66566, _66568] : [element(_66568, _66566), -(empty(_66566)), -(in(_66568, _66566))], (287 ^ _57764) ^ [_66850] : [empty(_66850), -(_66850 = empty_set)], (293 ^ _57764) ^ [_67052, _67054] : [in(_67054, _67052), empty(_67052)], (299 ^ _57764) ^ [_67244, _67246] : [-(subset(_67246, _67246))], (301 ^ _57764) ^ [_67353, _67355] : [relation(_67355), -(relation(relation_dom_restriction(_67355, _67353)))], (307 ^ _57764) ^ [_67565, _67567] : [314 ^ _57764 : [(315 ^ _57764) ^ [] : [-(relation(relation_dom_restriction(_67567, _67565)))], (317 ^ _57764) ^ [] : [-(function(relation_dom_restriction(_67567, _67565)))]], relation(_67567), function(_67567)], (320 ^ _57764) ^ [] : [-(relation(318 ^ []))], (322 ^ _57764) ^ [] : [-(function(318 ^ []))], (325 ^ _57764) ^ [] : [-(relation(323 ^ []))], (327 ^ _57764) ^ [] : [-(empty(323 ^ []))], (329 ^ _57764) ^ [] : [-(function(323 ^ []))], (332 ^ _57764) ^ [] : [-(relation(330 ^ []))], (334 ^ _57764) ^ [] : [-(function(330 ^ []))], (336 ^ _57764) ^ [] : [-(one_to_one(330 ^ []))], (338 ^ _57764) ^ [_68496] : [-(empty(_68496)), 342 ^ _57764 : [(343 ^ _57764) ^ [] : [-(element(341 ^ [_68496], powerset(_68496)))], (345 ^ _57764) ^ [] : [empty(341 ^ [_68496])]]], (348 ^ _57764) ^ [_68879] : [-(element(346 ^ [_68879], powerset(_68879)))], (350 ^ _57764) ^ [_68930] : [-(empty(346 ^ [_68930]))], (353 ^ _57764) ^ [] : [-(empty(351 ^ []))], (355 ^ _57764) ^ [] : [-(relation(351 ^ []))], (358 ^ _57764) ^ [] : [empty(356 ^ [])], (360 ^ _57764) ^ [] : [-(relation(356 ^ []))], (363 ^ _57764) ^ [] : [-(relation(361 ^ []))], (365 ^ _57764) ^ [] : [-(relation_empty_yielding(361 ^ []))], (368 ^ _57764) ^ [] : [-(empty(366 ^ []))], (371 ^ _57764) ^ [] : [empty(369 ^ [])], (373 ^ _57764) ^ [_69699, _69701] : [element(_69701, powerset(_69699)), -(subset(_69701, _69699))], (379 ^ _57764) ^ [_69865, _69867] : [subset(_69867, _69865), -(element(_69867, powerset(_69865)))], (385 ^ _57764) ^ [_70081, _70083] : [relation(_70081), -(subset(relation_dom(relation_dom_restriction(_70081, _70083)), relation_dom(_70081)))], (391 ^ _57764) ^ [_70283, _70285] : [relation(_70283), -(subset(relation_rng(relation_dom_restriction(_70283, _70285)), relation_rng(_70283)))]], input).
% 0.32/1.38 ncf('1',plain,[subset(relation_dom(relation_dom_restriction(397 ^ [], 396 ^ [])), relation_dom(397 ^ [])), subset(relation_rng(relation_dom_restriction(397 ^ [], 396 ^ [])), relation_rng(397 ^ []))],start(403 ^ 0)).
% 0.32/1.38 ncf('1.1',plain,[-(subset(relation_dom(relation_dom_restriction(397 ^ [], 396 ^ [])), relation_dom(397 ^ []))), relation(397 ^ [])],extension(385 ^ 1,bind([[_70081, _70083], [397 ^ [], 396 ^ []]]))).
% 0.32/1.38 ncf('1.1.1',plain,[-(relation(397 ^ []))],extension(399 ^ 2)).
% 0.32/1.38 ncf('1.2',plain,[-(subset(relation_rng(relation_dom_restriction(397 ^ [], 396 ^ [])), relation_rng(397 ^ []))), relation(397 ^ [])],extension(391 ^ 1,bind([[_70283, _70285], [397 ^ [], 396 ^ []]]))).
% 0.32/1.38 ncf('1.2.1',plain,[-(relation(397 ^ []))],extension(399 ^ 2)).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------