%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET064+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:55:16 EDT 2023
% Result : Theorem 0.22s 1.33s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.10 % Problem : SET064+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.10/0.11 % Command : nanocop.sh %s %d
% 0.10/0.30 % Computer : n006.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Thu May 18 19:02:06 EDT 2023
% 0.10/0.30 % CPUTime :
% 0.22/1.33
% 0.22/1.33 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.22/1.33 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/1.33 %-----------------------------------------------------
% 0.22/1.33 ncf(matrix, plain, [(714 ^ _103007) ^ [] : [712 ^ [] = null_class], (716 ^ _103007) ^ [_128286] : [member(_128286, 712 ^ [])], (2 ^ _103007) ^ [_103151] : [-(_103151 = _103151)], (4 ^ _103007) ^ [_103258, _103260] : [_103260 = _103258, -(_103258 = _103260)], (10 ^ _103007) ^ [_103462, _103464, _103466] : [-(_103466 = _103462), _103466 = _103464, _103464 = _103462], (20 ^ _103007) ^ [_103775, _103777] : [-(inductive(_103775)), _103777 = _103775, inductive(_103777)], (30 ^ _103007) ^ [_104098, _104100, _104102, _104104] : [-(subclass(_104102, _104098)), subclass(_104104, _104100), _104104 = _104102, _104100 = _104098], (44 ^ _103007) ^ [_104542, _104544, _104546, _104548] : [-(disjoint(_104546, _104542)), disjoint(_104548, _104544), _104548 = _104546, _104544 = _104542], (58 ^ _103007) ^ [_104958, _104960] : [-(function(_104958)), _104960 = _104958, function(_104960)], (68 ^ _103007) ^ [_105261, _105263, _105265, _105267] : [-(member(_105265, _105261)), member(_105267, _105263), _105267 = _105265, _105263 = _105261], (82 ^ _103007) ^ [_105719, _105721, _105723, _105725] : [-(unordered_pair(_105725, _105721) = unordered_pair(_105723, _105719)), _105725 = _105723, _105721 = _105719], (92 ^ _103007) ^ [_106050, _106052] : [_106052 = _106050, -(first(_106052) = first(_106050))], (98 ^ _103007) ^ [_106268, _106270] : [_106270 = _106268, -(second(_106270) = second(_106268))], (104 ^ _103007) ^ [_106486, _106488] : [_106488 = _106486, -(complement(_106488) = complement(_106486))], (110 ^ _103007) ^ [_106732, _106734, _106736, _106738] : [-(intersection(_106738, _106734) = intersection(_106736, _106732)), _106738 = _106736, _106734 = _106732], (120 ^ _103007) ^ [_107063, _107065] : [_107065 = _107063, -(rotate(_107065) = rotate(_107063))], (126 ^ _103007) ^ [_107309, _107311, _107313, _107315] : [-(union(_107315, _107311) = union(_107313, _107309)), _107315 = _107313, _107311 = _107309], (136 ^ _103007) ^ [_107640, _107642] : [_107642 = _107640, -(successor(_107642) = successor(_107640))], (142 ^ _103007) ^ [_107858, _107860] : [_107860 = _107858, -(flip(_107860) = flip(_107858))], (148 ^ _103007) ^ [_108076, _108078] : [_108078 = _108076, -(domain_of(_108078) = domain_of(_108076))], (154 ^ _103007) ^ [_108294, _108296] : [_108296 = _108294, -(range_of(_108296) = range_of(_108294))], (160 ^ _103007) ^ [_108568, _108570, _108572, _108574, _108576, _108578] : [-(restrict(_108578, _108574, _108570) = restrict(_108576, _108572, _108568)), _108578 = _108576, _108574 = _108572, _108570 = _108568], (174 ^ _103007) ^ [_109028, _109030] : [_109030 = _109028, -(power_class(_109030) = power_class(_109028))], (180 ^ _103007) ^ [_109274, _109276, _109278, _109280] : [-(ordered_pair(_109280, _109276) = ordered_pair(_109278, _109274)), _109280 = _109278, _109276 = _109274], (190 ^ _103007) ^ [_109633, _109635, _109637, _109639] : [-(cross_product(_109639, _109635) = cross_product(_109637, _109633)), _109639 = _109637, _109635 = _109633], (200 ^ _103007) ^ [_109992, _109994, _109996, _109998] : [-(compose(_109998, _109994) = compose(_109996, _109992)), _109998 = _109996, _109994 = _109992], (210 ^ _103007) ^ [_110323, _110325] : [_110325 = _110323, -(inverse(_110325) = inverse(_110323))], (216 ^ _103007) ^ [_110541, _110543] : [_110543 = _110541, -(sum_class(_110543) = sum_class(_110541))], (222 ^ _103007) ^ [_110787, _110789, _110791, _110793] : [-(image(_110793, _110789) = image(_110791, _110787)), _110793 = _110791, _110789 = _110787], (232 ^ _103007) ^ [_111118, _111120] : [_111120 = _111118, -(singleton(_111120) = singleton(_111118))], (238 ^ _103007) ^ [_111344, _111346, _111348, _111350] : [-(apply(_111350, _111346) = apply(_111348, _111344)), _111350 = _111348, _111346 = _111344], (258 ^ _103007) ^ [_112106, _112108] : [260 ^ _103007 : [(261 ^ _103007) ^ [] : [-(member(259 ^ [_112106, _112108], _112108))], (263 ^ _103007) ^ [] : [member(259 ^ [_112106, _112108], _112106)]], -(subclass(_112108, _112106))], (248 ^ _103007) ^ [_111792, _111794] : [subclass(_111794, _111792), 251 ^ _103007 : [(252 ^ _103007) ^ [_111929] : [member(_111929, _111794), -(member(_111929, _111792))]]], (267 ^ _103007) ^ [_112434] : [-(subclass(_112434, universal_class))], (269 ^ _103007) ^ [_112570, _112572] : [_112572 = _112570, 272 ^ _103007 : [(273 ^ _103007) ^ [] : [-(subclass(_112572, _112570))], (275 ^ _103007) ^ [] : [-(subclass(_112570, _112572))]]], (277 ^ _103007) ^ [_112807, _112809] : [-(_112809 = _112807), subclass(_112809, _112807), subclass(_112807, _112809)], (287 ^ _103007) ^ [_113151, _113153, _113155] : [member(_113155, unordered_pair(_113153, _113151)), 290 ^ _103007 : [(291 ^ _103007) ^ [] : [-(member(_113155, universal_class))], (293 ^ _103007) ^ [] : [-(_113155 = _113153), -(_113155 = _113151)]]], (299 ^ _103007) ^ [_113496, _113498, _113500] : [-(member(_113500, unordered_pair(_113498, _113496))), member(_113500, universal_class), 304 ^ _103007 : [(305 ^ _103007) ^ [] : [_113500 = _113498], (307 ^ _103007) ^ [] : [_113500 = _113496]]], (311 ^ _103007) ^ [_113874, _113876] : [-(member(unordered_pair(_113876, _113874), universal_class))], (313 ^ _103007) ^ [_113957] : [-(singleton(_113957) = unordered_pair(_113957, _113957))], (315 ^ _103007) ^ [_114054, _114056] : [-(ordered_pair(_114056, _114054) = unordered_pair(singleton(_114056), unordered_pair(_114056, singleton(_114054))))], (317 ^ _103007) ^ [_114233, _114235, _114237, _114239] : [member(ordered_pair(_114239, _114237), cross_product(_114235, _114233)), 320 ^ _103007 : [(321 ^ _103007) ^ [] : [-(member(_114239, _114235))], (323 ^ _103007) ^ [] : [-(member(_114237, _114233))]]], (325 ^ _103007) ^ [_114498, _114500, _114502, _114504] : [-(member(ordered_pair(_114504, _114502), cross_product(_114500, _114498))), member(_114504, _114500), member(_114502, _114498)], (335 ^ _103007) ^ [_114831, _114833] : [342 ^ _103007 : [(343 ^ _103007) ^ [] : [-(first(ordered_pair(_114833, _114831)) = _114833)], (345 ^ _103007) ^ [] : [-(second(ordered_pair(_114833, _114831)) = _114831)]], member(_114833, universal_class), member(_114831, universal_class)], (347 ^ _103007) ^ [_115239, _115241, _115243] : [member(_115239, cross_product(_115243, _115241)), -(_115239 = ordered_pair(first(_115239), second(_115239)))], (353 ^ _103007) ^ [_115504, _115506] : [member(ordered_pair(_115506, _115504), element_relation), 356 ^ _103007 : [(357 ^ _103007) ^ [] : [-(member(_115504, universal_class))], (359 ^ _103007) ^ [] : [-(member(_115506, _115504))]]], (361 ^ _103007) ^ [_115747, _115749] : [-(member(ordered_pair(_115749, _115747), element_relation)), member(_115747, universal_class), member(_115749, _115747)], (371 ^ _103007) ^ [] : [-(subclass(element_relation, cross_product(universal_class, universal_class)))], (373 ^ _103007) ^ [_116150, _116152, _116154] : [member(_116150, intersection(_116154, _116152)), 376 ^ _103007 : [(377 ^ _103007) ^ [] : [-(member(_116150, _116154))], (379 ^ _103007) ^ [] : [-(member(_116150, _116152))]]], (381 ^ _103007) ^ [_116401, _116403, _116405] : [-(member(_116401, intersection(_116405, _116403))), member(_116401, _116405), member(_116401, _116403)], (391 ^ _103007) ^ [_116747, _116749] : [member(_116747, complement(_116749)), 394 ^ _103007 : [(395 ^ _103007) ^ [] : [-(member(_116747, universal_class))], (397 ^ _103007) ^ [] : [member(_116747, _116749)]]], (399 ^ _103007) ^ [_116989, _116991] : [-(member(_116989, complement(_116991))), member(_116989, universal_class), -(member(_116989, _116991))], (409 ^ _103007) ^ [_117296, _117298, _117300] : [-(restrict(_117298, _117300, _117296) = intersection(_117298, cross_product(_117300, _117296)))], (411 ^ _103007) ^ [_117387] : [member(_117387, null_class)], (413 ^ _103007) ^ [_117523, _117525] : [member(_117523, domain_of(_117525)), 416 ^ _103007 : [(417 ^ _103007) ^ [] : [-(member(_117523, universal_class))], (419 ^ _103007) ^ [] : [restrict(_117525, singleton(_117523), universal_class) = null_class]]], (421 ^ _103007) ^ [_117777, _117779] : [-(member(_117777, domain_of(_117779))), member(_117777, universal_class), -(restrict(_117779, singleton(_117777), universal_class) = null_class)], (431 ^ _103007) ^ [_118154, _118156, _118158, _118160] : [member(ordered_pair(ordered_pair(_118158, _118156), _118154), rotate(_118160)), 434 ^ _103007 : [(435 ^ _103007) ^ [] : [-(member(ordered_pair(ordered_pair(_118158, _118156), _118154), cross_product(cross_product(universal_class, universal_class), universal_class)))], (437 ^ _103007) ^ [] : [-(member(ordered_pair(ordered_pair(_118156, _118154), _118158), _118160))]]], (439 ^ _103007) ^ [_118447, _118449, _118451, _118453] : [-(member(ordered_pair(ordered_pair(_118451, _118449), _118447), rotate(_118453))), member(ordered_pair(ordered_pair(_118451, _118449), _118447), cross_product(cross_product(universal_class, universal_class), universal_class)), member(ordered_pair(ordered_pair(_118449, _118447), _118451), _118453)], (449 ^ _103007) ^ [_118779] : [-(subclass(rotate(_118779), cross_product(cross_product(universal_class, universal_class), universal_class)))], (451 ^ _103007) ^ [_118945, _118947, _118949, _118951] : [member(ordered_pair(ordered_pair(_118951, _118949), _118947), flip(_118945)), 454 ^ _103007 : [(455 ^ _103007) ^ [] : [-(member(ordered_pair(ordered_pair(_118951, _118949), _118947), cross_product(cross_product(universal_class, universal_class), universal_class)))], (457 ^ _103007) ^ [] : [-(member(ordered_pair(ordered_pair(_118949, _118951), _118947), _118945))]]], (459 ^ _103007) ^ [_119238, _119240, _119242, _119244] : [-(member(ordered_pair(ordered_pair(_119244, _119242), _119240), flip(_119238))), member(ordered_pair(ordered_pair(_119244, _119242), _119240), cross_product(cross_product(universal_class, universal_class), universal_class)), member(ordered_pair(ordered_pair(_119242, _119244), _119240), _119238)], (469 ^ _103007) ^ [_119570] : [-(subclass(flip(_119570), cross_product(cross_product(universal_class, universal_class), universal_class)))], (481 ^ _103007) ^ [_119990, _119992, _119994] : [482 ^ _103007 : [(483 ^ _103007) ^ [] : [member(_119990, _119994)], (485 ^ _103007) ^ [] : [member(_119990, _119992)]], -(member(_119990, union(_119994, _119992)))], (471 ^ _103007) ^ [_119722, _119724, _119726] : [member(_119722, union(_119726, _119724)), -(member(_119722, _119726)), -(member(_119722, _119724))], (489 ^ _103007) ^ [_120261] : [-(successor(_120261) = union(_120261, singleton(_120261)))], (491 ^ _103007) ^ [] : [-(subclass(successor_relation, cross_product(universal_class, universal_class)))], (493 ^ _103007) ^ [_120457, _120459] : [member(ordered_pair(_120459, _120457), successor_relation), 496 ^ _103007 : [(497 ^ _103007) ^ [] : [-(member(_120459, universal_class))], (499 ^ _103007) ^ [] : [-(member(_120457, universal_class))], (501 ^ _103007) ^ [] : [-(successor(_120459) = _120457)]]], (503 ^ _103007) ^ [_120778, _120780] : [-(member(ordered_pair(_120780, _120778), successor_relation)), member(_120780, universal_class), member(_120778, universal_class), successor(_120780) = _120778], (517 ^ _103007) ^ [_121149] : [-(inverse(_121149) = domain_of(flip(cross_product(_121149, universal_class))))], (519 ^ _103007) ^ [_121236] : [-(range_of(_121236) = domain_of(inverse(_121236)))], (521 ^ _103007) ^ [_121334, _121336] : [-(image(_121334, _121336) = range_of(restrict(_121334, _121336, universal_class)))], (523 ^ _103007) ^ [_121467] : [inductive(_121467), 526 ^ _103007 : [(527 ^ _103007) ^ [] : [-(member(null_class, _121467))], (529 ^ _103007) ^ [] : [-(subclass(image(successor_relation, _121467), _121467))]]], (531 ^ _103007) ^ [_121700] : [-(inductive(_121700)), member(null_class, _121700), subclass(image(successor_relation, _121700), _121700)], (542 ^ _103007) ^ [] : [-(member(540 ^ [], universal_class))], (544 ^ _103007) ^ [] : [-(inductive(540 ^ []))], (546 ^ _103007) ^ [_122145] : [inductive(_122145), -(subclass(540 ^ [], _122145))], (552 ^ _103007) ^ [_122380, _122382] : [member(_122382, sum_class(_122380)), 556 ^ _103007 : [(557 ^ _103007) ^ [] : [-(member(_122382, 555 ^ [_122380, _122382]))], (559 ^ _103007) ^ [] : [-(member(555 ^ [_122380, _122382], _122380))]]], (561 ^ _103007) ^ [_122691, _122693] : [-(member(_122693, sum_class(_122691))), 562 ^ _103007 : [(563 ^ _103007) ^ [_122785] : [member(_122693, _122785), member(_122785, _122691)]]], (571 ^ _103007) ^ [_123045] : [member(_123045, universal_class), -(member(sum_class(_123045), universal_class))], (577 ^ _103007) ^ [_123282, _123284] : [member(_123284, power_class(_123282)), 580 ^ _103007 : [(581 ^ _103007) ^ [] : [-(member(_123284, universal_class))], (583 ^ _103007) ^ [] : [-(subclass(_123284, _123282))]]], (585 ^ _103007) ^ [_123523, _123525] : [-(member(_123525, power_class(_123523))), member(_123525, universal_class), subclass(_123525, _123523)], (595 ^ _103007) ^ [_123814] : [member(_123814, universal_class), -(member(power_class(_123814), universal_class))], (601 ^ _103007) ^ [_124007, _124009] : [-(subclass(compose(_124007, _124009), cross_product(universal_class, universal_class)))], (603 ^ _103007) ^ [_124176, _124178, _124180, _124182] : [member(ordered_pair(_124178, _124176), compose(_124180, _124182)), 606 ^ _103007 : [(607 ^ _103007) ^ [] : [-(member(_124178, universal_class))], (609 ^ _103007) ^ [] : [-(member(_124176, image(_124180, image(_124182, singleton(_124178)))))]]], (611 ^ _103007) ^ [_124457, _124459, _124461, _124463] : [-(member(ordered_pair(_124459, _124457), compose(_124461, _124463))), member(_124459, universal_class), member(_124457, image(_124461, image(_124463, singleton(_124459))))], (621 ^ _103007) ^ [_124821] : [member(_124821, identity_relation), 625 ^ _103007 : [(626 ^ _103007) ^ [] : [-(member(624 ^ [_124821], universal_class))], (628 ^ _103007) ^ [] : [-(_124821 = ordered_pair(624 ^ [_124821], 624 ^ [_124821]))]]], (630 ^ _103007) ^ [_125126] : [-(member(_125126, identity_relation)), 631 ^ _103007 : [(632 ^ _103007) ^ [_125219] : [member(_125219, universal_class), _125126 = ordered_pair(_125219, _125219)]]], (640 ^ _103007) ^ [_125502] : [function(_125502), 643 ^ _103007 : [(644 ^ _103007) ^ [] : [-(subclass(_125502, cross_product(universal_class, universal_class)))], (646 ^ _103007) ^ [] : [-(subclass(compose(_125502, inverse(_125502)), identity_relation))]]], (648 ^ _103007) ^ [_125739] : [-(function(_125739)), subclass(_125739, cross_product(universal_class, universal_class)), subclass(compose(_125739, inverse(_125739)), identity_relation)], (658 ^ _103007) ^ [_126038, _126040] : [-(member(image(_126038, _126040), universal_class)), member(_126040, universal_class), function(_126038)], (678 ^ _103007) ^ [_126685, _126687] : [680 ^ _103007 : [(681 ^ _103007) ^ [] : [-(member(679 ^ [_126685, _126687], _126687))], (683 ^ _103007) ^ [] : [-(member(679 ^ [_126685, _126687], _126685))]], -(disjoint(_126687, _126685))], (668 ^ _103007) ^ [_126370, _126372] : [disjoint(_126372, _126370), 671 ^ _103007 : [(672 ^ _103007) ^ [_126509] : [member(_126509, _126372), member(_126509, _126370)]]], (687 ^ _103007) ^ [_127033] : [-(_127033 = null_class), 691 ^ _103007 : [(692 ^ _103007) ^ [] : [-(member(690 ^ [_127033], universal_class))], (694 ^ _103007) ^ [] : [-(member(690 ^ [_127033], _127033))], (696 ^ _103007) ^ [] : [-(disjoint(690 ^ [_127033], _127033))]]], (698 ^ _103007) ^ [_127443, _127445] : [-(apply(_127445, _127443) = sum_class(image(_127445, singleton(_127443))))], (701 ^ _103007) ^ [] : [-(function(699 ^ []))], (703 ^ _103007) ^ [_127643] : [member(_127643, universal_class), -(_127643 = null_class), -(member(apply(699 ^ [], _127643), _127643))]], input).
% 0.22/1.33 ncf('1',plain,[member(690 ^ [712 ^ []], 712 ^ [])],start(716 ^ 0,bind([[_128286], [690 ^ [712 ^ []]]]))).
% 0.22/1.33 ncf('1.1',plain,[-(member(690 ^ [712 ^ []], 712 ^ [])), -(712 ^ [] = null_class)],extension(687 ^ 1,bind([[_127033], [712 ^ []]]))).
% 0.22/1.33 ncf('1.1.1',plain,[712 ^ [] = null_class],extension(714 ^ 2)).
% 0.22/1.33 %-----------------------------------------------------
% 0.22/1.33 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------