%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU354+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:03:15 EDT 2023
% Result : Theorem 0.37s 1.37s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU354+1 : TPTP v8.1.2. Released v3.3.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n013.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 12:22:36 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.37/1.37
% 0.37/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 ncf(matrix, plain, [(579 ^ _79653) ^ [] : [-(element(577 ^ [], powerset(576 ^ [])))], (581 ^ _79653) ^ [] : [582 ^ _79653 : [(583 ^ _79653) ^ [] : [-(proper_element(577 ^ [], powerset(576 ^ [])))], (585 ^ _79653) ^ [] : [-(577 ^ [] = 576 ^ [])]], 586 ^ _79653 : [(587 ^ _79653) ^ [] : [577 ^ [] = 576 ^ []], (589 ^ _79653) ^ [] : [proper_element(577 ^ [], powerset(576 ^ []))]]], (186 ^ _79653) ^ [_85456, _85458] : [_85458 = _85456, -(k1_pcomps_1(_85458) = k1_pcomps_1(_85456))], (192 ^ _79653) ^ [_85702, _85704, _85706, _85708] : [-(union_of_subsets(_85708, _85704) = union_of_subsets(_85706, _85702)), _85708 = _85706, _85704 = _85702], (202 ^ _79653) ^ [_86033, _86035] : [_86035 = _86033, -(union(_86035) = union(_86033))], (208 ^ _79653) ^ [_86231, _86233] : [_86233 = _86231, -(powerset(_86233) = powerset(_86231))], (2 ^ _79653) ^ [_79797] : [-(_79797 = _79797)], (4 ^ _79653) ^ [_79904, _79906] : [_79906 = _79904, -(_79904 = _79906)], (10 ^ _79653) ^ [_80108, _80110, _80112] : [-(_80112 = _80108), _80112 = _80110, _80110 = _80108], (20 ^ _79653) ^ [_80421, _80423] : [-(v1_xcmplx_0(_80421)), _80423 = _80421, v1_xcmplx_0(_80423)], (30 ^ _79653) ^ [_80716, _80718] : [-(natural(_80716)), _80718 = _80716, natural(_80718)], (40 ^ _79653) ^ [_81011, _81013] : [-(v1_xreal_0(_81011)), _81013 = _81011, v1_xreal_0(_81013)], (50 ^ _79653) ^ [_81306, _81308] : [-(v1_int_1(_81306)), _81308 = _81306, v1_int_1(_81308)], (60 ^ _79653) ^ [_81601, _81603] : [-(v1_rat_1(_81601)), _81603 = _81601, v1_rat_1(_81603)], (70 ^ _79653) ^ [_81896, _81898] : [-(v1_membered(_81896)), _81898 = _81896, v1_membered(_81898)], (80 ^ _79653) ^ [_82191, _82193] : [-(v2_membered(_82191)), _82193 = _82191, v2_membered(_82193)], (90 ^ _79653) ^ [_82486, _82488] : [-(v3_membered(_82486)), _82488 = _82486, v3_membered(_82488)], (100 ^ _79653) ^ [_82781, _82783] : [-(v4_membered(_82781)), _82783 = _82781, v4_membered(_82783)], (110 ^ _79653) ^ [_83076, _83078] : [-(v5_membered(_83076)), _83078 = _83076, v5_membered(_83078)], (120 ^ _79653) ^ [_83399, _83401, _83403, _83405] : [-(subset(_83403, _83399)), subset(_83405, _83401), _83405 = _83403, _83401 = _83399], (134 ^ _79653) ^ [_83843, _83845, _83847, _83849] : [-(in(_83847, _83843)), in(_83849, _83845), _83849 = _83847, _83845 = _83843], (148 ^ _79653) ^ [_84259, _84261] : [-(empty(_84259)), _84261 = _84259, empty(_84261)], (158 ^ _79653) ^ [_84582, _84584, _84586, _84588] : [-(element(_84586, _84582)), element(_84588, _84584), _84588 = _84586, _84584 = _84582], (172 ^ _79653) ^ [_85006, _85008, _85010, _85012] : [-(proper_element(_85010, _85006)), proper_element(_85012, _85008), _85012 = _85010, _85008 = _85006], (214 ^ _79653) ^ [_86495, _86497] : [in(_86497, _86495), in(_86495, _86497)], (220 ^ _79653) ^ [_86692] : [v1_membered(_86692), 223 ^ _79653 : [(224 ^ _79653) ^ [_86822] : [element(_86822, _86692), -(v1_xcmplx_0(_86822))]]], (230 ^ _79653) ^ [_87023] : [v2_membered(_87023), 233 ^ _79653 : [(234 ^ _79653) ^ [_87158] : [element(_87158, _87023), 237 ^ _79653 : [(238 ^ _79653) ^ [] : [-(v1_xcmplx_0(_87158))], (240 ^ _79653) ^ [] : [-(v1_xreal_0(_87158))]]]]], (242 ^ _79653) ^ [_87432] : [v3_membered(_87432), 245 ^ _79653 : [(246 ^ _79653) ^ [_87572] : [element(_87572, _87432), 249 ^ _79653 : [(250 ^ _79653) ^ [] : [-(v1_xcmplx_0(_87572))], (252 ^ _79653) ^ [] : [-(v1_xreal_0(_87572))], (254 ^ _79653) ^ [] : [-(v1_rat_1(_87572))]]]]], (256 ^ _79653) ^ [_87918] : [v4_membered(_87918), 259 ^ _79653 : [(260 ^ _79653) ^ [_88063] : [element(_88063, _87918), 263 ^ _79653 : [(264 ^ _79653) ^ [] : [-(v1_xcmplx_0(_88063))], (266 ^ _79653) ^ [] : [-(v1_xreal_0(_88063))], (268 ^ _79653) ^ [] : [-(v1_int_1(_88063))], (270 ^ _79653) ^ [] : [-(v1_rat_1(_88063))]]]]], (272 ^ _79653) ^ [_88481] : [v5_membered(_88481), 275 ^ _79653 : [(276 ^ _79653) ^ [_88631] : [element(_88631, _88481), 279 ^ _79653 : [(280 ^ _79653) ^ [] : [-(v1_xcmplx_0(_88631))], (282 ^ _79653) ^ [] : [-(natural(_88631))], (284 ^ _79653) ^ [] : [-(v1_xreal_0(_88631))], (286 ^ _79653) ^ [] : [-(v1_int_1(_88631))], (288 ^ _79653) ^ [] : [-(v1_rat_1(_88631))]]]]], (290 ^ _79653) ^ [_89121] : [empty(_89121), 293 ^ _79653 : [(294 ^ _79653) ^ [] : [-(v1_membered(_89121))], (296 ^ _79653) ^ [] : [-(v2_membered(_89121))], (298 ^ _79653) ^ [] : [-(v3_membered(_89121))], (300 ^ _79653) ^ [] : [-(v4_membered(_89121))], (302 ^ _79653) ^ [] : [-(v5_membered(_89121))]]], (304 ^ _79653) ^ [_89588] : [v1_membered(_89588), 307 ^ _79653 : [(308 ^ _79653) ^ [_89720] : [element(_89720, powerset(_89588)), -(v1_membered(_89720))]]], (314 ^ _79653) ^ [_89925] : [v2_membered(_89925), 317 ^ _79653 : [(318 ^ _79653) ^ [_90062] : [element(_90062, powerset(_89925)), 321 ^ _79653 : [(322 ^ _79653) ^ [] : [-(v1_membered(_90062))], (324 ^ _79653) ^ [] : [-(v2_membered(_90062))]]]]], (326 ^ _79653) ^ [_90340] : [v3_membered(_90340), 329 ^ _79653 : [(330 ^ _79653) ^ [_90482] : [element(_90482, powerset(_90340)), 333 ^ _79653 : [(334 ^ _79653) ^ [] : [-(v1_membered(_90482))], (336 ^ _79653) ^ [] : [-(v2_membered(_90482))], (338 ^ _79653) ^ [] : [-(v3_membered(_90482))]]]]], (340 ^ _79653) ^ [_90832] : [v4_membered(_90832), 343 ^ _79653 : [(344 ^ _79653) ^ [_90979] : [element(_90979, powerset(_90832)), 347 ^ _79653 : [(348 ^ _79653) ^ [] : [-(v1_membered(_90979))], (350 ^ _79653) ^ [] : [-(v2_membered(_90979))], (352 ^ _79653) ^ [] : [-(v3_membered(_90979))], (354 ^ _79653) ^ [] : [-(v4_membered(_90979))]]]]], (356 ^ _79653) ^ [_91401] : [v5_membered(_91401), -(v4_membered(_91401))], (362 ^ _79653) ^ [_91587] : [v5_membered(_91587), 365 ^ _79653 : [(366 ^ _79653) ^ [_91739] : [element(_91739, powerset(_91587)), 369 ^ _79653 : [(370 ^ _79653) ^ [] : [-(v1_membered(_91739))], (372 ^ _79653) ^ [] : [-(v2_membered(_91739))], (374 ^ _79653) ^ [] : [-(v3_membered(_91739))], (376 ^ _79653) ^ [] : [-(v4_membered(_91739))], (378 ^ _79653) ^ [] : [-(v5_membered(_91739))]]]]], (380 ^ _79653) ^ [_92233] : [v4_membered(_92233), -(v3_membered(_92233))], (386 ^ _79653) ^ [_92419] : [v3_membered(_92419), -(v2_membered(_92419))], (392 ^ _79653) ^ [_92605] : [v2_membered(_92605), -(v1_membered(_92605))], (398 ^ _79653) ^ [_92805, _92807] : [element(_92805, _92807), 401 ^ _79653 : [(402 ^ _79653) ^ [] : [proper_element(_92805, _92807), _92805 = union(_92807)], (408 ^ _79653) ^ [] : [-(_92805 = union(_92807)), -(proper_element(_92805, _92807))]]], (414 ^ _79653) ^ [_93244] : [-(element(k1_pcomps_1(_93244), powerset(powerset(_93244))))], (416 ^ _79653) ^ [] : [true___, -(true___)], (422 ^ _79653) ^ [] : [true___, -(true___)], (428 ^ _79653) ^ [] : [true___, -(true___)], (434 ^ _79653) ^ [_93714, _93716] : [element(_93714, powerset(powerset(_93716))), -(element(union_of_subsets(_93716, _93714), powerset(_93716)))], (440 ^ _79653) ^ [] : [true___, -(true___)], (447 ^ _79653) ^ [_94071] : [-(element(445 ^ [_94071], _94071))], (449 ^ _79653) ^ [_94153] : [empty(powerset(_94153))], (451 ^ _79653) ^ [] : [-(empty(empty_set))], (453 ^ _79653) ^ [] : [-(v1_membered(empty_set))], (455 ^ _79653) ^ [] : [-(v2_membered(empty_set))], (457 ^ _79653) ^ [] : [-(v3_membered(empty_set))], (459 ^ _79653) ^ [] : [-(v4_membered(empty_set))], (461 ^ _79653) ^ [] : [-(v5_membered(empty_set))], (464 ^ _79653) ^ [] : [empty(462 ^ [])], (466 ^ _79653) ^ [] : [-(v1_membered(462 ^ []))], (468 ^ _79653) ^ [] : [-(v2_membered(462 ^ []))], (470 ^ _79653) ^ [] : [-(v3_membered(462 ^ []))], (472 ^ _79653) ^ [] : [-(v4_membered(462 ^ []))], (474 ^ _79653) ^ [] : [-(v5_membered(462 ^ []))], (476 ^ _79653) ^ [_94965] : [-(empty(_94965)), 480 ^ _79653 : [(481 ^ _79653) ^ [] : [-(element(479 ^ [_94965], powerset(_94965)))], (483 ^ _79653) ^ [] : [empty(479 ^ [_94965])]]], (486 ^ _79653) ^ [_95348] : [-(element(484 ^ [_95348], powerset(_95348)))], (488 ^ _79653) ^ [_95399] : [-(empty(484 ^ [_95399]))], (491 ^ _79653) ^ [_95554] : [-(element(489 ^ [_95554], powerset(_95554)))], (493 ^ _79653) ^ [_95604] : [proper_element(489 ^ [_95604], powerset(_95604))], (495 ^ _79653) ^ [_95691] : [-(k1_pcomps_1(_95691) = powerset(_95691))], (497 ^ _79653) ^ [_95802, _95804] : [element(_95802, powerset(powerset(_95804))), -(union_of_subsets(_95804, _95802) = union(_95802))], (503 ^ _79653) ^ [_96015, _96017] : [-(subset(_96017, _96017))], (505 ^ _79653) ^ [_96124, _96126] : [in(_96126, _96124), -(element(_96126, _96124))], (511 ^ _79653) ^ [_96334, _96336] : [element(_96336, _96334), -(empty(_96334)), -(in(_96336, _96334))], (521 ^ _79653) ^ [_96661, _96663] : [element(_96663, powerset(_96661)), -(subset(_96663, _96661))], (527 ^ _79653) ^ [_96827, _96829] : [subset(_96829, _96827), -(element(_96829, powerset(_96827)))], (533 ^ _79653) ^ [_97057, _97059, _97061] : [-(element(_97061, _97057)), in(_97061, _97059), element(_97059, powerset(_97057))], (543 ^ _79653) ^ [_97384, _97386, _97388] : [in(_97388, _97386), element(_97386, powerset(_97384)), empty(_97384)], (553 ^ _79653) ^ [_97680] : [empty(_97680), -(_97680 = empty_set)], (559 ^ _79653) ^ [_97882, _97884] : [in(_97884, _97882), empty(_97882)], (575 ^ _79653) ^ [_98337] : [-(union(powerset(_98337)) = _98337)], (565 ^ _79653) ^ [_98089, _98091] : [empty(_98091), -(_98091 = _98089), empty(_98089)]], input).
% 0.37/1.37 ncf('1',plain,[element(577 ^ [], powerset(576 ^ [])), 402 : proper_element(577 ^ [], powerset(576 ^ [])), 402 : 577 ^ [] = union(powerset(576 ^ []))],start(398 ^ 0,bind([[_92805, _92807], [577 ^ [], powerset(576 ^ [])]]))).
% 0.37/1.37 ncf('1.1',plain,[-(element(577 ^ [], powerset(576 ^ [])))],extension(579 ^ 1)).
% 0.37/1.37 ncf('1.2',plain,[-(proper_element(577 ^ [], powerset(576 ^ []))), -(577 ^ [] = union(powerset(576 ^ [])))],extension(408 ^ 3)).
% 0.37/1.37 ncf('1.2.1',plain,[577 ^ [] = union(powerset(576 ^ [])), -(577 ^ [] = 576 ^ []), union(powerset(576 ^ [])) = 576 ^ []],extension(10 ^ 4,bind([[_80108, _80110, _80112], [576 ^ [], union(powerset(576 ^ [])), 577 ^ []]]))).
% 0.37/1.37 ncf('1.2.1.1',plain,[577 ^ [] = 576 ^ [], 583 : -(proper_element(577 ^ [], powerset(576 ^ [])))],extension(581 ^ 5)).
% 0.37/1.37 ncf('1.2.1.1.1',plain,[proper_element(577 ^ [], powerset(576 ^ []))],reduction('1')).
% 0.37/1.37 ncf('1.2.1.2',plain,[-(union(powerset(576 ^ [])) = 576 ^ [])],extension(575 ^ 5,bind([[_98337], [576 ^ []]]))).
% 0.37/1.37 ncf('1.3',plain,[-(577 ^ [] = union(powerset(576 ^ []))), 577 ^ [] = 576 ^ [], 576 ^ [] = union(powerset(576 ^ []))],extension(10 ^ 3,bind([[_80108, _80110, _80112], [union(powerset(576 ^ [])), 576 ^ [], 577 ^ []]]))).
% 0.37/1.37 ncf('1.3.1',plain,[-(577 ^ [] = 576 ^ []), 589 : proper_element(577 ^ [], powerset(576 ^ []))],extension(581 ^ 4)).
% 0.37/1.37 ncf('1.3.1.1',plain,[-(proper_element(577 ^ [], powerset(576 ^ [])))],lemmata('x')).
% 0.37/1.37 ncf('1.3.2',plain,[-(576 ^ [] = union(powerset(576 ^ []))), union(powerset(576 ^ [])) = 576 ^ []],extension(4 ^ 4,bind([[_79904, _79906], [576 ^ [], union(powerset(576 ^ []))]]))).
% 0.37/1.37 ncf('1.3.2.1',plain,[-(union(powerset(576 ^ [])) = 576 ^ [])],extension(575 ^ 5,bind([[_98337], [576 ^ []]]))).
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------