%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU115+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:02:14 EDT 2023
% Result : Theorem 0.34s 1.39s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU115+1 : TPTP v8.1.2. Released v3.2.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n019.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 12:57:12 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.34/1.39
% 0.34/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 ncf(matrix, plain, [(446 ^ _62613) ^ [] : [finite_subsets(empty_set) = singleton(empty_set)], (210 ^ _62613) ^ [_69225, _69227] : [-(subset(_69227, _69227))], (212 ^ _62613) ^ [_69334, _69336] : [in(_69336, _69334), in(_69334, _69336)], (218 ^ _62613) ^ [_69545, _69547] : [in(_69547, _69545), -(element(_69547, _69545))], (224 ^ _62613) ^ [_69769, _69771, _69773] : [-(element(_69773, _69769)), in(_69773, _69771), element(_69771, powerset(_69769))], (234 ^ _62613) ^ [_70096, _70098, _70100] : [in(_70100, _70098), element(_70098, powerset(_70096)), empty(_70096)], (245 ^ _62613) ^ [_70416] : [-(element(243 ^ [_70416], _70416))], (247 ^ _62613) ^ [_70514] : [preboolean(_70514), 250 ^ _62613 : [(251 ^ _62613) ^ [] : [-(cup_closed(_70514))], (253 ^ _62613) ^ [] : [-(diff_closed(_70514))]]], (255 ^ _62613) ^ [_70771] : [-(preboolean(_70771)), cup_closed(_70771), diff_closed(_70771)], (265 ^ _62613) ^ [_71054, _71056] : [element(_71054, finite_subsets(_71056)), -(finite(_71054))], (271 ^ _62613) ^ [_71252] : [empty(_71252), -(finite(_71252))], (277 ^ _62613) ^ [_71438] : [finite(_71438), 280 ^ _62613 : [(281 ^ _62613) ^ [_71570] : [element(_71570, powerset(_71438)), -(finite(_71570))]]], (287 ^ _62613) ^ [_71789, _71791] : [element(_71791, _71789), -(empty(_71789)), -(in(_71791, _71789))], (297 ^ _62613) ^ [_72116, _72118] : [element(_72118, powerset(_72116)), -(subset(_72118, _72116))], (303 ^ _62613) ^ [_72282, _72284] : [subset(_72284, _72282), -(element(_72284, powerset(_72282)))], (309 ^ _62613) ^ [_72498, _72500] : [in(_72500, _72498), empty(_72498)], (315 ^ _62613) ^ [_72705, _72707] : [empty(_72707), -(_72707 = _72705), empty(_72705)], (325 ^ _62613) ^ [_72973] : [-(preboolean(finite_subsets(_72973)))], (327 ^ _62613) ^ [_73071] : [empty(powerset(_73071))], (329 ^ _62613) ^ [_73136] : [-(cup_closed(powerset(_73136)))], (331 ^ _62613) ^ [_73201] : [-(diff_closed(powerset(_73201)))], (333 ^ _62613) ^ [_73246] : [-(preboolean(powerset(_73246)))], (335 ^ _62613) ^ [_73350] : [empty(finite_subsets(_73350))], (337 ^ _62613) ^ [_73415] : [-(cup_closed(finite_subsets(_73415)))], (339 ^ _62613) ^ [_73480] : [-(diff_closed(finite_subsets(_73480)))], (341 ^ _62613) ^ [_73525] : [-(preboolean(finite_subsets(_73525)))], (344 ^ _62613) ^ [] : [empty(342 ^ [])], (346 ^ _62613) ^ [] : [-(cup_closed(342 ^ []))], (348 ^ _62613) ^ [] : [-(cap_closed(342 ^ []))], (350 ^ _62613) ^ [] : [-(diff_closed(342 ^ []))], (352 ^ _62613) ^ [] : [-(preboolean(342 ^ []))], (354 ^ _62613) ^ [_73959] : [empty(singleton(_73959))], (356 ^ _62613) ^ [_74004] : [-(finite(singleton(_74004)))], (359 ^ _62613) ^ [] : [empty(357 ^ [])], (361 ^ _62613) ^ [] : [-(finite(357 ^ []))], (364 ^ _62613) ^ [_74341] : [-(element(362 ^ [_74341], powerset(_74341)))], (366 ^ _62613) ^ [_74412] : [-(empty(362 ^ [_74412]))], (368 ^ _62613) ^ [_74480] : [-(relation(362 ^ [_74480]))], (370 ^ _62613) ^ [_74548] : [-(function(362 ^ [_74548]))], (372 ^ _62613) ^ [_74616] : [-(one_to_one(362 ^ [_74616]))], (374 ^ _62613) ^ [_74684] : [-(epsilon_transitive(362 ^ [_74684]))], (376 ^ _62613) ^ [_74752] : [-(epsilon_connected(362 ^ [_74752]))], (378 ^ _62613) ^ [_74820] : [-(ordinal(362 ^ [_74820]))], (380 ^ _62613) ^ [_74888] : [-(natural(362 ^ [_74888]))], (382 ^ _62613) ^ [_74936] : [-(finite(362 ^ [_74936]))], (384 ^ _62613) ^ [_75051] : [-(empty(_75051)), 388 ^ _62613 : [(389 ^ _62613) ^ [] : [-(element(387 ^ [_75051], powerset(_75051)))], (391 ^ _62613) ^ [] : [empty(387 ^ [_75051])], (393 ^ _62613) ^ [] : [-(finite(387 ^ [_75051]))]]], (395 ^ _62613) ^ [_75463] : [-(empty(_75463)), 399 ^ _62613 : [(400 ^ _62613) ^ [] : [-(element(398 ^ [_75463], powerset(_75463)))], (402 ^ _62613) ^ [] : [empty(398 ^ [_75463])], (404 ^ _62613) ^ [] : [-(finite(398 ^ [_75463]))]]], (406 ^ _62613) ^ [_75859] : [empty(powerset(_75859))], (408 ^ _62613) ^ [_75937] : [empty(singleton(_75937))], (410 ^ _62613) ^ [_76031] : [-(empty(_76031)), 414 ^ _62613 : [(415 ^ _62613) ^ [] : [-(element(413 ^ [_76031], powerset(_76031)))], (417 ^ _62613) ^ [] : [empty(413 ^ [_76031])]]], (420 ^ _62613) ^ [_76414] : [-(element(418 ^ [_76414], powerset(_76414)))], (422 ^ _62613) ^ [_76465] : [-(empty(418 ^ [_76465]))], (424 ^ _62613) ^ [] : [-(empty(empty_set))], (427 ^ _62613) ^ [] : [-(empty(425 ^ []))], (430 ^ _62613) ^ [] : [empty(428 ^ [])], (432 ^ _62613) ^ [_76796] : [empty(_76796), -(_76796 = empty_set)], (444 ^ _62613) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (438 ^ _62613) ^ [_76984] : [finite(_76984), -(finite_subsets(_76984) = powerset(_76984))], (192 ^ _62613) ^ [_68564, _68566] : [_68566 = _68564, -(powerset(_68566) = powerset(_68564))], (198 ^ _62613) ^ [_68782, _68784] : [_68784 = _68782, -(finite_subsets(_68784) = finite_subsets(_68782))], (204 ^ _62613) ^ [_68980, _68982] : [_68982 = _68980, -(singleton(_68982) = singleton(_68980))], (2 ^ _62613) ^ [_62757] : [-(_62757 = _62757)], (4 ^ _62613) ^ [_62864, _62866] : [_62866 = _62864, -(_62864 = _62866)], (10 ^ _62613) ^ [_63068, _63070, _63072] : [-(_63072 = _63068), _63072 = _63070, _63070 = _63068], (20 ^ _62613) ^ [_63409, _63411, _63413, _63415] : [-(subset(_63413, _63409)), subset(_63415, _63411), _63415 = _63413, _63411 = _63409], (34 ^ _62613) ^ [_63853, _63855, _63857, _63859] : [-(in(_63857, _63853)), in(_63859, _63855), _63859 = _63857, _63855 = _63853], (48 ^ _62613) ^ [_64269, _64271] : [-(cup_closed(_64269)), _64271 = _64269, cup_closed(_64271)], (58 ^ _62613) ^ [_64564, _64566] : [-(cap_closed(_64564)), _64566 = _64564, cap_closed(_64566)], (68 ^ _62613) ^ [_64859, _64861] : [-(diff_closed(_64859)), _64861 = _64859, diff_closed(_64861)], (78 ^ _62613) ^ [_65154, _65156] : [-(preboolean(_65154)), _65156 = _65154, preboolean(_65156)], (88 ^ _62613) ^ [_65449, _65451] : [-(relation(_65449)), _65451 = _65449, relation(_65451)], (98 ^ _62613) ^ [_65744, _65746] : [-(function(_65744)), _65746 = _65744, function(_65746)], (108 ^ _62613) ^ [_66039, _66041] : [-(one_to_one(_66039)), _66041 = _66039, one_to_one(_66041)], (118 ^ _62613) ^ [_66334, _66336] : [-(epsilon_transitive(_66334)), _66336 = _66334, epsilon_transitive(_66336)], (128 ^ _62613) ^ [_66629, _66631] : [-(epsilon_connected(_66629)), _66631 = _66629, epsilon_connected(_66631)], (138 ^ _62613) ^ [_66924, _66926] : [-(ordinal(_66924)), _66926 = _66924, ordinal(_66926)], (148 ^ _62613) ^ [_67219, _67221] : [-(natural(_67219)), _67221 = _67219, natural(_67221)], (158 ^ _62613) ^ [_67542, _67544, _67546, _67548] : [-(element(_67546, _67542)), element(_67548, _67544), _67548 = _67546, _67544 = _67542], (172 ^ _62613) ^ [_67958, _67960] : [-(empty(_67958)), _67960 = _67958, empty(_67960)], (182 ^ _62613) ^ [_68233, _68235] : [-(finite(_68233)), _68235 = _68233, finite(_68235)]], input).
% 0.34/1.39 ncf('1',plain,[finite_subsets(empty_set) = singleton(empty_set)],start(446 ^ 0)).
% 0.34/1.39 ncf('1.1',plain,[-(finite_subsets(empty_set) = singleton(empty_set)), finite_subsets(empty_set) = powerset(empty_set), powerset(empty_set) = singleton(empty_set)],extension(10 ^ 1,bind([[_63068, _63070, _63072], [singleton(empty_set), powerset(empty_set), finite_subsets(empty_set)]]))).
% 0.34/1.39 ncf('1.1.1',plain,[-(finite_subsets(empty_set) = powerset(empty_set)), finite(empty_set)],extension(438 ^ 2,bind([[_76984], [empty_set]]))).
% 0.34/1.39 ncf('1.1.1.1',plain,[-(finite(empty_set)), empty(empty_set)],extension(271 ^ 3,bind([[_71252], [empty_set]]))).
% 0.34/1.39 ncf('1.1.1.1.1',plain,[-(empty(empty_set))],extension(424 ^ 4)).
% 0.34/1.39 ncf('1.1.2',plain,[-(powerset(empty_set) = singleton(empty_set))],extension(444 ^ 2)).
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------