%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET809+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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 0.35s 1.38s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SET809+4 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.12 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 19:40:41 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.35/1.38
% 0.35/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 ncf(matrix, plain, [(612 ^ _76239) ^ [] : [-(member(610 ^ [], on))], (614 ^ _76239) ^ [] : [-(member(610 ^ [], 610 ^ []))], (136 ^ _76239) ^ [_80740, _80742] : [_80742 = _80740, -(power_set(_80742) = power_set(_80740))], (142 ^ _76239) ^ [_80986, _80988, _80990, _80992] : [-(intersection(_80992, _80988) = intersection(_80990, _80986)), _80992 = _80990, _80988 = _80986], (152 ^ _76239) ^ [_81345, _81347, _81349, _81351] : [-(difference(_81351, _81347) = difference(_81349, _81345)), _81351 = _81349, _81347 = _81345], (162 ^ _76239) ^ [_81704, _81706, _81708, _81710] : [-(unordered_pair(_81710, _81706) = unordered_pair(_81708, _81704)), _81710 = _81708, _81706 = _81704], (172 ^ _76239) ^ [_82035, _82037] : [_82037 = _82035, -(sum(_82037) = sum(_82035))], (178 ^ _76239) ^ [_82253, _82255] : [_82255 = _82253, -(product(_82255) = product(_82253))], (184 ^ _76239) ^ [_82527, _82529, _82531, _82533, _82535, _82537] : [-(initial_segment(_82537, _82533, _82529) = initial_segment(_82535, _82531, _82527)), _82537 = _82535, _82533 = _82531, _82529 = _82527], (198 ^ _76239) ^ [_82987, _82989] : [_82989 = _82987, -(suc(_82989) = suc(_82987))], (214 ^ _76239) ^ [_83544, _83546] : [_83546 = _83544, -(singleton(_83546) = singleton(_83544))], (204 ^ _76239) ^ [_83233, _83235, _83237, _83239] : [-(union(_83239, _83235) = union(_83237, _83233)), _83239 = _83237, _83235 = _83233], (2 ^ _76239) ^ [_76383] : [-(_76383 = _76383)], (4 ^ _76239) ^ [_76490, _76492] : [_76492 = _76490, -(_76490 = _76492)], (10 ^ _76239) ^ [_76694, _76696, _76698] : [-(_76698 = _76694), _76698 = _76696, _76696 = _76694], (20 ^ _76239) ^ [_77035, _77037, _77039, _77041] : [-(equal_set(_77039, _77035)), equal_set(_77041, _77037), _77041 = _77039, _77037 = _77035], (34 ^ _76239) ^ [_77479, _77481, _77483, _77485] : [-(strict_well_order(_77483, _77479)), strict_well_order(_77485, _77481), _77485 = _77483, _77481 = _77479], (48 ^ _76239) ^ [_77923, _77925, _77927, _77929] : [-(subset(_77927, _77923)), subset(_77929, _77925), _77929 = _77927, _77925 = _77923], (62 ^ _76239) ^ [_78395, _78397, _78399, _78401, _78403, _78405] : [-(least(_78403, _78399, _78395)), least(_78405, _78401, _78397), _78405 = _78403, _78401 = _78399, _78397 = _78395], (80 ^ _76239) ^ [_78976, _78978, _78980, _78982] : [-(strict_order(_78980, _78976)), strict_order(_78982, _78978), _78982 = _78980, _78978 = _78976], (94 ^ _76239) ^ [_79392, _79394] : [-(set(_79392)), _79394 = _79392, set(_79394)], (122 ^ _76239) ^ [_80304, _80306, _80308, _80310] : [-(member(_80308, _80304)), member(_80310, _80306), _80310 = _80308, _80306 = _80304], (104 ^ _76239) ^ [_79743, _79745, _79747, _79749, _79751, _79753] : [-(apply(_79751, _79747, _79743)), apply(_79753, _79749, _79745), _79753 = _79751, _79749 = _79747, _79745 = _79743], (230 ^ _76239) ^ [_84195, _84197] : [232 ^ _76239 : [(233 ^ _76239) ^ [] : [-(member(231 ^ [_84195, _84197], _84197))], (235 ^ _76239) ^ [] : [member(231 ^ [_84195, _84197], _84195)]], -(subset(_84197, _84195))], (220 ^ _76239) ^ [_83881, _83883] : [subset(_83883, _83881), 223 ^ _76239 : [(224 ^ _76239) ^ [_84018] : [member(_84018, _83883), -(member(_84018, _83881))]]], (239 ^ _76239) ^ [_84581, _84583] : [equal_set(_84583, _84581), 242 ^ _76239 : [(243 ^ _76239) ^ [] : [-(subset(_84583, _84581))], (245 ^ _76239) ^ [] : [-(subset(_84581, _84583))]]], (247 ^ _76239) ^ [_84818, _84820] : [-(equal_set(_84820, _84818)), subset(_84820, _84818), subset(_84818, _84820)], (257 ^ _76239) ^ [_85148, _85150] : [member(_85150, power_set(_85148)), -(subset(_85150, _85148))], (263 ^ _76239) ^ [_85314, _85316] : [subset(_85316, _85314), -(member(_85316, power_set(_85314)))], (269 ^ _76239) ^ [_85573, _85575, _85577] : [member(_85577, intersection(_85575, _85573)), 272 ^ _76239 : [(273 ^ _76239) ^ [] : [-(member(_85577, _85575))], (275 ^ _76239) ^ [] : [-(member(_85577, _85573))]]], (277 ^ _76239) ^ [_85824, _85826, _85828] : [-(member(_85828, intersection(_85826, _85824))), member(_85828, _85826), member(_85828, _85824)], (297 ^ _76239) ^ [_86452, _86454, _86456] : [298 ^ _76239 : [(299 ^ _76239) ^ [] : [member(_86456, _86454)], (301 ^ _76239) ^ [] : [member(_86456, _86452)]], -(member(_86456, union(_86454, _86452)))], (287 ^ _76239) ^ [_86184, _86186, _86188] : [member(_86188, union(_86186, _86184)), -(member(_86188, _86186)), -(member(_86188, _86184))], (305 ^ _76239) ^ [_86722] : [member(_86722, empty_set)], (307 ^ _76239) ^ [_86872, _86874, _86876] : [member(_86876, difference(_86872, _86874)), 310 ^ _76239 : [(311 ^ _76239) ^ [] : [-(member(_86876, _86872))], (313 ^ _76239) ^ [] : [member(_86876, _86874)]]], (315 ^ _76239) ^ [_87124, _87126, _87128] : [-(member(_87128, difference(_87124, _87126))), member(_87128, _87124), -(member(_87128, _87126))], (325 ^ _76239) ^ [_87473, _87475] : [member(_87475, singleton(_87473)), -(_87475 = _87473)], (331 ^ _76239) ^ [_87639, _87641] : [_87641 = _87639, -(member(_87641, singleton(_87639)))], (347 ^ _76239) ^ [_88166, _88168, _88170] : [348 ^ _76239 : [(349 ^ _76239) ^ [] : [_88170 = _88168], (351 ^ _76239) ^ [] : [_88170 = _88166]], -(member(_88170, unordered_pair(_88168, _88166)))], (337 ^ _76239) ^ [_87898, _87900, _87902] : [member(_87902, unordered_pair(_87900, _87898)), -(_87902 = _87900), -(_87902 = _87898)], (355 ^ _76239) ^ [_88495, _88497] : [member(_88497, sum(_88495)), 359 ^ _76239 : [(360 ^ _76239) ^ [] : [-(member(358 ^ [_88495, _88497], _88495))], (362 ^ _76239) ^ [] : [-(member(_88497, 358 ^ [_88495, _88497]))]]], (364 ^ _76239) ^ [_88806, _88808] : [-(member(_88808, sum(_88806))), 365 ^ _76239 : [(366 ^ _76239) ^ [_88900] : [member(_88900, _88806), member(_88808, _88900)]]], (384 ^ _76239) ^ [_89501, _89503] : [386 ^ _76239 : [(387 ^ _76239) ^ [] : [-(member(385 ^ [_89501, _89503], _89501))], (389 ^ _76239) ^ [] : [member(_89503, 385 ^ [_89501, _89503])]], -(member(_89503, product(_89501)))], (374 ^ _76239) ^ [_89183, _89185] : [member(_89185, product(_89183)), 377 ^ _76239 : [(378 ^ _76239) ^ [_89324] : [member(_89324, _89183), -(member(_89185, _89324))]]], (393 ^ _76239) ^ [_89915] : [member(_89915, on), 396 ^ _76239 : [(397 ^ _76239) ^ [] : [-(set(_89915))], (399 ^ _76239) ^ [] : [-(strict_well_order(member_predicate, _89915))], (401 ^ _76239) ^ [_90186] : [member(_90186, _89915), -(subset(_90186, _89915))]]], (407 ^ _76239) ^ [_90359] : [-(member(_90359, on)), set(_90359), strict_well_order(member_predicate, _90359), 417 ^ _76239 : [(418 ^ _76239) ^ [] : [-(member(416 ^ [_90359], _90359))], (420 ^ _76239) ^ [] : [subset(416 ^ [_90359], _90359)]]], (441 ^ _76239) ^ [_91483, _91485] : [-(strict_well_order(_91485, _91483)), strict_order(_91485, _91483), 447 ^ _76239 : [(448 ^ _76239) ^ [] : [-(subset(446 ^ [_91483, _91485], _91483))], (451 ^ _76239) ^ [] : [-(member(449 ^ [_91483, _91485], 446 ^ [_91483, _91485]))], (453 ^ _76239) ^ [_91936] : [least(_91936, _91485, 446 ^ [_91483, _91485])]]], (424 ^ _76239) ^ [_90897, _90899] : [strict_well_order(_90899, _90897), 427 ^ _76239 : [(428 ^ _76239) ^ [] : [-(strict_order(_90899, _90897))], (430 ^ _76239) ^ [_91123] : [-(least(437 ^ [_90897, _90899, _91123], _90899, _91123)), subset(_91123, _90897), 435 ^ _76239 : [(436 ^ _76239) ^ [_91294] : [member(_91294, _91123)]]]]], (473 ^ _76239) ^ [_92670, _92672, _92674] : [-(least(_92670, _92674, _92672)), member(_92670, _92672), 479 ^ _76239 : [(480 ^ _76239) ^ [] : [-(member(478 ^ [_92670, _92672, _92674], _92672))], (482 ^ _76239) ^ [] : [_92670 = 478 ^ [_92670, _92672, _92674]], (484 ^ _76239) ^ [] : [apply(_92674, _92670, 478 ^ [_92670, _92672, _92674])]]], (457 ^ _76239) ^ [_92159, _92161, _92163] : [least(_92159, _92163, _92161), 460 ^ _76239 : [(461 ^ _76239) ^ [] : [-(member(_92159, _92161))], (463 ^ _76239) ^ [_92383] : [member(_92383, _92161), -(_92159 = _92383), -(apply(_92163, _92159, _92383))]]], (488 ^ _76239) ^ [_93260, _93262] : [apply(member_predicate, _93262, _93260), -(member(_93262, _93260))], (494 ^ _76239) ^ [_93424, _93426] : [member(_93426, _93424), -(apply(member_predicate, _93426, _93424))], (571 ^ _76239) ^ [_96443] : [set(_96443), 574 ^ _76239 : [(575 ^ _76239) ^ [_96573] : [member(_96573, _96443), -(set(_96573))]]], (599 ^ _76239) ^ [_97448, _97450] : [member(_97448, suc(_97450)), -(member(_97448, union(_97450, singleton(_97450))))], (605 ^ _76239) ^ [_97624, _97626] : [member(_97624, union(_97626, singleton(_97626))), -(member(_97624, suc(_97626)))], (581 ^ _76239) ^ [_96845, _96847, _96849, _96851] : [member(_96845, initial_segment(_96851, _96849, _96847)), 584 ^ _76239 : [(585 ^ _76239) ^ [] : [-(member(_96845, _96847))], (587 ^ _76239) ^ [] : [-(apply(_96849, _96845, _96851))]]], (589 ^ _76239) ^ [_97108, _97110, _97112, _97114] : [-(member(_97108, initial_segment(_97114, _97112, _97110))), member(_97108, _97110), apply(_97112, _97108, _97114)], (540 ^ _76239) ^ [_94939, _94941] : [-(strict_order(_94941, _94939)), 545 ^ _76239 : [(546 ^ _76239) ^ [] : [-(member(543 ^ [_94939, _94941], _94939))], (548 ^ _76239) ^ [] : [-(member(544 ^ [_94939, _94941], _94939))], (550 ^ _76239) ^ [] : [-(apply(_94941, 543 ^ [_94939, _94941], 544 ^ [_94939, _94941]))], (552 ^ _76239) ^ [] : [-(apply(_94941, 544 ^ [_94939, _94941], 543 ^ [_94939, _94941]))]], 556 ^ _76239 : [(557 ^ _76239) ^ [] : [-(member(553 ^ [_94939, _94941], _94939))], (559 ^ _76239) ^ [] : [-(member(554 ^ [_94939, _94941], _94939))], (561 ^ _76239) ^ [] : [-(member(555 ^ [_94939, _94941], _94939))], (563 ^ _76239) ^ [] : [-(apply(_94941, 553 ^ [_94939, _94941], 554 ^ [_94939, _94941]))], (565 ^ _76239) ^ [] : [-(apply(_94941, 554 ^ [_94939, _94941], 555 ^ [_94939, _94941]))], (567 ^ _76239) ^ [] : [apply(_94941, 553 ^ [_94939, _94941], 555 ^ [_94939, _94941])]]], (500 ^ _76239) ^ [_93667, _93669] : [strict_order(_93669, _93667), 503 ^ _76239 : [(504 ^ _76239) ^ [_93913, _93915] : [member(_93915, _93667), member(_93913, _93667), apply(_93669, _93915, _93913), apply(_93669, _93913, _93915)], (518 ^ _76239) ^ [_94334, _94336, _94338] : [member(_94338, _93667), member(_94336, _93667), member(_94334, _93667), -(apply(_93669, _94338, _94334)), apply(_93669, _94338, _94336), apply(_93669, _94336, _94334)]]]], input).
% 0.35/1.38 ncf('1',plain,[strict_order(member_predicate, 610 ^ []), 504 : member(610 ^ [], 610 ^ []), 504 : member(610 ^ [], 610 ^ []), 504 : apply(member_predicate, 610 ^ [], 610 ^ []), 504 : apply(member_predicate, 610 ^ [], 610 ^ [])],start(500 ^ 0,bind([[_93667, _93669, _93913, _93915], [610 ^ [], member_predicate, 610 ^ [], 610 ^ []]]))).
% 0.35/1.38 ncf('1.1',plain,[-(strict_order(member_predicate, 610 ^ [])), strict_well_order(member_predicate, 610 ^ [])],extension(424 ^ 1,bind([[_90897, _90899], [610 ^ [], member_predicate]]))).
% 0.35/1.38 ncf('1.1.1',plain,[-(strict_well_order(member_predicate, 610 ^ [])), member(610 ^ [], on)],extension(393 ^ 2,bind([[_89915], [610 ^ []]]))).
% 0.35/1.38 ncf('1.1.1.1',plain,[-(member(610 ^ [], on))],extension(612 ^ 3)).
% 0.35/1.38 ncf('1.2',plain,[-(member(610 ^ [], 610 ^ []))],extension(614 ^ 3)).
% 0.35/1.38 ncf('1.3',plain,[-(member(610 ^ [], 610 ^ []))],extension(614 ^ 3)).
% 0.35/1.38 ncf('1.4',plain,[-(apply(member_predicate, 610 ^ [], 610 ^ [])), member(610 ^ [], 610 ^ [])],extension(494 ^ 3,bind([[_93424, _93426], [610 ^ [], 610 ^ []]]))).
% 0.35/1.38 ncf('1.4.1',plain,[-(member(610 ^ [], 610 ^ []))],lemmata('x')).
% 0.35/1.38 ncf('1.5',plain,[-(apply(member_predicate, 610 ^ [], 610 ^ []))],lemmata('x')).
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------