%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET067+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:17 EDT 2023
% Result : Theorem 0.51s 1.38s
% Output : Proof 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.12 % Problem : SET067+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.09/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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 19:02:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.51/1.38
% 0.51/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.51/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.51/1.38 %-----------------------------------------------------
% 0.51/1.38 ncf(matrix, plain, [(715 ^ _105979) ^ [] : [subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ []))], (2 ^ _105979) ^ [_106123] : [-(_106123 = _106123)], (4 ^ _105979) ^ [_106230, _106232] : [_106232 = _106230, -(_106230 = _106232)], (10 ^ _105979) ^ [_106434, _106436, _106438] : [-(_106438 = _106434), _106438 = _106436, _106436 = _106434], (20 ^ _105979) ^ [_106747, _106749] : [-(inductive(_106747)), _106749 = _106747, inductive(_106749)], (30 ^ _105979) ^ [_107070, _107072, _107074, _107076] : [-(disjoint(_107074, _107070)), disjoint(_107076, _107072), _107076 = _107074, _107072 = _107070], (44 ^ _105979) ^ [_107486, _107488] : [-(function(_107486)), _107488 = _107486, function(_107488)], (54 ^ _105979) ^ [_107809, _107811, _107813, _107815] : [-(member(_107813, _107809)), member(_107815, _107811), _107815 = _107813, _107811 = _107809], (68 ^ _105979) ^ [_108233, _108235, _108237, _108239] : [-(subclass(_108237, _108233)), subclass(_108239, _108235), _108239 = _108237, _108235 = _108233], (82 ^ _105979) ^ [_108663, _108665] : [_108665 = _108663, -(first(_108665) = first(_108663))], (88 ^ _105979) ^ [_108881, _108883] : [_108883 = _108881, -(second(_108883) = second(_108881))], (94 ^ _105979) ^ [_109099, _109101] : [_109101 = _109099, -(complement(_109101) = complement(_109099))], (100 ^ _105979) ^ [_109345, _109347, _109349, _109351] : [-(intersection(_109351, _109347) = intersection(_109349, _109345)), _109351 = _109349, _109347 = _109345], (110 ^ _105979) ^ [_109676, _109678] : [_109678 = _109676, -(rotate(_109678) = rotate(_109676))], (116 ^ _105979) ^ [_109922, _109924, _109926, _109928] : [-(union(_109928, _109924) = union(_109926, _109922)), _109928 = _109926, _109924 = _109922], (126 ^ _105979) ^ [_110253, _110255] : [_110255 = _110253, -(successor(_110255) = successor(_110253))], (132 ^ _105979) ^ [_110471, _110473] : [_110473 = _110471, -(flip(_110473) = flip(_110471))], (138 ^ _105979) ^ [_110689, _110691] : [_110691 = _110689, -(domain_of(_110691) = domain_of(_110689))], (144 ^ _105979) ^ [_110907, _110909] : [_110909 = _110907, -(range_of(_110909) = range_of(_110907))], (150 ^ _105979) ^ [_111181, _111183, _111185, _111187, _111189, _111191] : [-(restrict(_111191, _111187, _111183) = restrict(_111189, _111185, _111181)), _111191 = _111189, _111187 = _111185, _111183 = _111181], (164 ^ _105979) ^ [_111641, _111643] : [_111643 = _111641, -(power_class(_111643) = power_class(_111641))], (170 ^ _105979) ^ [_111887, _111889, _111891, _111893] : [-(ordered_pair(_111893, _111889) = ordered_pair(_111891, _111887)), _111893 = _111891, _111889 = _111887], (180 ^ _105979) ^ [_112246, _112248, _112250, _112252] : [-(cross_product(_112252, _112248) = cross_product(_112250, _112246)), _112252 = _112250, _112248 = _112246], (190 ^ _105979) ^ [_112605, _112607, _112609, _112611] : [-(compose(_112611, _112607) = compose(_112609, _112605)), _112611 = _112609, _112607 = _112605], (200 ^ _105979) ^ [_112936, _112938] : [_112938 = _112936, -(inverse(_112938) = inverse(_112936))], (206 ^ _105979) ^ [_113154, _113156] : [_113156 = _113154, -(sum_class(_113156) = sum_class(_113154))], (212 ^ _105979) ^ [_113400, _113402, _113404, _113406] : [-(image(_113406, _113402) = image(_113404, _113400)), _113406 = _113404, _113402 = _113400], (222 ^ _105979) ^ [_113731, _113733] : [_113733 = _113731, -(singleton(_113733) = singleton(_113731))], (228 ^ _105979) ^ [_113977, _113979, _113981, _113983] : [-(apply(_113983, _113979) = apply(_113981, _113977)), _113983 = _113981, _113979 = _113977], (238 ^ _105979) ^ [_114316, _114318, _114320, _114322] : [-(unordered_pair(_114322, _114318) = unordered_pair(_114320, _114316)), _114322 = _114320, _114318 = _114316], (258 ^ _105979) ^ [_115078, _115080] : [260 ^ _105979 : [(261 ^ _105979) ^ [] : [-(member(259 ^ [_115078, _115080], _115080))], (263 ^ _105979) ^ [] : [member(259 ^ [_115078, _115080], _115078)]], -(subclass(_115080, _115078))], (248 ^ _105979) ^ [_114764, _114766] : [subclass(_114766, _114764), 251 ^ _105979 : [(252 ^ _105979) ^ [_114901] : [member(_114901, _114766), -(member(_114901, _114764))]]], (267 ^ _105979) ^ [_115406] : [-(subclass(_115406, universal_class))], (269 ^ _105979) ^ [_115542, _115544] : [_115544 = _115542, 272 ^ _105979 : [(273 ^ _105979) ^ [] : [-(subclass(_115544, _115542))], (275 ^ _105979) ^ [] : [-(subclass(_115542, _115544))]]], (277 ^ _105979) ^ [_115779, _115781] : [-(_115781 = _115779), subclass(_115781, _115779), subclass(_115779, _115781)], (287 ^ _105979) ^ [_116123, _116125, _116127] : [member(_116127, unordered_pair(_116125, _116123)), 290 ^ _105979 : [(291 ^ _105979) ^ [] : [-(member(_116127, universal_class))], (293 ^ _105979) ^ [] : [-(_116127 = _116125), -(_116127 = _116123)]]], (299 ^ _105979) ^ [_116468, _116470, _116472] : [-(member(_116472, unordered_pair(_116470, _116468))), member(_116472, universal_class), 304 ^ _105979 : [(305 ^ _105979) ^ [] : [_116472 = _116470], (307 ^ _105979) ^ [] : [_116472 = _116468]]], (311 ^ _105979) ^ [_116846, _116848] : [-(member(unordered_pair(_116848, _116846), universal_class))], (313 ^ _105979) ^ [_116929] : [-(singleton(_116929) = unordered_pair(_116929, _116929))], (315 ^ _105979) ^ [_117026, _117028] : [-(ordered_pair(_117028, _117026) = unordered_pair(singleton(_117028), unordered_pair(_117028, singleton(_117026))))], (317 ^ _105979) ^ [_117205, _117207, _117209, _117211] : [member(ordered_pair(_117211, _117209), cross_product(_117207, _117205)), 320 ^ _105979 : [(321 ^ _105979) ^ [] : [-(member(_117211, _117207))], (323 ^ _105979) ^ [] : [-(member(_117209, _117205))]]], (325 ^ _105979) ^ [_117470, _117472, _117474, _117476] : [-(member(ordered_pair(_117476, _117474), cross_product(_117472, _117470))), member(_117476, _117472), member(_117474, _117470)], (335 ^ _105979) ^ [_117803, _117805] : [342 ^ _105979 : [(343 ^ _105979) ^ [] : [-(first(ordered_pair(_117805, _117803)) = _117805)], (345 ^ _105979) ^ [] : [-(second(ordered_pair(_117805, _117803)) = _117803)]], member(_117805, universal_class), member(_117803, universal_class)], (347 ^ _105979) ^ [_118211, _118213, _118215] : [member(_118211, cross_product(_118215, _118213)), -(_118211 = ordered_pair(first(_118211), second(_118211)))], (353 ^ _105979) ^ [_118476, _118478] : [member(ordered_pair(_118478, _118476), element_relation), 356 ^ _105979 : [(357 ^ _105979) ^ [] : [-(member(_118476, universal_class))], (359 ^ _105979) ^ [] : [-(member(_118478, _118476))]]], (361 ^ _105979) ^ [_118719, _118721] : [-(member(ordered_pair(_118721, _118719), element_relation)), member(_118719, universal_class), member(_118721, _118719)], (371 ^ _105979) ^ [] : [-(subclass(element_relation, cross_product(universal_class, universal_class)))], (373 ^ _105979) ^ [_119122, _119124, _119126] : [member(_119122, intersection(_119126, _119124)), 376 ^ _105979 : [(377 ^ _105979) ^ [] : [-(member(_119122, _119126))], (379 ^ _105979) ^ [] : [-(member(_119122, _119124))]]], (381 ^ _105979) ^ [_119373, _119375, _119377] : [-(member(_119373, intersection(_119377, _119375))), member(_119373, _119377), member(_119373, _119375)], (391 ^ _105979) ^ [_119719, _119721] : [member(_119719, complement(_119721)), 394 ^ _105979 : [(395 ^ _105979) ^ [] : [-(member(_119719, universal_class))], (397 ^ _105979) ^ [] : [member(_119719, _119721)]]], (399 ^ _105979) ^ [_119961, _119963] : [-(member(_119961, complement(_119963))), member(_119961, universal_class), -(member(_119961, _119963))], (409 ^ _105979) ^ [_120268, _120270, _120272] : [-(restrict(_120270, _120272, _120268) = intersection(_120270, cross_product(_120272, _120268)))], (411 ^ _105979) ^ [_120359] : [member(_120359, null_class)], (413 ^ _105979) ^ [_120495, _120497] : [member(_120495, domain_of(_120497)), 416 ^ _105979 : [(417 ^ _105979) ^ [] : [-(member(_120495, universal_class))], (419 ^ _105979) ^ [] : [restrict(_120497, singleton(_120495), universal_class) = null_class]]], (421 ^ _105979) ^ [_120749, _120751] : [-(member(_120749, domain_of(_120751))), member(_120749, universal_class), -(restrict(_120751, singleton(_120749), universal_class) = null_class)], (431 ^ _105979) ^ [_121126, _121128, _121130, _121132] : [member(ordered_pair(ordered_pair(_121130, _121128), _121126), rotate(_121132)), 434 ^ _105979 : [(435 ^ _105979) ^ [] : [-(member(ordered_pair(ordered_pair(_121130, _121128), _121126), cross_product(cross_product(universal_class, universal_class), universal_class)))], (437 ^ _105979) ^ [] : [-(member(ordered_pair(ordered_pair(_121128, _121126), _121130), _121132))]]], (439 ^ _105979) ^ [_121419, _121421, _121423, _121425] : [-(member(ordered_pair(ordered_pair(_121423, _121421), _121419), rotate(_121425))), member(ordered_pair(ordered_pair(_121423, _121421), _121419), cross_product(cross_product(universal_class, universal_class), universal_class)), member(ordered_pair(ordered_pair(_121421, _121419), _121423), _121425)], (449 ^ _105979) ^ [_121751] : [-(subclass(rotate(_121751), cross_product(cross_product(universal_class, universal_class), universal_class)))], (451 ^ _105979) ^ [_121917, _121919, _121921, _121923] : [member(ordered_pair(ordered_pair(_121923, _121921), _121919), flip(_121917)), 454 ^ _105979 : [(455 ^ _105979) ^ [] : [-(member(ordered_pair(ordered_pair(_121923, _121921), _121919), cross_product(cross_product(universal_class, universal_class), universal_class)))], (457 ^ _105979) ^ [] : [-(member(ordered_pair(ordered_pair(_121921, _121923), _121919), _121917))]]], (459 ^ _105979) ^ [_122210, _122212, _122214, _122216] : [-(member(ordered_pair(ordered_pair(_122216, _122214), _122212), flip(_122210))), member(ordered_pair(ordered_pair(_122216, _122214), _122212), cross_product(cross_product(universal_class, universal_class), universal_class)), member(ordered_pair(ordered_pair(_122214, _122216), _122212), _122210)], (469 ^ _105979) ^ [_122542] : [-(subclass(flip(_122542), cross_product(cross_product(universal_class, universal_class), universal_class)))], (481 ^ _105979) ^ [_122962, _122964, _122966] : [482 ^ _105979 : [(483 ^ _105979) ^ [] : [member(_122962, _122966)], (485 ^ _105979) ^ [] : [member(_122962, _122964)]], -(member(_122962, union(_122966, _122964)))], (471 ^ _105979) ^ [_122694, _122696, _122698] : [member(_122694, union(_122698, _122696)), -(member(_122694, _122698)), -(member(_122694, _122696))], (489 ^ _105979) ^ [_123233] : [-(successor(_123233) = union(_123233, singleton(_123233)))], (491 ^ _105979) ^ [] : [-(subclass(successor_relation, cross_product(universal_class, universal_class)))], (493 ^ _105979) ^ [_123429, _123431] : [member(ordered_pair(_123431, _123429), successor_relation), 496 ^ _105979 : [(497 ^ _105979) ^ [] : [-(member(_123431, universal_class))], (499 ^ _105979) ^ [] : [-(member(_123429, universal_class))], (501 ^ _105979) ^ [] : [-(successor(_123431) = _123429)]]], (503 ^ _105979) ^ [_123750, _123752] : [-(member(ordered_pair(_123752, _123750), successor_relation)), member(_123752, universal_class), member(_123750, universal_class), successor(_123752) = _123750], (517 ^ _105979) ^ [_124121] : [-(inverse(_124121) = domain_of(flip(cross_product(_124121, universal_class))))], (519 ^ _105979) ^ [_124208] : [-(range_of(_124208) = domain_of(inverse(_124208)))], (521 ^ _105979) ^ [_124306, _124308] : [-(image(_124306, _124308) = range_of(restrict(_124306, _124308, universal_class)))], (523 ^ _105979) ^ [_124439] : [inductive(_124439), 526 ^ _105979 : [(527 ^ _105979) ^ [] : [-(member(null_class, _124439))], (529 ^ _105979) ^ [] : [-(subclass(image(successor_relation, _124439), _124439))]]], (531 ^ _105979) ^ [_124672] : [-(inductive(_124672)), member(null_class, _124672), subclass(image(successor_relation, _124672), _124672)], (542 ^ _105979) ^ [] : [-(member(540 ^ [], universal_class))], (544 ^ _105979) ^ [] : [-(inductive(540 ^ []))], (546 ^ _105979) ^ [_125117] : [inductive(_125117), -(subclass(540 ^ [], _125117))], (552 ^ _105979) ^ [_125352, _125354] : [member(_125354, sum_class(_125352)), 556 ^ _105979 : [(557 ^ _105979) ^ [] : [-(member(_125354, 555 ^ [_125352, _125354]))], (559 ^ _105979) ^ [] : [-(member(555 ^ [_125352, _125354], _125352))]]], (561 ^ _105979) ^ [_125663, _125665] : [-(member(_125665, sum_class(_125663))), 562 ^ _105979 : [(563 ^ _105979) ^ [_125757] : [member(_125665, _125757), member(_125757, _125663)]]], (571 ^ _105979) ^ [_126017] : [member(_126017, universal_class), -(member(sum_class(_126017), universal_class))], (577 ^ _105979) ^ [_126254, _126256] : [member(_126256, power_class(_126254)), 580 ^ _105979 : [(581 ^ _105979) ^ [] : [-(member(_126256, universal_class))], (583 ^ _105979) ^ [] : [-(subclass(_126256, _126254))]]], (585 ^ _105979) ^ [_126495, _126497] : [-(member(_126497, power_class(_126495))), member(_126497, universal_class), subclass(_126497, _126495)], (595 ^ _105979) ^ [_126786] : [member(_126786, universal_class), -(member(power_class(_126786), universal_class))], (601 ^ _105979) ^ [_126979, _126981] : [-(subclass(compose(_126979, _126981), cross_product(universal_class, universal_class)))], (603 ^ _105979) ^ [_127148, _127150, _127152, _127154] : [member(ordered_pair(_127150, _127148), compose(_127152, _127154)), 606 ^ _105979 : [(607 ^ _105979) ^ [] : [-(member(_127150, universal_class))], (609 ^ _105979) ^ [] : [-(member(_127148, image(_127152, image(_127154, singleton(_127150)))))]]], (611 ^ _105979) ^ [_127429, _127431, _127433, _127435] : [-(member(ordered_pair(_127431, _127429), compose(_127433, _127435))), member(_127431, universal_class), member(_127429, image(_127433, image(_127435, singleton(_127431))))], (621 ^ _105979) ^ [_127793] : [member(_127793, identity_relation), 625 ^ _105979 : [(626 ^ _105979) ^ [] : [-(member(624 ^ [_127793], universal_class))], (628 ^ _105979) ^ [] : [-(_127793 = ordered_pair(624 ^ [_127793], 624 ^ [_127793]))]]], (630 ^ _105979) ^ [_128098] : [-(member(_128098, identity_relation)), 631 ^ _105979 : [(632 ^ _105979) ^ [_128191] : [member(_128191, universal_class), _128098 = ordered_pair(_128191, _128191)]]], (640 ^ _105979) ^ [_128474] : [function(_128474), 643 ^ _105979 : [(644 ^ _105979) ^ [] : [-(subclass(_128474, cross_product(universal_class, universal_class)))], (646 ^ _105979) ^ [] : [-(subclass(compose(_128474, inverse(_128474)), identity_relation))]]], (648 ^ _105979) ^ [_128711] : [-(function(_128711)), subclass(_128711, cross_product(universal_class, universal_class)), subclass(compose(_128711, inverse(_128711)), identity_relation)], (658 ^ _105979) ^ [_129010, _129012] : [-(member(image(_129010, _129012), universal_class)), member(_129012, universal_class), function(_129010)], (678 ^ _105979) ^ [_129657, _129659] : [680 ^ _105979 : [(681 ^ _105979) ^ [] : [-(member(679 ^ [_129657, _129659], _129659))], (683 ^ _105979) ^ [] : [-(member(679 ^ [_129657, _129659], _129657))]], -(disjoint(_129659, _129657))], (668 ^ _105979) ^ [_129342, _129344] : [disjoint(_129344, _129342), 671 ^ _105979 : [(672 ^ _105979) ^ [_129481] : [member(_129481, _129344), member(_129481, _129342)]]], (687 ^ _105979) ^ [_130005] : [-(_130005 = null_class), 691 ^ _105979 : [(692 ^ _105979) ^ [] : [-(member(690 ^ [_130005], universal_class))], (694 ^ _105979) ^ [] : [-(member(690 ^ [_130005], _130005))], (696 ^ _105979) ^ [] : [-(disjoint(690 ^ [_130005], _130005))]]], (698 ^ _105979) ^ [_130415, _130417] : [-(apply(_130417, _130415) = sum_class(image(_130417, singleton(_130415))))], (701 ^ _105979) ^ [] : [-(function(699 ^ []))], (703 ^ _105979) ^ [_130615] : [member(_130615, universal_class), -(_130615 = null_class), -(member(apply(699 ^ [], _130615), _130615))]], input).
% 0.51/1.38 ncf('1',plain,[member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], complement(unordered_pair(712 ^ [], 713 ^ []))), 397 : member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 713 ^ []))],start(391 ^ 0,bind([[_119719, _119721], [259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 713 ^ [])]]))).
% 0.51/1.38 ncf('1.1',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], complement(unordered_pair(712 ^ [], 713 ^ [])))), member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], universal_class), -(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 713 ^ [])))],extension(399 ^ 1,bind([[_119961, _119963], [259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 713 ^ [])]]))).
% 0.51/1.38 ncf('1.1.1',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], universal_class)), 252 : member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 712 ^ [])), 252 : subclass(unordered_pair(712 ^ [], 712 ^ []), universal_class)],extension(248 ^ 2,bind([[_114764, _114766, _114901], [universal_class, unordered_pair(712 ^ [], 712 ^ []), 259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]]))).
% 0.51/1.38 ncf('1.1.1.1',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 712 ^ []))), -(subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ [])))],extension(258 ^ 5,bind([[_115078, _115080], [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]))).
% 0.51/1.38 ncf('1.1.1.1.1',plain,[subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ []))],extension(715 ^ 6)).
% 0.51/1.38 ncf('1.1.1.2',plain,[-(subclass(unordered_pair(712 ^ [], 712 ^ []), universal_class))],extension(267 ^ 3,bind([[_115406], [unordered_pair(712 ^ [], 712 ^ [])]]))).
% 0.51/1.38 ncf('1.1.2',plain,[member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 713 ^ [])), -(subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ [])))],extension(258 ^ 2,bind([[_115078, _115080], [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]))).
% 0.51/1.38 ncf('1.1.2.1',plain,[subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ []))],extension(715 ^ 3)).
% 0.51/1.38 ncf('1.2',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 713 ^ []))), member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], universal_class), 305 : 259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])] = 712 ^ []],extension(299 ^ 3,bind([[_116468, _116470, _116472], [713 ^ [], 712 ^ [], 259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]]))).
% 0.51/1.38 ncf('1.2.1',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], universal_class)), 252 : member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 712 ^ [])), 252 : subclass(unordered_pair(712 ^ [], 712 ^ []), universal_class)],extension(248 ^ 4,bind([[_114764, _114766, _114901], [universal_class, unordered_pair(712 ^ [], 712 ^ []), 259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]]))).
% 0.51/1.38 ncf('1.2.1.1',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 712 ^ []))), -(subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ [])))],extension(258 ^ 7,bind([[_115078, _115080], [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]))).
% 0.51/1.38 ncf('1.2.1.1.1',plain,[subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ []))],extension(715 ^ 8)).
% 0.51/1.38 ncf('1.2.1.2',plain,[-(subclass(unordered_pair(712 ^ [], 712 ^ []), universal_class))],extension(267 ^ 5,bind([[_115406], [unordered_pair(712 ^ [], 712 ^ [])]]))).
% 0.51/1.38 ncf('1.2.2',plain,[-(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])] = 712 ^ []), 293 : -(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])] = 712 ^ []), 293 : member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 712 ^ []))],extension(287 ^ 6,bind([[_116123, _116125, _116127], [712 ^ [], 712 ^ [], 259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]]))).
% 0.51/1.38 ncf('1.2.2.1',plain,[259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])] = 712 ^ []],reduction('1.2')).
% 0.51/1.38 ncf('1.2.2.2',plain,[-(member(259 ^ [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])], unordered_pair(712 ^ [], 712 ^ []))), -(subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ [])))],extension(258 ^ 7,bind([[_115078, _115080], [unordered_pair(712 ^ [], 713 ^ []), unordered_pair(712 ^ [], 712 ^ [])]]))).
% 0.51/1.38 ncf('1.2.2.2.1',plain,[subclass(unordered_pair(712 ^ [], 712 ^ []), unordered_pair(712 ^ [], 713 ^ []))],extension(715 ^ 8)).
% 0.51/1.38 %-----------------------------------------------------
% 0.51/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------