%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU234+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:48 EDT 2023
% Result : Theorem 0.61s 1.38s
% Output : Proof 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU234+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n028.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:25:48 EDT 2023
% 0.14/0.34 % CPUTime :
% 0.61/1.38
% 0.61/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.61/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/1.38 %-----------------------------------------------------
% 0.61/1.38 ncf(matrix, plain, [(513 ^ _65610) ^ [] : [ordinal(503 ^ [])], (505 ^ _65610) ^ [_81472] : [in(_81472, 503 ^ []), 508 ^ _65610 : [(509 ^ _65610) ^ [] : [-(ordinal(_81472))], (511 ^ _65610) ^ [] : [-(subset(_81472, 503 ^ []))]]], (142 ^ _65610) ^ [_70056, _70058] : [_70058 = _70056, -(powerset(_70058) = powerset(_70056))], (2 ^ _65610) ^ [_65754] : [-(_65754 = _65754)], (4 ^ _65610) ^ [_65861, _65863] : [_65863 = _65861, -(_65861 = _65863)], (10 ^ _65610) ^ [_66065, _66067, _66069] : [-(_66069 = _66065), _66069 = _66067, _66067 = _66065], (20 ^ _65610) ^ [_66378, _66380] : [-(one_to_one(_66378)), _66380 = _66378, one_to_one(_66380)], (30 ^ _65610) ^ [_66673, _66675] : [-(epsilon_transitive(_66673)), _66675 = _66673, epsilon_transitive(_66675)], (40 ^ _65610) ^ [_66968, _66970] : [-(epsilon_connected(_66968)), _66970 = _66968, epsilon_connected(_66970)], (50 ^ _65610) ^ [_67263, _67265] : [-(relation(_67263)), _67265 = _67263, relation(_67265)], (60 ^ _65610) ^ [_67558, _67560] : [-(relation_empty_yielding(_67558)), _67560 = _67558, relation_empty_yielding(_67560)], (70 ^ _65610) ^ [_67853, _67855] : [-(function(_67853)), _67855 = _67853, function(_67855)], (80 ^ _65610) ^ [_68176, _68178, _68180, _68182] : [-(element(_68180, _68176)), element(_68182, _68178), _68182 = _68180, _68178 = _68176], (94 ^ _65610) ^ [_68592, _68594] : [-(empty(_68592)), _68594 = _68592, empty(_68594)], (104 ^ _65610) ^ [_68915, _68917, _68919, _68921] : [-(in(_68919, _68915)), in(_68921, _68917), _68921 = _68919, _68917 = _68915], (132 ^ _65610) ^ [_69755, _69757] : [-(ordinal(_69755)), _69757 = _69755, ordinal(_69757)], (118 ^ _65610) ^ [_69359, _69361, _69363, _69365] : [-(subset(_69363, _69359)), subset(_69365, _69361), _69365 = _69363, _69361 = _69359], (148 ^ _65610) ^ [_70276, _70278] : [in(_70278, _70276), in(_70276, _70278)], (154 ^ _65610) ^ [_70473] : [empty(_70473), -(function(_70473))], (160 ^ _65610) ^ [_70659] : [ordinal(_70659), 163 ^ _65610 : [(164 ^ _65610) ^ [] : [-(epsilon_transitive(_70659))], (166 ^ _65610) ^ [] : [-(epsilon_connected(_70659))]]], (168 ^ _65610) ^ [_70916] : [empty(_70916), -(relation(_70916))], (174 ^ _65610) ^ [_71102] : [185 ^ _65610 : [(186 ^ _65610) ^ [] : [-(relation(_71102))], (188 ^ _65610) ^ [] : [-(function(_71102))], (190 ^ _65610) ^ [] : [-(one_to_one(_71102))]], relation(_71102), empty(_71102), function(_71102)], (192 ^ _65610) ^ [_71595] : [-(ordinal(_71595)), epsilon_transitive(_71595), epsilon_connected(_71595)], (202 ^ _65610) ^ [_71864] : [empty(_71864), 205 ^ _65610 : [(206 ^ _65610) ^ [] : [-(epsilon_transitive(_71864))], (208 ^ _65610) ^ [] : [-(epsilon_connected(_71864))], (210 ^ _65610) ^ [] : [-(ordinal(_71864))]]], (222 ^ _65610) ^ [_72520] : [224 ^ _65610 : [(225 ^ _65610) ^ [] : [-(in(223 ^ [_72520], _72520))], (227 ^ _65610) ^ [] : [subset(223 ^ [_72520], _72520)]], -(epsilon_transitive(_72520))], (212 ^ _65610) ^ [_72220] : [epsilon_transitive(_72220), 215 ^ _65610 : [(216 ^ _65610) ^ [_72351] : [in(_72351, _72220), -(subset(_72351, _72220))]]], (253 ^ _65610) ^ [_73512] : [256 ^ _65610 : [(257 ^ _65610) ^ [] : [-(in(254 ^ [_73512], _73512))], (259 ^ _65610) ^ [] : [-(in(255 ^ [_73512], _73512))], (261 ^ _65610) ^ [] : [in(254 ^ [_73512], 255 ^ [_73512])], (263 ^ _65610) ^ [] : [254 ^ [_73512] = 255 ^ [_73512]], (265 ^ _65610) ^ [] : [in(255 ^ [_73512], 254 ^ [_73512])]], -(epsilon_connected(_73512))], (231 ^ _65610) ^ [_72874] : [epsilon_connected(_72874), 234 ^ _65610 : [(235 ^ _65610) ^ [_73050, _73052] : [in(_73052, _72874), in(_73050, _72874), -(in(_73052, _73050)), -(_73052 = _73050), -(in(_73050, _73052))]]], (269 ^ _65610) ^ [_74247] : [ordinal(_74247), 272 ^ _65610 : [(273 ^ _65610) ^ [] : [-(epsilon_transitive(_74247))], (275 ^ _65610) ^ [] : [-(epsilon_connected(_74247))]]], (277 ^ _65610) ^ [_74470] : [-(ordinal(_74470)), epsilon_transitive(_74470), epsilon_connected(_74470)], (287 ^ _65610) ^ [] : [true___, -(true___)], (293 ^ _65610) ^ [] : [true___, -(true___)], (299 ^ _65610) ^ [] : [true___, -(true___)], (306 ^ _65610) ^ [_75122] : [-(element(304 ^ [_75122], _75122))], (308 ^ _65610) ^ [] : [-(empty(empty_set))], (310 ^ _65610) ^ [] : [-(relation(empty_set))], (312 ^ _65610) ^ [] : [-(relation_empty_yielding(empty_set))], (314 ^ _65610) ^ [] : [-(empty(empty_set))], (316 ^ _65610) ^ [] : [-(relation(empty_set))], (318 ^ _65610) ^ [] : [-(relation_empty_yielding(empty_set))], (320 ^ _65610) ^ [] : [-(function(empty_set))], (322 ^ _65610) ^ [] : [-(one_to_one(empty_set))], (324 ^ _65610) ^ [] : [-(empty(empty_set))], (326 ^ _65610) ^ [] : [-(epsilon_transitive(empty_set))], (328 ^ _65610) ^ [] : [-(epsilon_connected(empty_set))], (330 ^ _65610) ^ [] : [-(ordinal(empty_set))], (332 ^ _65610) ^ [] : [-(empty(empty_set))], (334 ^ _65610) ^ [] : [-(relation(empty_set))], (337 ^ _65610) ^ [] : [-(relation(335 ^ []))], (339 ^ _65610) ^ [] : [-(function(335 ^ []))], (342 ^ _65610) ^ [] : [-(epsilon_transitive(340 ^ []))], (344 ^ _65610) ^ [] : [-(epsilon_connected(340 ^ []))], (346 ^ _65610) ^ [] : [-(ordinal(340 ^ []))], (349 ^ _65610) ^ [] : [-(empty(347 ^ []))], (351 ^ _65610) ^ [] : [-(relation(347 ^ []))], (354 ^ _65610) ^ [] : [-(empty(352 ^ []))], (357 ^ _65610) ^ [] : [-(relation(355 ^ []))], (359 ^ _65610) ^ [] : [-(empty(355 ^ []))], (361 ^ _65610) ^ [] : [-(function(355 ^ []))], (364 ^ _65610) ^ [] : [-(relation(362 ^ []))], (366 ^ _65610) ^ [] : [-(function(362 ^ []))], (368 ^ _65610) ^ [] : [-(one_to_one(362 ^ []))], (370 ^ _65610) ^ [] : [-(empty(362 ^ []))], (372 ^ _65610) ^ [] : [-(epsilon_transitive(362 ^ []))], (374 ^ _65610) ^ [] : [-(epsilon_connected(362 ^ []))], (376 ^ _65610) ^ [] : [-(ordinal(362 ^ []))], (379 ^ _65610) ^ [] : [empty(377 ^ [])], (381 ^ _65610) ^ [] : [-(relation(377 ^ []))], (384 ^ _65610) ^ [] : [empty(382 ^ [])], (387 ^ _65610) ^ [] : [-(relation(385 ^ []))], (389 ^ _65610) ^ [] : [-(function(385 ^ []))], (391 ^ _65610) ^ [] : [-(one_to_one(385 ^ []))], (394 ^ _65610) ^ [] : [empty(392 ^ [])], (396 ^ _65610) ^ [] : [-(epsilon_transitive(392 ^ []))], (398 ^ _65610) ^ [] : [-(epsilon_connected(392 ^ []))], (400 ^ _65610) ^ [] : [-(ordinal(392 ^ []))], (403 ^ _65610) ^ [] : [-(relation(401 ^ []))], (405 ^ _65610) ^ [] : [-(relation_empty_yielding(401 ^ []))], (408 ^ _65610) ^ [] : [-(relation(406 ^ []))], (410 ^ _65610) ^ [] : [-(relation_empty_yielding(406 ^ []))], (412 ^ _65610) ^ [] : [-(function(406 ^ []))], (414 ^ _65610) ^ [_78312, _78314] : [-(subset(_78314, _78314))], (416 ^ _65610) ^ [_78421, _78423] : [in(_78423, _78421), -(element(_78423, _78421))], (422 ^ _65610) ^ [_78617] : [ordinal(_78617), 425 ^ _65610 : [(426 ^ _65610) ^ [_78767] : [ordinal(_78767), -(in(_78617, _78767)), -(_78617 = _78767), -(in(_78767, _78617))]]], (440 ^ _65610) ^ [_79170, _79172] : [element(_79172, _79170), -(empty(_79170)), -(in(_79172, _79170))], (450 ^ _65610) ^ [_79497, _79499] : [element(_79499, powerset(_79497)), -(subset(_79499, _79497))], (456 ^ _65610) ^ [_79663, _79665] : [subset(_79665, _79663), -(element(_79665, powerset(_79663)))], (462 ^ _65610) ^ [_79893, _79895, _79897] : [-(element(_79897, _79893)), in(_79897, _79895), element(_79895, powerset(_79893))], (472 ^ _65610) ^ [_80220, _80222, _80224] : [in(_80224, _80222), element(_80222, powerset(_80220)), empty(_80220)], (482 ^ _65610) ^ [_80516] : [empty(_80516), -(_80516 = empty_set)], (488 ^ _65610) ^ [_80718, _80720] : [in(_80720, _80718), empty(_80718)], (494 ^ _65610) ^ [_80905, _80907] : [empty(_80907), -(_80907 = _80905), empty(_80905)]], input).
% 0.61/1.38 ncf('1',plain,[ordinal(503 ^ [])],start(513 ^ 0)).
% 0.61/1.38 ncf('1.1',plain,[-(ordinal(503 ^ [])), epsilon_transitive(503 ^ []), epsilon_connected(503 ^ [])],extension(192 ^ 1,bind([[_71595], [503 ^ []]]))).
% 0.61/1.38 ncf('1.1.1',plain,[-(epsilon_transitive(503 ^ [])), 225 : -(in(223 ^ [503 ^ []], 503 ^ []))],extension(222 ^ 2,bind([[_72520], [503 ^ []]]))).
% 0.61/1.38 ncf('1.1.1.1',plain,[in(223 ^ [503 ^ []], 503 ^ []), 511 : -(subset(223 ^ [503 ^ []], 503 ^ []))],extension(505 ^ 5,bind([[_81472], [223 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.1.1.1',plain,[subset(223 ^ [503 ^ []], 503 ^ []), -(subset(223 ^ [503 ^ []], 503 ^ [])), 223 ^ [503 ^ []] = 223 ^ [503 ^ []], 503 ^ [] = 503 ^ []],extension(118 ^ 8,bind([[_69359, _69361, _69363, _69365], [503 ^ [], 503 ^ [], 223 ^ [503 ^ []], 223 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.1.1.1.1',plain,[subset(223 ^ [503 ^ []], 503 ^ [])],extension(227 ^ 9)).
% 0.61/1.38 ncf('1.1.1.1.1.2',plain,[-(223 ^ [503 ^ []] = 223 ^ [503 ^ []])],extension(2 ^ 9,bind([[_65754], [223 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.1.1.1.3',plain,[-(503 ^ [] = 503 ^ [])],extension(2 ^ 9,bind([[_65754], [503 ^ []]]))).
% 0.61/1.38 ncf('1.1.2',plain,[-(epsilon_connected(503 ^ [])), 261 : in(254 ^ [503 ^ []], 255 ^ [503 ^ []])],extension(253 ^ 2,bind([[_73512], [503 ^ []]]))).
% 0.61/1.38 ncf('1.1.2.1',plain,[-(in(254 ^ [503 ^ []], 255 ^ [503 ^ []])), 426 : ordinal(255 ^ [503 ^ []]), 426 : -(254 ^ [503 ^ []] = 255 ^ [503 ^ []]), 426 : -(in(255 ^ [503 ^ []], 254 ^ [503 ^ []])), 426 : ordinal(254 ^ [503 ^ []])],extension(422 ^ 5,bind([[_78617, _78767], [254 ^ [503 ^ []], 255 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.2.1.1',plain,[-(ordinal(255 ^ [503 ^ []])), in(255 ^ [503 ^ []], 503 ^ [])],extension(505 ^ 8,bind([[_81472], [255 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.2.1.1.1',plain,[-(in(255 ^ [503 ^ []], 503 ^ []))],extension(259 ^ 9)).
% 0.61/1.38 ncf('1.1.2.1.2',plain,[254 ^ [503 ^ []] = 255 ^ [503 ^ []], -(254 ^ [503 ^ []] = 255 ^ [503 ^ []]), 255 ^ [503 ^ []] = 255 ^ [503 ^ []]],extension(10 ^ 8,bind([[_66065, _66067, _66069], [255 ^ [503 ^ []], 255 ^ [503 ^ []], 254 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.2.1.2.1',plain,[254 ^ [503 ^ []] = 255 ^ [503 ^ []]],extension(263 ^ 9)).
% 0.61/1.38 ncf('1.1.2.1.2.2',plain,[-(255 ^ [503 ^ []] = 255 ^ [503 ^ []])],extension(2 ^ 9,bind([[_65754], [255 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.2.1.3',plain,[in(255 ^ [503 ^ []], 254 ^ [503 ^ []])],extension(265 ^ 8)).
% 0.61/1.38 ncf('1.1.2.1.4',plain,[-(ordinal(254 ^ [503 ^ []])), in(254 ^ [503 ^ []], 503 ^ [])],extension(505 ^ 6,bind([[_81472], [254 ^ [503 ^ []]]]))).
% 0.61/1.38 ncf('1.1.2.1.4.1',plain,[-(in(254 ^ [503 ^ []], 503 ^ []))],extension(257 ^ 7)).
% 0.61/1.38 %-----------------------------------------------------
% 0.61/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------