%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU224+1 : TPTP v8.1.2. Released v3.3.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:45 EDT 2023
% Result : Theorem 13.13s 13.67s
% Output : Proof 13.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.09 % Problem : SEU224+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.10 % 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.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Thu May 18 12:54:19 EDT 2023
% 0.09/0.29 % CPUTime :
% 13.13/13.67
% 13.13/13.67 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 13.13/13.67 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.13/13.67 %-----------------------------------------------------
% 13.13/13.67 ncf(matrix, plain, [(444 ^ _65617) ^ [] : [-(relation(442 ^ []))], (446 ^ _65617) ^ [] : [-(function(442 ^ []))], (448 ^ _65617) ^ [] : [457 ^ _65617 : [(458 ^ _65617) ^ [] : [-(in(441 ^ [], relation_dom(442 ^ [])))], (460 ^ _65617) ^ [] : [-(in(441 ^ [], 440 ^ []))], (462 ^ _65617) ^ [] : [in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])))]], 449 ^ _65617 : [(450 ^ _65617) ^ [] : [-(in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ []))))], (452 ^ _65617) ^ [] : [in(441 ^ [], relation_dom(442 ^ [])), in(441 ^ [], 440 ^ [])]]], (98 ^ _65617) ^ [_68774, _68776, _68778, _68780] : [-(set_intersection2(_68780, _68776) = set_intersection2(_68778, _68774)), _68780 = _68778, _68776 = _68774], (108 ^ _65617) ^ [_69133, _69135, _69137, _69139] : [-(apply(_69139, _69135) = apply(_69137, _69133)), _69139 = _69137, _69135 = _69133], (128 ^ _65617) ^ [_69803, _69805] : [_69805 = _69803, -(relation_dom(_69805) = relation_dom(_69803))], (118 ^ _65617) ^ [_69492, _69494, _69496, _69498] : [-(relation_dom_restriction(_69498, _69494) = relation_dom_restriction(_69496, _69492)), _69498 = _69496, _69494 = _69492], (2 ^ _65617) ^ [_65761] : [-(_65761 = _65761)], (4 ^ _65617) ^ [_65868, _65870] : [_65870 = _65868, -(_65868 = _65870)], (10 ^ _65617) ^ [_66072, _66074, _66076] : [-(_66076 = _66072), _66076 = _66074, _66074 = _66072], (20 ^ _65617) ^ [_66385, _66387] : [-(one_to_one(_66385)), _66387 = _66385, one_to_one(_66387)], (30 ^ _65617) ^ [_66680, _66682] : [-(relation_empty_yielding(_66680)), _66682 = _66680, relation_empty_yielding(_66682)], (40 ^ _65617) ^ [_67003, _67005, _67007, _67009] : [-(element(_67007, _67003)), element(_67009, _67005), _67009 = _67007, _67005 = _67003], (54 ^ _65617) ^ [_67419, _67421] : [-(empty(_67419)), _67421 = _67419, empty(_67421)], (64 ^ _65617) ^ [_67714, _67716] : [-(relation(_67714)), _67716 = _67714, relation(_67716)], (74 ^ _65617) ^ [_68009, _68011] : [-(function(_68009)), _68011 = _68009, function(_68011)], (84 ^ _65617) ^ [_68312, _68314, _68316, _68318] : [-(in(_68316, _68312)), in(_68318, _68314), _68318 = _68316, _68314 = _68312], (134 ^ _65617) ^ [_70035, _70037] : [in(_70037, _70035), in(_70035, _70037)], (140 ^ _65617) ^ [_70232] : [empty(_70232), -(function(_70232))], (146 ^ _65617) ^ [_70418] : [empty(_70418), -(relation(_70418))], (152 ^ _65617) ^ [_70604] : [163 ^ _65617 : [(164 ^ _65617) ^ [] : [-(relation(_70604))], (166 ^ _65617) ^ [] : [-(function(_70604))], (168 ^ _65617) ^ [] : [-(one_to_one(_70604))]], relation(_70604), empty(_70604), function(_70604)], (170 ^ _65617) ^ [_71096, _71098] : [-(set_intersection2(_71098, _71096) = set_intersection2(_71096, _71098))], (194 ^ _65617) ^ [_71979, _71981, _71983] : [-(_71979 = set_intersection2(_71983, _71981)), 206 ^ _65617 : [(207 ^ _65617) ^ [] : [-(in(195 ^ [_71979, _71981, _71983], _71983))], (209 ^ _65617) ^ [] : [-(in(195 ^ [_71979, _71981, _71983], _71981))], (211 ^ _65617) ^ [] : [in(195 ^ [_71979, _71981, _71983], _71979)]], 198 ^ _65617 : [(199 ^ _65617) ^ [] : [-(in(195 ^ [_71979, _71981, _71983], _71979))], (201 ^ _65617) ^ [] : [in(195 ^ [_71979, _71981, _71983], _71983), in(195 ^ [_71979, _71981, _71983], _71981)]]], (172 ^ _65617) ^ [_71254, _71256, _71258] : [_71254 = set_intersection2(_71258, _71256), 175 ^ _65617 : [(176 ^ _65617) ^ [_71436] : [in(_71436, _71254), 179 ^ _65617 : [(180 ^ _65617) ^ [] : [-(in(_71436, _71258))], (182 ^ _65617) ^ [] : [-(in(_71436, _71256))]]], (184 ^ _65617) ^ [_71695] : [-(in(_71695, _71254)), in(_71695, _71258), in(_71695, _71256)]]], (215 ^ _65617) ^ [] : [true___, -(true___)], (221 ^ _65617) ^ [] : [true___, -(true___)], (227 ^ _65617) ^ [] : [true___, -(true___)], (233 ^ _65617) ^ [] : [true___, -(true___)], (239 ^ _65617) ^ [_73208, _73210] : [relation(_73210), -(relation(relation_dom_restriction(_73210, _73208)))], (245 ^ _65617) ^ [] : [true___, -(true___)], (252 ^ _65617) ^ [_73549] : [-(element(250 ^ [_73549], _73549))], (254 ^ _65617) ^ [] : [-(empty(empty_set))], (256 ^ _65617) ^ [] : [-(relation(empty_set))], (258 ^ _65617) ^ [] : [-(relation_empty_yielding(empty_set))], (260 ^ _65617) ^ [_73824, _73826] : [267 ^ _65617 : [(268 ^ _65617) ^ [] : [-(relation(relation_dom_restriction(_73826, _73824)))], (270 ^ _65617) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_73826, _73824)))]], relation(_73826), relation_empty_yielding(_73826)], (272 ^ _65617) ^ [_74202, _74204] : [-(relation(set_intersection2(_74204, _74202))), relation(_74204), relation(_74202)], (282 ^ _65617) ^ [] : [-(empty(empty_set))], (284 ^ _65617) ^ [_74554, _74556] : [291 ^ _65617 : [(292 ^ _65617) ^ [] : [-(relation(relation_dom_restriction(_74556, _74554)))], (294 ^ _65617) ^ [] : [-(function(relation_dom_restriction(_74556, _74554)))]], relation(_74556), function(_74556)], (296 ^ _65617) ^ [] : [-(empty(empty_set))], (298 ^ _65617) ^ [] : [-(relation(empty_set))], (300 ^ _65617) ^ [_75026] : [empty(relation_dom(_75026)), -(empty(_75026)), relation(_75026)], (310 ^ _65617) ^ [_75303] : [empty(_75303), 313 ^ _65617 : [(314 ^ _65617) ^ [] : [-(empty(relation_dom(_75303)))], (316 ^ _65617) ^ [] : [-(relation(relation_dom(_75303)))]]], (318 ^ _65617) ^ [_75567, _75569] : [-(set_intersection2(_75569, _75569) = _75569)], (321 ^ _65617) ^ [] : [-(relation(319 ^ []))], (323 ^ _65617) ^ [] : [-(function(319 ^ []))], (326 ^ _65617) ^ [] : [-(empty(324 ^ []))], (328 ^ _65617) ^ [] : [-(relation(324 ^ []))], (331 ^ _65617) ^ [] : [-(empty(329 ^ []))], (334 ^ _65617) ^ [] : [-(relation(332 ^ []))], (336 ^ _65617) ^ [] : [-(empty(332 ^ []))], (338 ^ _65617) ^ [] : [-(function(332 ^ []))], (341 ^ _65617) ^ [] : [empty(339 ^ [])], (343 ^ _65617) ^ [] : [-(relation(339 ^ []))], (346 ^ _65617) ^ [] : [empty(344 ^ [])], (349 ^ _65617) ^ [] : [-(relation(347 ^ []))], (351 ^ _65617) ^ [] : [-(function(347 ^ []))], (353 ^ _65617) ^ [] : [-(one_to_one(347 ^ []))], (356 ^ _65617) ^ [] : [-(relation(354 ^ []))], (358 ^ _65617) ^ [] : [-(relation_empty_yielding(354 ^ []))], (360 ^ _65617) ^ [_76873, _76875] : [in(_76875, _76873), -(element(_76875, _76873))], (366 ^ _65617) ^ [_77054] : [-(set_intersection2(_77054, empty_set) = empty_set)], (368 ^ _65617) ^ [_77164, _77166] : [element(_77166, _77164), -(empty(_77164)), -(in(_77166, _77164))], (419 ^ _65617) ^ [_78837] : [empty(_78837), -(_78837 = empty_set)], (425 ^ _65617) ^ [_79039, _79041] : [in(_79041, _79039), empty(_79039)], (431 ^ _65617) ^ [_79226, _79228] : [empty(_79228), -(_79228 = _79226), empty(_79226)], (378 ^ _65617) ^ [_77462, _77464] : [relation(_77462), function(_77462), 385 ^ _65617 : [(386 ^ _65617) ^ [_77729] : [relation(_77729), function(_77729), 393 ^ _65617 : [(394 ^ _65617) ^ [] : [_77462 = relation_dom_restriction(_77729, _77464), 397 ^ _65617 : [(398 ^ _65617) ^ [] : [-(relation_dom(_77462) = set_intersection2(relation_dom(_77729), _77464))], (400 ^ _65617) ^ [_78183] : [in(_78183, relation_dom(_77462)), -(apply(_77462, _78183) = apply(_77729, _78183))]]], (406 ^ _65617) ^ [] : [-(_77462 = relation_dom_restriction(_77729, _77464)), relation_dom(_77462) = set_intersection2(relation_dom(_77729), _77464), 412 ^ _65617 : [(413 ^ _65617) ^ [] : [-(in(411 ^ [_77462, _77464, _77729], relation_dom(_77462)))], (415 ^ _65617) ^ [] : [apply(_77462, 411 ^ [_77462, _77464, _77729]) = apply(_77729, 411 ^ [_77462, _77464, _77729])]]]]]]]], input).
% 13.13/13.67 ncf('1',plain,[462 : in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ []))), 452 : in(441 ^ [], relation_dom(442 ^ [])), 452 : in(441 ^ [], 440 ^ [])],start(448 ^ 0)).
% 13.13/13.67 ncf('1.1',plain,[-(in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])))), 184 : in(441 ^ [], relation_dom(442 ^ [])), 184 : in(441 ^ [], 440 ^ []), 184 : relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])) = set_intersection2(relation_dom(442 ^ []), 440 ^ [])],extension(172 ^ 3,bind([[_71254, _71256, _71258, _71695], [relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])), 440 ^ [], relation_dom(442 ^ []), 441 ^ []]]))).
% 13.13/13.67 ncf('1.1.1',plain,[-(in(441 ^ [], relation_dom(442 ^ [])))],extension(458 ^ 6)).
% 13.13/13.67 ncf('1.1.2',plain,[-(in(441 ^ [], 440 ^ []))],extension(460 ^ 6)).
% 13.13/13.67 ncf('1.1.3',plain,[-(relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])) = set_intersection2(relation_dom(442 ^ []), 440 ^ [])), 394 : relation_dom_restriction(442 ^ [], 440 ^ []) = relation_dom_restriction(442 ^ [], 440 ^ []), 394 : relation(442 ^ []), 394 : function(442 ^ []), 386 : relation(relation_dom_restriction(442 ^ [], 440 ^ [])), 386 : function(relation_dom_restriction(442 ^ [], 440 ^ []))],extension(378 ^ 4,bind([[_77462, _77464, _77729], [relation_dom_restriction(442 ^ [], 440 ^ []), 440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.1.3.1',plain,[-(relation_dom_restriction(442 ^ [], 440 ^ []) = relation_dom_restriction(442 ^ [], 440 ^ []))],extension(2 ^ 9,bind([[_65761], [relation_dom_restriction(442 ^ [], 440 ^ [])]]))).
% 13.13/13.67 ncf('1.1.3.2',plain,[-(relation(442 ^ []))],extension(444 ^ 7)).
% 13.13/13.67 ncf('1.1.3.3',plain,[-(function(442 ^ []))],extension(446 ^ 7)).
% 13.13/13.67 ncf('1.1.3.4',plain,[-(relation(relation_dom_restriction(442 ^ [], 440 ^ []))), relation(442 ^ [])],extension(239 ^ 5,bind([[_73208, _73210], [440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.1.3.4.1',plain,[-(relation(442 ^ []))],extension(444 ^ 6)).
% 13.13/13.67 ncf('1.1.3.5',plain,[-(function(relation_dom_restriction(442 ^ [], 440 ^ []))), relation(442 ^ []), function(442 ^ [])],extension(284 ^ 5,bind([[_74554, _74556], [440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.1.3.5.1',plain,[-(relation(442 ^ []))],extension(444 ^ 6)).
% 13.13/13.67 ncf('1.1.3.5.2',plain,[-(function(442 ^ []))],extension(446 ^ 6)).
% 13.13/13.67 ncf('1.2',plain,[-(in(441 ^ [], relation_dom(442 ^ []))), 176 : in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ []))), 176 : relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])) = set_intersection2(relation_dom(442 ^ []), 440 ^ [])],extension(172 ^ 3,bind([[_71254, _71256, _71258, _71436], [relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])), 440 ^ [], relation_dom(442 ^ []), 441 ^ []]]))).
% 13.13/13.67 ncf('1.2.1',plain,[-(in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ []))))],extension(450 ^ 6)).
% 13.13/13.67 ncf('1.2.2',plain,[-(relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])) = set_intersection2(relation_dom(442 ^ []), 440 ^ [])), 394 : relation_dom_restriction(442 ^ [], 440 ^ []) = relation_dom_restriction(442 ^ [], 440 ^ []), 394 : relation(442 ^ []), 394 : function(442 ^ []), 386 : relation(relation_dom_restriction(442 ^ [], 440 ^ [])), 386 : function(relation_dom_restriction(442 ^ [], 440 ^ []))],extension(378 ^ 4,bind([[_77462, _77464, _77729], [relation_dom_restriction(442 ^ [], 440 ^ []), 440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.2.2.1',plain,[-(relation_dom_restriction(442 ^ [], 440 ^ []) = relation_dom_restriction(442 ^ [], 440 ^ []))],extension(2 ^ 9,bind([[_65761], [relation_dom_restriction(442 ^ [], 440 ^ [])]]))).
% 13.13/13.67 ncf('1.2.2.2',plain,[-(relation(442 ^ []))],extension(444 ^ 7)).
% 13.13/13.67 ncf('1.2.2.3',plain,[-(function(442 ^ []))],extension(446 ^ 7)).
% 13.13/13.67 ncf('1.2.2.4',plain,[-(relation(relation_dom_restriction(442 ^ [], 440 ^ []))), relation(442 ^ [])],extension(239 ^ 5,bind([[_73208, _73210], [440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.2.2.4.1',plain,[-(relation(442 ^ []))],extension(444 ^ 6)).
% 13.13/13.67 ncf('1.2.2.5',plain,[-(function(relation_dom_restriction(442 ^ [], 440 ^ []))), relation(442 ^ []), function(442 ^ [])],extension(284 ^ 5,bind([[_74554, _74556], [440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.2.2.5.1',plain,[-(relation(442 ^ []))],extension(444 ^ 6)).
% 13.13/13.67 ncf('1.2.2.5.2',plain,[-(function(442 ^ []))],extension(446 ^ 6)).
% 13.13/13.67 ncf('1.3',plain,[-(in(441 ^ [], 440 ^ [])), 176 : in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ []))), 176 : relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])) = set_intersection2(relation_dom(442 ^ []), 440 ^ [])],extension(172 ^ 3,bind([[_71254, _71256, _71258, _71436], [relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])), 440 ^ [], relation_dom(442 ^ []), 441 ^ []]]))).
% 13.13/13.67 ncf('1.3.1',plain,[-(in(441 ^ [], relation_dom(relation_dom_restriction(442 ^ [], 440 ^ []))))],extension(450 ^ 6)).
% 13.13/13.67 ncf('1.3.2',plain,[-(relation_dom(relation_dom_restriction(442 ^ [], 440 ^ [])) = set_intersection2(relation_dom(442 ^ []), 440 ^ [])), 394 : relation_dom_restriction(442 ^ [], 440 ^ []) = relation_dom_restriction(442 ^ [], 440 ^ []), 394 : relation(442 ^ []), 394 : function(442 ^ []), 386 : relation(relation_dom_restriction(442 ^ [], 440 ^ [])), 386 : function(relation_dom_restriction(442 ^ [], 440 ^ []))],extension(378 ^ 4,bind([[_77462, _77464, _77729], [relation_dom_restriction(442 ^ [], 440 ^ []), 440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.3.2.1',plain,[-(relation_dom_restriction(442 ^ [], 440 ^ []) = relation_dom_restriction(442 ^ [], 440 ^ []))],extension(2 ^ 9,bind([[_65761], [relation_dom_restriction(442 ^ [], 440 ^ [])]]))).
% 13.13/13.67 ncf('1.3.2.2',plain,[-(relation(442 ^ []))],extension(444 ^ 7)).
% 13.13/13.67 ncf('1.3.2.3',plain,[-(function(442 ^ []))],extension(446 ^ 7)).
% 13.13/13.67 ncf('1.3.2.4',plain,[-(relation(relation_dom_restriction(442 ^ [], 440 ^ []))), relation(442 ^ [])],extension(239 ^ 5,bind([[_73208, _73210], [440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.3.2.4.1',plain,[-(relation(442 ^ []))],extension(444 ^ 6)).
% 13.13/13.67 ncf('1.3.2.5',plain,[-(function(relation_dom_restriction(442 ^ [], 440 ^ []))), relation(442 ^ []), function(442 ^ [])],extension(284 ^ 5,bind([[_74554, _74556], [440 ^ [], 442 ^ []]]))).
% 13.13/13.67 ncf('1.3.2.5.1',plain,[-(relation(442 ^ []))],extension(444 ^ 6)).
% 13.13/13.67 ncf('1.3.2.5.2',plain,[-(function(442 ^ []))],extension(446 ^ 6)).
% 13.13/13.67 %-----------------------------------------------------
% 13.13/13.67 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------