%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET810+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:28 EDT 2023
% Result : Theorem 3.87s 4.49s
% Output : Proof 3.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET810+4 : TPTP v8.1.2. Released v3.2.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n001.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 18 19:29:35 EDT 2023
% 0.14/0.34 % CPUTime :
% 3.87/4.49
% 3.87/4.49 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 3.87/4.49 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.87/4.49 %-----------------------------------------------------
% 3.87/4.49 ncf(matrix, plain, [(613 ^ _79589) ^ [] : [-(member(610 ^ [], on))], (615 ^ _79589) ^ [] : [-(member(611 ^ [], on))], (617 ^ _79589) ^ [] : [-(member(610 ^ [], 611 ^ []))], (619 ^ _79589) ^ [] : [-(member(611 ^ [], 610 ^ []))], (136 ^ _79589) ^ [_84090, _84092] : [_84092 = _84090, -(power_set(_84092) = power_set(_84090))], (142 ^ _79589) ^ [_84336, _84338, _84340, _84342] : [-(intersection(_84342, _84338) = intersection(_84340, _84336)), _84342 = _84340, _84338 = _84336], (152 ^ _79589) ^ [_84695, _84697, _84699, _84701] : [-(difference(_84701, _84697) = difference(_84699, _84695)), _84701 = _84699, _84697 = _84695], (162 ^ _79589) ^ [_85054, _85056, _85058, _85060] : [-(unordered_pair(_85060, _85056) = unordered_pair(_85058, _85054)), _85060 = _85058, _85056 = _85054], (172 ^ _79589) ^ [_85385, _85387] : [_85387 = _85385, -(sum(_85387) = sum(_85385))], (178 ^ _79589) ^ [_85603, _85605] : [_85605 = _85603, -(product(_85605) = product(_85603))], (184 ^ _79589) ^ [_85877, _85879, _85881, _85883, _85885, _85887] : [-(initial_segment(_85887, _85883, _85879) = initial_segment(_85885, _85881, _85877)), _85887 = _85885, _85883 = _85881, _85879 = _85877], (198 ^ _79589) ^ [_86337, _86339] : [_86339 = _86337, -(suc(_86339) = suc(_86337))], (214 ^ _79589) ^ [_86894, _86896] : [_86896 = _86894, -(singleton(_86896) = singleton(_86894))], (204 ^ _79589) ^ [_86583, _86585, _86587, _86589] : [-(union(_86589, _86585) = union(_86587, _86583)), _86589 = _86587, _86585 = _86583], (2 ^ _79589) ^ [_79733] : [-(_79733 = _79733)], (4 ^ _79589) ^ [_79840, _79842] : [_79842 = _79840, -(_79840 = _79842)], (10 ^ _79589) ^ [_80044, _80046, _80048] : [-(_80048 = _80044), _80048 = _80046, _80046 = _80044], (20 ^ _79589) ^ [_80385, _80387, _80389, _80391] : [-(equal_set(_80389, _80385)), equal_set(_80391, _80387), _80391 = _80389, _80387 = _80385], (34 ^ _79589) ^ [_80829, _80831, _80833, _80835] : [-(strict_well_order(_80833, _80829)), strict_well_order(_80835, _80831), _80835 = _80833, _80831 = _80829], (48 ^ _79589) ^ [_81273, _81275, _81277, _81279] : [-(subset(_81277, _81273)), subset(_81279, _81275), _81279 = _81277, _81275 = _81273], (62 ^ _79589) ^ [_81745, _81747, _81749, _81751, _81753, _81755] : [-(least(_81753, _81749, _81745)), least(_81755, _81751, _81747), _81755 = _81753, _81751 = _81749, _81747 = _81745], (80 ^ _79589) ^ [_82326, _82328, _82330, _82332] : [-(strict_order(_82330, _82326)), strict_order(_82332, _82328), _82332 = _82330, _82328 = _82326], (94 ^ _79589) ^ [_82742, _82744] : [-(set(_82742)), _82744 = _82742, set(_82744)], (122 ^ _79589) ^ [_83654, _83656, _83658, _83660] : [-(member(_83658, _83654)), member(_83660, _83656), _83660 = _83658, _83656 = _83654], (104 ^ _79589) ^ [_83093, _83095, _83097, _83099, _83101, _83103] : [-(apply(_83101, _83097, _83093)), apply(_83103, _83099, _83095), _83103 = _83101, _83099 = _83097, _83095 = _83093], (230 ^ _79589) ^ [_87545, _87547] : [232 ^ _79589 : [(233 ^ _79589) ^ [] : [-(member(231 ^ [_87545, _87547], _87547))], (235 ^ _79589) ^ [] : [member(231 ^ [_87545, _87547], _87545)]], -(subset(_87547, _87545))], (220 ^ _79589) ^ [_87231, _87233] : [subset(_87233, _87231), 223 ^ _79589 : [(224 ^ _79589) ^ [_87368] : [member(_87368, _87233), -(member(_87368, _87231))]]], (239 ^ _79589) ^ [_87931, _87933] : [equal_set(_87933, _87931), 242 ^ _79589 : [(243 ^ _79589) ^ [] : [-(subset(_87933, _87931))], (245 ^ _79589) ^ [] : [-(subset(_87931, _87933))]]], (247 ^ _79589) ^ [_88168, _88170] : [-(equal_set(_88170, _88168)), subset(_88170, _88168), subset(_88168, _88170)], (257 ^ _79589) ^ [_88498, _88500] : [member(_88500, power_set(_88498)), -(subset(_88500, _88498))], (263 ^ _79589) ^ [_88664, _88666] : [subset(_88666, _88664), -(member(_88666, power_set(_88664)))], (269 ^ _79589) ^ [_88923, _88925, _88927] : [member(_88927, intersection(_88925, _88923)), 272 ^ _79589 : [(273 ^ _79589) ^ [] : [-(member(_88927, _88925))], (275 ^ _79589) ^ [] : [-(member(_88927, _88923))]]], (277 ^ _79589) ^ [_89174, _89176, _89178] : [-(member(_89178, intersection(_89176, _89174))), member(_89178, _89176), member(_89178, _89174)], (297 ^ _79589) ^ [_89802, _89804, _89806] : [298 ^ _79589 : [(299 ^ _79589) ^ [] : [member(_89806, _89804)], (301 ^ _79589) ^ [] : [member(_89806, _89802)]], -(member(_89806, union(_89804, _89802)))], (287 ^ _79589) ^ [_89534, _89536, _89538] : [member(_89538, union(_89536, _89534)), -(member(_89538, _89536)), -(member(_89538, _89534))], (305 ^ _79589) ^ [_90072] : [member(_90072, empty_set)], (307 ^ _79589) ^ [_90222, _90224, _90226] : [member(_90226, difference(_90222, _90224)), 310 ^ _79589 : [(311 ^ _79589) ^ [] : [-(member(_90226, _90222))], (313 ^ _79589) ^ [] : [member(_90226, _90224)]]], (315 ^ _79589) ^ [_90474, _90476, _90478] : [-(member(_90478, difference(_90474, _90476))), member(_90478, _90474), -(member(_90478, _90476))], (325 ^ _79589) ^ [_90823, _90825] : [member(_90825, singleton(_90823)), -(_90825 = _90823)], (331 ^ _79589) ^ [_90989, _90991] : [_90991 = _90989, -(member(_90991, singleton(_90989)))], (347 ^ _79589) ^ [_91516, _91518, _91520] : [348 ^ _79589 : [(349 ^ _79589) ^ [] : [_91520 = _91518], (351 ^ _79589) ^ [] : [_91520 = _91516]], -(member(_91520, unordered_pair(_91518, _91516)))], (337 ^ _79589) ^ [_91248, _91250, _91252] : [member(_91252, unordered_pair(_91250, _91248)), -(_91252 = _91250), -(_91252 = _91248)], (355 ^ _79589) ^ [_91845, _91847] : [member(_91847, sum(_91845)), 359 ^ _79589 : [(360 ^ _79589) ^ [] : [-(member(358 ^ [_91845, _91847], _91845))], (362 ^ _79589) ^ [] : [-(member(_91847, 358 ^ [_91845, _91847]))]]], (364 ^ _79589) ^ [_92156, _92158] : [-(member(_92158, sum(_92156))), 365 ^ _79589 : [(366 ^ _79589) ^ [_92250] : [member(_92250, _92156), member(_92158, _92250)]]], (384 ^ _79589) ^ [_92851, _92853] : [386 ^ _79589 : [(387 ^ _79589) ^ [] : [-(member(385 ^ [_92851, _92853], _92851))], (389 ^ _79589) ^ [] : [member(_92853, 385 ^ [_92851, _92853])]], -(member(_92853, product(_92851)))], (374 ^ _79589) ^ [_92533, _92535] : [member(_92535, product(_92533)), 377 ^ _79589 : [(378 ^ _79589) ^ [_92674] : [member(_92674, _92533), -(member(_92535, _92674))]]], (393 ^ _79589) ^ [_93265] : [member(_93265, on), 396 ^ _79589 : [(397 ^ _79589) ^ [] : [-(set(_93265))], (399 ^ _79589) ^ [] : [-(strict_well_order(member_predicate, _93265))], (401 ^ _79589) ^ [_93536] : [member(_93536, _93265), -(subset(_93536, _93265))]]], (407 ^ _79589) ^ [_93709] : [-(member(_93709, on)), set(_93709), strict_well_order(member_predicate, _93709), 417 ^ _79589 : [(418 ^ _79589) ^ [] : [-(member(416 ^ [_93709], _93709))], (420 ^ _79589) ^ [] : [subset(416 ^ [_93709], _93709)]]], (441 ^ _79589) ^ [_94833, _94835] : [-(strict_well_order(_94835, _94833)), strict_order(_94835, _94833), 447 ^ _79589 : [(448 ^ _79589) ^ [] : [-(subset(446 ^ [_94833, _94835], _94833))], (451 ^ _79589) ^ [] : [-(member(449 ^ [_94833, _94835], 446 ^ [_94833, _94835]))], (453 ^ _79589) ^ [_95286] : [least(_95286, _94835, 446 ^ [_94833, _94835])]]], (424 ^ _79589) ^ [_94247, _94249] : [strict_well_order(_94249, _94247), 427 ^ _79589 : [(428 ^ _79589) ^ [] : [-(strict_order(_94249, _94247))], (430 ^ _79589) ^ [_94473] : [-(least(437 ^ [_94247, _94249, _94473], _94249, _94473)), subset(_94473, _94247), 435 ^ _79589 : [(436 ^ _79589) ^ [_94644] : [member(_94644, _94473)]]]]], (473 ^ _79589) ^ [_96020, _96022, _96024] : [-(least(_96020, _96024, _96022)), member(_96020, _96022), 479 ^ _79589 : [(480 ^ _79589) ^ [] : [-(member(478 ^ [_96020, _96022, _96024], _96022))], (482 ^ _79589) ^ [] : [_96020 = 478 ^ [_96020, _96022, _96024]], (484 ^ _79589) ^ [] : [apply(_96024, _96020, 478 ^ [_96020, _96022, _96024])]]], (457 ^ _79589) ^ [_95509, _95511, _95513] : [least(_95509, _95513, _95511), 460 ^ _79589 : [(461 ^ _79589) ^ [] : [-(member(_95509, _95511))], (463 ^ _79589) ^ [_95733] : [member(_95733, _95511), -(_95509 = _95733), -(apply(_95513, _95509, _95733))]]], (488 ^ _79589) ^ [_96610, _96612] : [apply(member_predicate, _96612, _96610), -(member(_96612, _96610))], (494 ^ _79589) ^ [_96774, _96776] : [member(_96776, _96774), -(apply(member_predicate, _96776, _96774))], (571 ^ _79589) ^ [_99793] : [set(_99793), 574 ^ _79589 : [(575 ^ _79589) ^ [_99923] : [member(_99923, _99793), -(set(_99923))]]], (599 ^ _79589) ^ [_100798, _100800] : [member(_100798, suc(_100800)), -(member(_100798, union(_100800, singleton(_100800))))], (605 ^ _79589) ^ [_100974, _100976] : [member(_100974, union(_100976, singleton(_100976))), -(member(_100974, suc(_100976)))], (581 ^ _79589) ^ [_100195, _100197, _100199, _100201] : [member(_100195, initial_segment(_100201, _100199, _100197)), 584 ^ _79589 : [(585 ^ _79589) ^ [] : [-(member(_100195, _100197))], (587 ^ _79589) ^ [] : [-(apply(_100199, _100195, _100201))]]], (589 ^ _79589) ^ [_100458, _100460, _100462, _100464] : [-(member(_100458, initial_segment(_100464, _100462, _100460))), member(_100458, _100460), apply(_100462, _100458, _100464)], (540 ^ _79589) ^ [_98289, _98291] : [-(strict_order(_98291, _98289)), 545 ^ _79589 : [(546 ^ _79589) ^ [] : [-(member(543 ^ [_98289, _98291], _98289))], (548 ^ _79589) ^ [] : [-(member(544 ^ [_98289, _98291], _98289))], (550 ^ _79589) ^ [] : [-(apply(_98291, 543 ^ [_98289, _98291], 544 ^ [_98289, _98291]))], (552 ^ _79589) ^ [] : [-(apply(_98291, 544 ^ [_98289, _98291], 543 ^ [_98289, _98291]))]], 556 ^ _79589 : [(557 ^ _79589) ^ [] : [-(member(553 ^ [_98289, _98291], _98289))], (559 ^ _79589) ^ [] : [-(member(554 ^ [_98289, _98291], _98289))], (561 ^ _79589) ^ [] : [-(member(555 ^ [_98289, _98291], _98289))], (563 ^ _79589) ^ [] : [-(apply(_98291, 553 ^ [_98289, _98291], 554 ^ [_98289, _98291]))], (565 ^ _79589) ^ [] : [-(apply(_98291, 554 ^ [_98289, _98291], 555 ^ [_98289, _98291]))], (567 ^ _79589) ^ [] : [apply(_98291, 553 ^ [_98289, _98291], 555 ^ [_98289, _98291])]]], (500 ^ _79589) ^ [_97017, _97019] : [strict_order(_97019, _97017), 503 ^ _79589 : [(504 ^ _79589) ^ [_97263, _97265] : [member(_97265, _97017), member(_97263, _97017), apply(_97019, _97265, _97263), apply(_97019, _97263, _97265)], (518 ^ _79589) ^ [_97684, _97686, _97688] : [member(_97688, _97017), member(_97686, _97017), member(_97684, _97017), -(apply(_97019, _97688, _97684)), apply(_97019, _97688, _97686), apply(_97019, _97686, _97684)]]]], input).
% 3.87/4.49 ncf('1',plain,[strict_order(member_predicate, 610 ^ []), 504 : member(611 ^ [], 610 ^ []), 504 : member(611 ^ [], 610 ^ []), 504 : apply(member_predicate, 611 ^ [], 611 ^ []), 504 : apply(member_predicate, 611 ^ [], 611 ^ [])],start(500 ^ 0,bind([[_97017, _97019, _97263, _97265], [610 ^ [], member_predicate, 611 ^ [], 611 ^ []]]))).
% 3.87/4.49 ncf('1.1',plain,[-(strict_order(member_predicate, 610 ^ [])), strict_order(member_predicate, 610 ^ []), member_predicate = member_predicate, 610 ^ [] = 610 ^ []],extension(80 ^ 1,bind([[_82326, _82328, _82330, _82332], [610 ^ [], 610 ^ [], member_predicate, member_predicate]]))).
% 3.87/4.49 ncf('1.1.1',plain,[-(strict_order(member_predicate, 610 ^ [])), strict_order(member_predicate, 610 ^ []), member_predicate = member_predicate, 610 ^ [] = 610 ^ []],extension(80 ^ 2,bind([[_82326, _82328, _82330, _82332], [610 ^ [], 610 ^ [], member_predicate, member_predicate]]))).
% 3.87/4.49 ncf('1.1.1.1',plain,[-(strict_order(member_predicate, 610 ^ [])), strict_well_order(member_predicate, 610 ^ [])],extension(424 ^ 3,bind([[_94247, _94249], [610 ^ [], member_predicate]]))).
% 3.87/4.49 ncf('1.1.1.1.1',plain,[-(strict_well_order(member_predicate, 610 ^ [])), member(610 ^ [], on)],extension(393 ^ 4,bind([[_93265], [610 ^ []]]))).
% 3.87/4.49 ncf('1.1.1.1.1.1',plain,[-(member(610 ^ [], on))],extension(613 ^ 5)).
% 3.87/4.49 ncf('1.1.1.2',plain,[-(member_predicate = member_predicate)],extension(2 ^ 3,bind([[_79733], [member_predicate]]))).
% 3.87/4.49 ncf('1.1.1.3',plain,[-(610 ^ [] = 610 ^ [])],extension(2 ^ 3,bind([[_79733], [610 ^ []]]))).
% 3.87/4.49 ncf('1.1.2',plain,[-(member_predicate = member_predicate)],extension(2 ^ 2,bind([[_79733], [member_predicate]]))).
% 3.87/4.49 ncf('1.1.3',plain,[-(610 ^ [] = 610 ^ [])],extension(2 ^ 2,bind([[_79733], [610 ^ []]]))).
% 3.87/4.49 ncf('1.2',plain,[-(member(611 ^ [], 610 ^ []))],extension(619 ^ 3)).
% 3.87/4.49 ncf('1.3',plain,[-(member(611 ^ [], 610 ^ []))],extension(619 ^ 3)).
% 3.87/4.49 ncf('1.4',plain,[-(apply(member_predicate, 611 ^ [], 611 ^ [])), member(611 ^ [], 611 ^ [])],extension(494 ^ 3,bind([[_96774, _96776], [611 ^ [], 611 ^ []]]))).
% 3.87/4.49 ncf('1.4.1',plain,[-(member(611 ^ [], 611 ^ [])), member(611 ^ [], union(611 ^ [], on)), -(member(611 ^ [], on))],extension(287 ^ 4,bind([[_89534, _89536, _89538], [on, 611 ^ [], 611 ^ []]]))).
% 3.87/4.49 ncf('1.4.1.1',plain,[-(member(611 ^ [], union(611 ^ [], on))), 301 : member(611 ^ [], on)],extension(297 ^ 5,bind([[_89802, _89804, _89806], [on, 611 ^ [], 611 ^ []]]))).
% 3.87/4.49 ncf('1.4.1.1.1',plain,[-(member(611 ^ [], on))],extension(615 ^ 8)).
% 3.87/4.49 ncf('1.4.1.2',plain,[member(611 ^ [], on), 401 : member(610 ^ [], 611 ^ []), 401 : -(subset(610 ^ [], 611 ^ []))],extension(393 ^ 5,bind([[_93265, _93536], [611 ^ [], 610 ^ []]]))).
% 3.87/4.49 ncf('1.4.1.2.1',plain,[-(member(610 ^ [], 611 ^ []))],extension(617 ^ 8)).
% 3.87/4.49 ncf('1.4.1.2.2',plain,[subset(610 ^ [], 611 ^ []), 224 : member(611 ^ [], 610 ^ []), 224 : -(member(611 ^ [], 611 ^ []))],extension(220 ^ 8,bind([[_87231, _87233, _87368], [611 ^ [], 610 ^ [], 611 ^ []]]))).
% 3.87/4.49 ncf('1.4.1.2.2.1',plain,[-(member(611 ^ [], 610 ^ []))],extension(619 ^ 11)).
% 3.87/4.49 ncf('1.4.1.2.2.2',plain,[member(611 ^ [], 611 ^ [])],reduction('1.4')).
% 3.87/4.49 ncf('1.5',plain,[-(apply(member_predicate, 611 ^ [], 611 ^ []))],lemmata('x')).
% 3.87/4.49 %-----------------------------------------------------
% 3.87/4.49 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------