%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU112+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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 101.81s 98.58s
% Output : Proof 101.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SEU112+1 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.14 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n009.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 13:35:18 EDT 2023
% 0.14/0.34 % CPUTime :
% 101.81/98.58
% 101.81/98.58 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 101.81/98.58 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 101.81/98.58 %-----------------------------------------------------
% 101.81/98.58 ncf(matrix, plain, [(484 ^ _71705) ^ [] : [subset(set_union2(finite_subsets(481 ^ []), finite_subsets(482 ^ [])), finite_subsets(set_union2(481 ^ [], 482 ^ [])))], (214 ^ _71705) ^ [_78473, _78475] : [in(_78475, _78473), in(_78473, _78475)], (220 ^ _71705) ^ [_78670] : [empty(_78670), -(finite(_78670))], (226 ^ _71705) ^ [_78856] : [preboolean(_78856), 229 ^ _71705 : [(230 ^ _71705) ^ [] : [-(cup_closed(_78856))], (232 ^ _71705) ^ [] : [-(diff_closed(_78856))]]], (234 ^ _71705) ^ [_79113] : [finite(_79113), 237 ^ _71705 : [(238 ^ _71705) ^ [_79245] : [element(_79245, powerset(_79113)), -(finite(_79245))]]], (244 ^ _71705) ^ [_79450] : [-(preboolean(_79450)), cup_closed(_79450), diff_closed(_79450)], (254 ^ _71705) ^ [_79733, _79735] : [element(_79733, finite_subsets(_79735)), -(finite(_79733))], (260 ^ _71705) ^ [_79930, _79932] : [-(set_union2(_79932, _79930) = set_union2(_79930, _79932))], (262 ^ _71705) ^ [_80016] : [-(preboolean(finite_subsets(_80016)))], (265 ^ _71705) ^ [_80134] : [-(element(263 ^ [_80134], _80134))], (267 ^ _71705) ^ [_80236] : [empty(powerset(_80236))], (269 ^ _71705) ^ [_80301] : [-(cup_closed(powerset(_80301)))], (271 ^ _71705) ^ [_80366] : [-(diff_closed(powerset(_80366)))], (273 ^ _71705) ^ [_80411] : [-(preboolean(powerset(_80411)))], (275 ^ _71705) ^ [_80495] : [empty(powerset(_80495))], (277 ^ _71705) ^ [] : [-(empty(empty_set))], (279 ^ _71705) ^ [_80646] : [empty(finite_subsets(_80646))], (281 ^ _71705) ^ [_80711] : [-(cup_closed(finite_subsets(_80711)))], (283 ^ _71705) ^ [_80776] : [-(diff_closed(finite_subsets(_80776)))], (285 ^ _71705) ^ [_80821] : [-(preboolean(finite_subsets(_80821)))], (287 ^ _71705) ^ [_80935, _80937] : [-(empty(_80937)), empty(set_union2(_80937, _80935))], (293 ^ _71705) ^ [_81151, _81153] : [-(empty(_81153)), empty(set_union2(_81151, _81153))], (299 ^ _71705) ^ [_81367, _81369] : [-(finite(set_union2(_81369, _81367))), finite(_81369), finite(_81367)], (309 ^ _71705) ^ [_81651, _81653] : [-(set_union2(_81653, _81653) = _81653)], (312 ^ _71705) ^ [] : [empty(310 ^ [])], (314 ^ _71705) ^ [] : [-(finite(310 ^ []))], (317 ^ _71705) ^ [] : [empty(315 ^ [])], (319 ^ _71705) ^ [] : [-(cup_closed(315 ^ []))], (321 ^ _71705) ^ [] : [-(cap_closed(315 ^ []))], (323 ^ _71705) ^ [] : [-(diff_closed(315 ^ []))], (325 ^ _71705) ^ [] : [-(preboolean(315 ^ []))], (327 ^ _71705) ^ [_82229] : [-(empty(_82229)), 331 ^ _71705 : [(332 ^ _71705) ^ [] : [-(element(330 ^ [_82229], powerset(_82229)))], (334 ^ _71705) ^ [] : [empty(330 ^ [_82229])]]], (337 ^ _71705) ^ [] : [-(empty(335 ^ []))], (340 ^ _71705) ^ [_82741] : [-(element(338 ^ [_82741], powerset(_82741)))], (342 ^ _71705) ^ [_82812] : [-(empty(338 ^ [_82812]))], (344 ^ _71705) ^ [_82880] : [-(relation(338 ^ [_82880]))], (346 ^ _71705) ^ [_82948] : [-(function(338 ^ [_82948]))], (348 ^ _71705) ^ [_83016] : [-(one_to_one(338 ^ [_83016]))], (350 ^ _71705) ^ [_83084] : [-(epsilon_transitive(338 ^ [_83084]))], (352 ^ _71705) ^ [_83152] : [-(epsilon_connected(338 ^ [_83152]))], (354 ^ _71705) ^ [_83220] : [-(ordinal(338 ^ [_83220]))], (356 ^ _71705) ^ [_83288] : [-(natural(338 ^ [_83288]))], (358 ^ _71705) ^ [_83336] : [-(finite(338 ^ [_83336]))], (361 ^ _71705) ^ [_83502] : [-(element(359 ^ [_83502], powerset(_83502)))], (363 ^ _71705) ^ [_83553] : [-(empty(359 ^ [_83553]))], (366 ^ _71705) ^ [] : [empty(364 ^ [])], (368 ^ _71705) ^ [_83742] : [-(empty(_83742)), 372 ^ _71705 : [(373 ^ _71705) ^ [] : [-(element(371 ^ [_83742], powerset(_83742)))], (375 ^ _71705) ^ [] : [empty(371 ^ [_83742])], (377 ^ _71705) ^ [] : [-(finite(371 ^ [_83742]))]]], (379 ^ _71705) ^ [_84154] : [-(empty(_84154)), 383 ^ _71705 : [(384 ^ _71705) ^ [] : [-(element(382 ^ [_84154], powerset(_84154)))], (386 ^ _71705) ^ [] : [empty(382 ^ [_84154])], (388 ^ _71705) ^ [] : [-(finite(382 ^ [_84154]))]]], (390 ^ _71705) ^ [_84565, _84567] : [-(subset(_84567, _84567))], (392 ^ _71705) ^ [_84645] : [-(set_union2(_84645, empty_set) = _84645)], (394 ^ _71705) ^ [_84755, _84757] : [in(_84757, _84755), -(element(_84757, _84755))], (400 ^ _71705) ^ [_84965, _84967] : [subset(_84967, _84965), -(subset(finite_subsets(_84967), finite_subsets(_84965)))], (406 ^ _71705) ^ [_85183, _85185] : [element(_85185, _85183), -(empty(_85183)), -(in(_85185, _85183))], (416 ^ _71705) ^ [_85510, _85512] : [element(_85512, powerset(_85510)), -(subset(_85512, _85510))], (422 ^ _71705) ^ [_85676, _85678] : [subset(_85678, _85676), -(element(_85678, powerset(_85676)))], (428 ^ _71705) ^ [_85906, _85908, _85910] : [-(element(_85910, _85906)), in(_85910, _85908), element(_85908, powerset(_85906))], (438 ^ _71705) ^ [_86233, _86235, _86237] : [in(_86237, _86235), element(_86235, powerset(_86233)), empty(_86233)], (448 ^ _71705) ^ [_86529] : [empty(_86529), -(_86529 = empty_set)], (454 ^ _71705) ^ [_86731, _86733] : [in(_86733, _86731), empty(_86731)], (460 ^ _71705) ^ [_86923, _86925] : [-(subset(_86925, set_union2(_86925, _86923)))], (462 ^ _71705) ^ [_87035, _87037] : [empty(_87037), -(_87037 = _87035), empty(_87035)], (472 ^ _71705) ^ [_87326, _87328, _87330] : [-(subset(set_union2(_87330, _87326), _87328)), subset(_87330, _87328), subset(_87326, _87328)], (192 ^ _71705) ^ [_77656, _77658] : [_77658 = _77656, -(powerset(_77658) = powerset(_77656))], (198 ^ _71705) ^ [_77874, _77876] : [_77876 = _77874, -(finite_subsets(_77876) = finite_subsets(_77874))], (204 ^ _71705) ^ [_78100, _78102, _78104, _78106] : [-(set_union2(_78106, _78102) = set_union2(_78104, _78100)), _78106 = _78104, _78102 = _78100], (2 ^ _71705) ^ [_71849] : [-(_71849 = _71849)], (4 ^ _71705) ^ [_71956, _71958] : [_71958 = _71956, -(_71956 = _71958)], (10 ^ _71705) ^ [_72160, _72162, _72164] : [-(_72164 = _72160), _72164 = _72162, _72162 = _72160], (20 ^ _71705) ^ [_72473, _72475] : [-(cup_closed(_72473)), _72475 = _72473, cup_closed(_72475)], (30 ^ _71705) ^ [_72768, _72770] : [-(cap_closed(_72768)), _72770 = _72768, cap_closed(_72770)], (40 ^ _71705) ^ [_73063, _73065] : [-(diff_closed(_73063)), _73065 = _73063, diff_closed(_73065)], (50 ^ _71705) ^ [_73358, _73360] : [-(preboolean(_73358)), _73360 = _73358, preboolean(_73360)], (60 ^ _71705) ^ [_73653, _73655] : [-(relation(_73653)), _73655 = _73653, relation(_73655)], (70 ^ _71705) ^ [_73948, _73950] : [-(function(_73948)), _73950 = _73948, function(_73950)], (80 ^ _71705) ^ [_74243, _74245] : [-(one_to_one(_74243)), _74245 = _74243, one_to_one(_74245)], (90 ^ _71705) ^ [_74538, _74540] : [-(epsilon_transitive(_74538)), _74540 = _74538, epsilon_transitive(_74540)], (100 ^ _71705) ^ [_74833, _74835] : [-(epsilon_connected(_74833)), _74835 = _74833, epsilon_connected(_74835)], (110 ^ _71705) ^ [_75128, _75130] : [-(ordinal(_75128)), _75130 = _75128, ordinal(_75130)], (120 ^ _71705) ^ [_75423, _75425] : [-(natural(_75423)), _75425 = _75423, natural(_75425)], (130 ^ _71705) ^ [_75718, _75720] : [-(finite(_75718)), _75720 = _75718, finite(_75720)], (140 ^ _71705) ^ [_76041, _76043, _76045, _76047] : [-(element(_76045, _76041)), element(_76047, _76043), _76047 = _76045, _76043 = _76041], (154 ^ _71705) ^ [_76485, _76487, _76489, _76491] : [-(in(_76489, _76485)), in(_76491, _76487), _76491 = _76489, _76487 = _76485], (168 ^ _71705) ^ [_76901, _76903] : [-(empty(_76901)), _76903 = _76901, empty(_76903)], (178 ^ _71705) ^ [_77204, _77206, _77208, _77210] : [-(subset(_77208, _77204)), subset(_77210, _77206), _77210 = _77208, _77206 = _77204]], input).
% 101.81/98.58 ncf('1',plain,[subset(set_union2(finite_subsets(481 ^ []), finite_subsets(482 ^ [])), finite_subsets(set_union2(481 ^ [], 482 ^ [])))],start(484 ^ 0)).
% 101.81/98.58 ncf('1.1',plain,[-(subset(set_union2(finite_subsets(481 ^ []), finite_subsets(482 ^ [])), finite_subsets(set_union2(481 ^ [], 482 ^ [])))), subset(finite_subsets(481 ^ []), finite_subsets(set_union2(481 ^ [], 482 ^ []))), subset(finite_subsets(482 ^ []), finite_subsets(set_union2(481 ^ [], 482 ^ [])))],extension(472 ^ 1,bind([[_87326, _87328, _87330], [finite_subsets(482 ^ []), finite_subsets(set_union2(481 ^ [], 482 ^ [])), finite_subsets(481 ^ [])]]))).
% 101.81/98.58 ncf('1.1.1',plain,[-(subset(finite_subsets(481 ^ []), finite_subsets(set_union2(481 ^ [], 482 ^ [])))), subset(481 ^ [], set_union2(481 ^ [], 482 ^ []))],extension(400 ^ 2,bind([[_84965, _84967], [set_union2(481 ^ [], 482 ^ []), 481 ^ []]]))).
% 101.81/98.58 ncf('1.1.1.1',plain,[-(subset(481 ^ [], set_union2(481 ^ [], 482 ^ [])))],extension(460 ^ 3,bind([[_86923, _86925], [482 ^ [], 481 ^ []]]))).
% 101.81/98.58 ncf('1.1.2',plain,[-(subset(finite_subsets(482 ^ []), finite_subsets(set_union2(481 ^ [], 482 ^ [])))), subset(482 ^ [], set_union2(481 ^ [], 482 ^ []))],extension(400 ^ 2,bind([[_84965, _84967], [set_union2(481 ^ [], 482 ^ []), 482 ^ []]]))).
% 101.81/98.58 ncf('1.1.2.1',plain,[-(subset(482 ^ [], set_union2(481 ^ [], 482 ^ []))), subset(482 ^ [], set_union2(482 ^ [], 481 ^ [])), 482 ^ [] = 482 ^ [], set_union2(482 ^ [], 481 ^ []) = set_union2(481 ^ [], 482 ^ [])],extension(178 ^ 3,bind([[_77204, _77206, _77208, _77210], [set_union2(481 ^ [], 482 ^ []), set_union2(482 ^ [], 481 ^ []), 482 ^ [], 482 ^ []]]))).
% 101.81/98.58 ncf('1.1.2.1.1',plain,[-(subset(482 ^ [], set_union2(482 ^ [], 481 ^ [])))],extension(460 ^ 4,bind([[_86923, _86925], [481 ^ [], 482 ^ []]]))).
% 101.81/98.58 ncf('1.1.2.1.2',plain,[-(482 ^ [] = 482 ^ [])],extension(2 ^ 4,bind([[_71849], [482 ^ []]]))).
% 101.81/98.58 ncf('1.1.2.1.3',plain,[-(set_union2(482 ^ [], 481 ^ []) = set_union2(481 ^ [], 482 ^ []))],extension(260 ^ 4,bind([[_79930, _79932], [481 ^ [], 482 ^ []]]))).
% 101.81/98.58 %-----------------------------------------------------
% 101.81/98.58 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------