%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU326+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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:09 EDT 2023
% Result : Theorem 0.65s 1.38s
% Output : Proof 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU326+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n018.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 13:20:42 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.65/1.38
% 0.65/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.65/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.65/1.38 %-----------------------------------------------------
% 0.65/1.38 ncf(matrix, plain, [(530 ^ _75257) ^ [] : [-(element(528 ^ [], powerset(powerset(527 ^ []))))], (532 ^ _75257) ^ [] : [533 ^ _75257 : [(534 ^ _75257) ^ [] : [528 ^ [] = empty_set], (536 ^ _75257) ^ [] : [-(complements_of_subsets(527 ^ [], 528 ^ []) = empty_set)]], 537 ^ _75257 : [(538 ^ _75257) ^ [] : [complements_of_subsets(527 ^ [], 528 ^ []) = empty_set], (540 ^ _75257) ^ [] : [-(528 ^ [] = empty_set)]]], (172 ^ _75257) ^ [_80614, _80616] : [_80616 = _80614, -(powerset(_80616) = powerset(_80614))], (178 ^ _75257) ^ [_80840, _80842, _80844, _80846] : [-(complements_of_subsets(_80846, _80842) = complements_of_subsets(_80844, _80840)), _80846 = _80844, _80842 = _80840], (2 ^ _75257) ^ [_75401] : [-(_75401 = _75401)], (4 ^ _75257) ^ [_75508, _75510] : [_75510 = _75508, -(_75508 = _75510)], (10 ^ _75257) ^ [_75712, _75714, _75716] : [-(_75716 = _75712), _75716 = _75714, _75714 = _75712], (20 ^ _75257) ^ [_76025, _76027] : [-(v1_xcmplx_0(_76025)), _76027 = _76025, v1_xcmplx_0(_76027)], (30 ^ _75257) ^ [_76320, _76322] : [-(natural(_76320)), _76322 = _76320, natural(_76322)], (40 ^ _75257) ^ [_76615, _76617] : [-(v1_xreal_0(_76615)), _76617 = _76615, v1_xreal_0(_76617)], (50 ^ _75257) ^ [_76910, _76912] : [-(v1_int_1(_76910)), _76912 = _76910, v1_int_1(_76912)], (60 ^ _75257) ^ [_77205, _77207] : [-(v1_rat_1(_77205)), _77207 = _77205, v1_rat_1(_77207)], (70 ^ _75257) ^ [_77500, _77502] : [-(v1_membered(_77500)), _77502 = _77500, v1_membered(_77502)], (80 ^ _75257) ^ [_77795, _77797] : [-(v2_membered(_77795)), _77797 = _77795, v2_membered(_77797)], (90 ^ _75257) ^ [_78090, _78092] : [-(v3_membered(_78090)), _78092 = _78090, v3_membered(_78092)], (100 ^ _75257) ^ [_78385, _78387] : [-(v4_membered(_78385)), _78387 = _78385, v4_membered(_78387)], (110 ^ _75257) ^ [_78680, _78682] : [-(v5_membered(_78680)), _78682 = _78680, v5_membered(_78682)], (120 ^ _75257) ^ [_79003, _79005, _79007, _79009] : [-(subset(_79007, _79003)), subset(_79009, _79005), _79009 = _79007, _79005 = _79003], (134 ^ _75257) ^ [_79447, _79449, _79451, _79453] : [-(in(_79451, _79447)), in(_79453, _79449), _79453 = _79451, _79449 = _79447], (148 ^ _75257) ^ [_79863, _79865] : [-(empty(_79863)), _79865 = _79863, empty(_79865)], (158 ^ _75257) ^ [_80166, _80168, _80170, _80172] : [-(element(_80170, _80166)), element(_80172, _80168), _80172 = _80170, _80168 = _80166], (188 ^ _75257) ^ [_81177, _81179] : [in(_81179, _81177), in(_81177, _81179)], (194 ^ _75257) ^ [_81374] : [v1_membered(_81374), 197 ^ _75257 : [(198 ^ _75257) ^ [_81504] : [element(_81504, _81374), -(v1_xcmplx_0(_81504))]]], (204 ^ _75257) ^ [_81705] : [v2_membered(_81705), 207 ^ _75257 : [(208 ^ _75257) ^ [_81840] : [element(_81840, _81705), 211 ^ _75257 : [(212 ^ _75257) ^ [] : [-(v1_xcmplx_0(_81840))], (214 ^ _75257) ^ [] : [-(v1_xreal_0(_81840))]]]]], (216 ^ _75257) ^ [_82114] : [v3_membered(_82114), 219 ^ _75257 : [(220 ^ _75257) ^ [_82254] : [element(_82254, _82114), 223 ^ _75257 : [(224 ^ _75257) ^ [] : [-(v1_xcmplx_0(_82254))], (226 ^ _75257) ^ [] : [-(v1_xreal_0(_82254))], (228 ^ _75257) ^ [] : [-(v1_rat_1(_82254))]]]]], (230 ^ _75257) ^ [_82600] : [v4_membered(_82600), 233 ^ _75257 : [(234 ^ _75257) ^ [_82745] : [element(_82745, _82600), 237 ^ _75257 : [(238 ^ _75257) ^ [] : [-(v1_xcmplx_0(_82745))], (240 ^ _75257) ^ [] : [-(v1_xreal_0(_82745))], (242 ^ _75257) ^ [] : [-(v1_int_1(_82745))], (244 ^ _75257) ^ [] : [-(v1_rat_1(_82745))]]]]], (246 ^ _75257) ^ [_83163] : [v5_membered(_83163), 249 ^ _75257 : [(250 ^ _75257) ^ [_83313] : [element(_83313, _83163), 253 ^ _75257 : [(254 ^ _75257) ^ [] : [-(v1_xcmplx_0(_83313))], (256 ^ _75257) ^ [] : [-(natural(_83313))], (258 ^ _75257) ^ [] : [-(v1_xreal_0(_83313))], (260 ^ _75257) ^ [] : [-(v1_int_1(_83313))], (262 ^ _75257) ^ [] : [-(v1_rat_1(_83313))]]]]], (264 ^ _75257) ^ [_83803] : [empty(_83803), 267 ^ _75257 : [(268 ^ _75257) ^ [] : [-(v1_membered(_83803))], (270 ^ _75257) ^ [] : [-(v2_membered(_83803))], (272 ^ _75257) ^ [] : [-(v3_membered(_83803))], (274 ^ _75257) ^ [] : [-(v4_membered(_83803))], (276 ^ _75257) ^ [] : [-(v5_membered(_83803))]]], (278 ^ _75257) ^ [_84270] : [v1_membered(_84270), 281 ^ _75257 : [(282 ^ _75257) ^ [_84402] : [element(_84402, powerset(_84270)), -(v1_membered(_84402))]]], (288 ^ _75257) ^ [_84607] : [v2_membered(_84607), 291 ^ _75257 : [(292 ^ _75257) ^ [_84744] : [element(_84744, powerset(_84607)), 295 ^ _75257 : [(296 ^ _75257) ^ [] : [-(v1_membered(_84744))], (298 ^ _75257) ^ [] : [-(v2_membered(_84744))]]]]], (300 ^ _75257) ^ [_85022] : [v3_membered(_85022), 303 ^ _75257 : [(304 ^ _75257) ^ [_85164] : [element(_85164, powerset(_85022)), 307 ^ _75257 : [(308 ^ _75257) ^ [] : [-(v1_membered(_85164))], (310 ^ _75257) ^ [] : [-(v2_membered(_85164))], (312 ^ _75257) ^ [] : [-(v3_membered(_85164))]]]]], (314 ^ _75257) ^ [_85514] : [v4_membered(_85514), 317 ^ _75257 : [(318 ^ _75257) ^ [_85661] : [element(_85661, powerset(_85514)), 321 ^ _75257 : [(322 ^ _75257) ^ [] : [-(v1_membered(_85661))], (324 ^ _75257) ^ [] : [-(v2_membered(_85661))], (326 ^ _75257) ^ [] : [-(v3_membered(_85661))], (328 ^ _75257) ^ [] : [-(v4_membered(_85661))]]]]], (330 ^ _75257) ^ [_86083] : [v5_membered(_86083), -(v4_membered(_86083))], (336 ^ _75257) ^ [_86269] : [v5_membered(_86269), 339 ^ _75257 : [(340 ^ _75257) ^ [_86421] : [element(_86421, powerset(_86269)), 343 ^ _75257 : [(344 ^ _75257) ^ [] : [-(v1_membered(_86421))], (346 ^ _75257) ^ [] : [-(v2_membered(_86421))], (348 ^ _75257) ^ [] : [-(v3_membered(_86421))], (350 ^ _75257) ^ [] : [-(v4_membered(_86421))], (352 ^ _75257) ^ [] : [-(v5_membered(_86421))]]]]], (354 ^ _75257) ^ [_86915] : [v4_membered(_86915), -(v3_membered(_86915))], (360 ^ _75257) ^ [_87101] : [v3_membered(_87101), -(v2_membered(_87101))], (366 ^ _75257) ^ [_87287] : [v2_membered(_87287), -(v1_membered(_87287))], (372 ^ _75257) ^ [] : [true___, -(true___)], (378 ^ _75257) ^ [] : [true___, -(true___)], (384 ^ _75257) ^ [_87725, _87727] : [element(_87725, powerset(powerset(_87727))), -(element(complements_of_subsets(_87727, _87725), powerset(powerset(_87727))))], (390 ^ _75257) ^ [] : [true___, -(true___)], (397 ^ _75257) ^ [_88086] : [-(element(395 ^ [_88086], _88086))], (399 ^ _75257) ^ [_88168] : [empty(powerset(_88168))], (401 ^ _75257) ^ [] : [-(empty(empty_set))], (403 ^ _75257) ^ [] : [-(v1_membered(empty_set))], (405 ^ _75257) ^ [] : [-(v2_membered(empty_set))], (407 ^ _75257) ^ [] : [-(v3_membered(empty_set))], (409 ^ _75257) ^ [] : [-(v4_membered(empty_set))], (411 ^ _75257) ^ [] : [-(v5_membered(empty_set))], (413 ^ _75257) ^ [_88604, _88606] : [element(_88604, powerset(powerset(_88606))), -(complements_of_subsets(_88606, complements_of_subsets(_88606, _88604)) = _88604)], (420 ^ _75257) ^ [] : [empty(418 ^ [])], (422 ^ _75257) ^ [] : [-(v1_membered(418 ^ []))], (424 ^ _75257) ^ [] : [-(v2_membered(418 ^ []))], (426 ^ _75257) ^ [] : [-(v3_membered(418 ^ []))], (428 ^ _75257) ^ [] : [-(v4_membered(418 ^ []))], (430 ^ _75257) ^ [] : [-(v5_membered(418 ^ []))], (432 ^ _75257) ^ [_89210] : [-(empty(_89210)), 436 ^ _75257 : [(437 ^ _75257) ^ [] : [-(element(435 ^ [_89210], powerset(_89210)))], (439 ^ _75257) ^ [] : [empty(435 ^ [_89210])]]], (442 ^ _75257) ^ [_89593] : [-(element(440 ^ [_89593], powerset(_89593)))], (444 ^ _75257) ^ [_89644] : [-(empty(440 ^ [_89644]))], (446 ^ _75257) ^ [_89742, _89744] : [-(subset(_89744, _89744))], (448 ^ _75257) ^ [_89851, _89853] : [in(_89853, _89851), -(element(_89853, _89851))], (454 ^ _75257) ^ [_90061, _90063] : [element(_90063, _90061), -(empty(_90061)), -(in(_90063, _90061))], (464 ^ _75257) ^ [_90388, _90390] : [element(_90390, powerset(_90388)), -(subset(_90390, _90388))], (470 ^ _75257) ^ [_90554, _90556] : [subset(_90556, _90554), -(element(_90556, powerset(_90554)))], (476 ^ _75257) ^ [_90770, _90772] : [element(_90770, powerset(powerset(_90772))), -(_90770 = empty_set), complements_of_subsets(_90772, _90770) = empty_set], (486 ^ _75257) ^ [_91101, _91103, _91105] : [-(element(_91105, _91101)), in(_91105, _91103), element(_91103, powerset(_91101))], (496 ^ _75257) ^ [_91428, _91430, _91432] : [in(_91432, _91430), element(_91430, powerset(_91428)), empty(_91428)], (506 ^ _75257) ^ [_91724] : [empty(_91724), -(_91724 = empty_set)], (512 ^ _75257) ^ [_91926, _91928] : [in(_91928, _91926), empty(_91926)], (518 ^ _75257) ^ [_92113, _92115] : [empty(_92115), -(_92115 = _92113), empty(_92113)]], input).
% 0.65/1.38 ncf('1',plain,[534 : 528 ^ [] = empty_set, 538 : complements_of_subsets(527 ^ [], 528 ^ []) = empty_set],start(532 ^ 0)).
% 0.65/1.38 ncf('1.1',plain,[-(528 ^ [] = empty_set), element(528 ^ [], powerset(powerset(527 ^ []))), complements_of_subsets(527 ^ [], 528 ^ []) = empty_set],extension(476 ^ 3,bind([[_90770, _90772], [528 ^ [], 527 ^ []]]))).
% 0.65/1.38 ncf('1.1.1',plain,[-(element(528 ^ [], powerset(powerset(527 ^ []))))],extension(530 ^ 4)).
% 0.65/1.38 ncf('1.1.2',plain,[-(complements_of_subsets(527 ^ [], 528 ^ []) = empty_set)],extension(536 ^ 4)).
% 0.65/1.38 ncf('1.2',plain,[-(complements_of_subsets(527 ^ [], 528 ^ []) = empty_set), complements_of_subsets(527 ^ [], 528 ^ []) = complements_of_subsets(527 ^ [], empty_set), complements_of_subsets(527 ^ [], empty_set) = empty_set],extension(10 ^ 3,bind([[_75712, _75714, _75716], [empty_set, complements_of_subsets(527 ^ [], empty_set), complements_of_subsets(527 ^ [], 528 ^ [])]]))).
% 0.65/1.38 ncf('1.2.1',plain,[-(complements_of_subsets(527 ^ [], 528 ^ []) = complements_of_subsets(527 ^ [], empty_set)), 527 ^ [] = 527 ^ [], 528 ^ [] = empty_set],extension(178 ^ 4,bind([[_80840, _80842, _80844, _80846], [empty_set, 528 ^ [], 527 ^ [], 527 ^ []]]))).
% 0.65/1.38 ncf('1.2.1.1',plain,[-(527 ^ [] = 527 ^ [])],extension(2 ^ 5,bind([[_75401], [527 ^ []]]))).
% 0.65/1.38 ncf('1.2.1.2',plain,[-(528 ^ [] = empty_set)],extension(540 ^ 5)).
% 0.65/1.38 ncf('1.2.2',plain,[-(complements_of_subsets(527 ^ [], empty_set) = empty_set), element(complements_of_subsets(527 ^ [], empty_set), powerset(powerset(527 ^ []))), complements_of_subsets(527 ^ [], complements_of_subsets(527 ^ [], empty_set)) = empty_set],extension(476 ^ 4,bind([[_90770, _90772], [complements_of_subsets(527 ^ [], empty_set), 527 ^ []]]))).
% 0.65/1.38 ncf('1.2.2.1',plain,[-(element(complements_of_subsets(527 ^ [], empty_set), powerset(powerset(527 ^ [])))), element(empty_set, powerset(powerset(527 ^ [])))],extension(384 ^ 5,bind([[_87725, _87727], [empty_set, 527 ^ []]]))).
% 0.65/1.38 ncf('1.2.2.1.1',plain,[-(element(empty_set, powerset(powerset(527 ^ [])))), element(528 ^ [], powerset(powerset(527 ^ []))), 528 ^ [] = empty_set, powerset(powerset(527 ^ [])) = powerset(powerset(527 ^ []))],extension(158 ^ 6,bind([[_80166, _80168, _80170, _80172], [powerset(powerset(527 ^ [])), powerset(powerset(527 ^ [])), empty_set, 528 ^ []]]))).
% 0.65/1.38 ncf('1.2.2.1.1.1',plain,[-(element(528 ^ [], powerset(powerset(527 ^ []))))],extension(530 ^ 7)).
% 0.65/1.38 ncf('1.2.2.1.1.2',plain,[-(528 ^ [] = empty_set)],extension(540 ^ 7)).
% 0.65/1.38 ncf('1.2.2.1.1.3',plain,[-(powerset(powerset(527 ^ [])) = powerset(powerset(527 ^ [])))],extension(2 ^ 7,bind([[_75401], [powerset(powerset(527 ^ []))]]))).
% 0.65/1.38 ncf('1.2.2.2',plain,[-(complements_of_subsets(527 ^ [], complements_of_subsets(527 ^ [], empty_set)) = empty_set), element(empty_set, powerset(powerset(527 ^ [])))],extension(413 ^ 5,bind([[_88604, _88606], [empty_set, 527 ^ []]]))).
% 0.65/1.38 ncf('1.2.2.2.1',plain,[-(element(empty_set, powerset(powerset(527 ^ [])))), element(528 ^ [], powerset(powerset(527 ^ []))), 528 ^ [] = empty_set, powerset(powerset(527 ^ [])) = powerset(powerset(527 ^ []))],extension(158 ^ 6,bind([[_80166, _80168, _80170, _80172], [powerset(powerset(527 ^ [])), powerset(powerset(527 ^ [])), empty_set, 528 ^ []]]))).
% 0.65/1.38 ncf('1.2.2.2.1.1',plain,[-(element(528 ^ [], powerset(powerset(527 ^ []))))],extension(530 ^ 7)).
% 0.65/1.38 ncf('1.2.2.2.1.2',plain,[-(528 ^ [] = empty_set)],extension(540 ^ 7)).
% 0.65/1.38 ncf('1.2.2.2.1.3',plain,[-(powerset(powerset(527 ^ [])) = powerset(powerset(527 ^ [])))],extension(2 ^ 7,bind([[_75401], [powerset(powerset(527 ^ []))]]))).
% 0.65/1.38 %-----------------------------------------------------
% 0.65/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------