%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU236+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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:49 EDT 2023
% Result : Theorem 62.58s 60.60s
% Output : Proof 62.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU236+1 : TPTP v8.1.2. Released v3.3.0.
% 0.04/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n014.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 18 12:27:12 EDT 2023
% 0.14/0.36 % CPUTime :
% 62.58/60.60
% 62.58/60.60 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 62.58/60.60 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.58/60.60 %-----------------------------------------------------
% 62.58/60.60 ncf(matrix, plain, [(640 ^ _121694) ^ [] : [641 ^ _121694 : [(644 ^ _121694) ^ [] : [ordinal_subset(succ(633 ^ []), 636 ^ [])], (642 ^ _121694) ^ [] : [-(in(633 ^ [], 636 ^ []))]], 645 ^ _121694 : [(648 ^ _121694) ^ [] : [in(633 ^ [], 636 ^ [])], (646 ^ _121694) ^ [] : [-(ordinal_subset(succ(633 ^ []), 636 ^ []))]]], (638 ^ _121694) ^ [] : [-(ordinal(636 ^ []))], (635 ^ _121694) ^ [] : [-(ordinal(633 ^ []))], !, (504 ^ _101671) ^ [] : [-(ordinal(496 ^ []))], (4 ^ _101671) ^ [_101902, _101904] : [_101904 = _101902, -(_101902 = _101904)], (238 ^ _101671) ^ [_109158] : [empty(_109158), 241 ^ _101671 : [(246 ^ _101671) ^ [] : [-(ordinal(_109158))], (244 ^ _101671) ^ [] : [-(epsilon_connected(_109158))], (242 ^ _101671) ^ [] : [-(epsilon_transitive(_109158))]]], (443 ^ _101671) ^ [] : [-(function(439 ^ []))], (436 ^ _101671) ^ [] : [-(relation(empty_set))], (20 ^ _101671) ^ [_102419, _102421] : [-(one_to_one(_102419)), _102421 = _102419, one_to_one(_102421)], (493 ^ _101671) ^ [] : [-(function(489 ^ []))], (488 ^ _101671) ^ [] : [empty(486 ^ [])], (472 ^ _101671) ^ [] : [-(one_to_one(466 ^ []))], (168 ^ _101671) ^ [_107027, _107029, _107031, _107033] : [-(set_union2(_107033, _107029) = set_union2(_107031, _107027)), _107033 = _107031, _107029 = _107027], (376 ^ _101671) ^ [] : [-(relation(empty_set))], (264 ^ _101671) ^ [_109957] : [-(succ(_109957) = set_union2(_109957, singleton(_109957)))], (410 ^ _101671) ^ [_114378, _114380] : [-(empty(_114380)), empty(set_union2(_114380, _114378))], (380 ^ _101671) ^ [_113480] : [empty(succ(_113480))], (483 ^ _101671) ^ [] : [empty(481 ^ [])], (470 ^ _101671) ^ [] : [-(function(466 ^ []))], (474 ^ _101671) ^ [] : [-(empty(466 ^ []))], (384 ^ _101671) ^ [] : [-(relation(empty_set))], (458 ^ _101671) ^ [] : [-(empty(456 ^ []))], (248 ^ _101671) ^ [_109484, _109486] : [-(set_union2(_109486, _109484) = set_union2(_109484, _109486))], (461 ^ _101671) ^ [] : [-(relation(459 ^ []))], (538 ^ _101671) ^ [_118307, _118309] : [-(ordinal_subset(_118309, _118309)), ordinal(_118309), ordinal(_118307)], (178 ^ _101671) ^ [_107338, _107340] : [_107340 = _107338, -(succ(_107340) = succ(_107338))], (455 ^ _101671) ^ [] : [-(relation(451 ^ []))], (441 ^ _101671) ^ [] : [-(relation(439 ^ []))], (204 ^ _101671) ^ [_108210] : [empty(_108210), -(relation(_108210))], (582 ^ _101671) ^ [_119790, _119792, _119794] : [-(element(_119794, _119790)), in(_119794, _119792), element(_119792, powerset(_119790))], (162 ^ _101671) ^ [_106781, _106783] : [_106783 = _106781, -(powerset(_106783) = powerset(_106781))], (297 ^ _101671) ^ [_111172] : [epsilon_transitive(_111172), 300 ^ _101671 : [(301 ^ _101671) ^ [_111303] : [in(_111303, _111172), -(subset(_111303, _111172))]]], (118 ^ _101671) ^ [_105372, _105374] : [-(ordinal(_105372)), _105374 = _105372, ordinal(_105374)], (196 ^ _101671) ^ [_107953] : [ordinal(_107953), 199 ^ _101671 : [(202 ^ _101671) ^ [] : [-(epsilon_connected(_107953))], (200 ^ _101671) ^ [] : [-(epsilon_transitive(_107953))]]], (453 ^ _101671) ^ [] : [-(empty(451 ^ []))], (50 ^ _101671) ^ [_103304, _103306] : [-(relation(_103304)), _103306 = _103304, relation(_103306)], (491 ^ _101671) ^ [] : [-(relation(489 ^ []))], (507 ^ _101671) ^ [] : [-(relation(505 ^ []))], (326 ^ _101671) ^ [_112154, _112156] : [328 ^ _101671 : [(331 ^ _101671) ^ [] : [in(327 ^ [_112154, _112156], _112154)], (329 ^ _101671) ^ [] : [-(in(327 ^ [_112154, _112156], _112156))]], -(subset(_112156, _112154))], (468 ^ _101671) ^ [] : [-(relation(466 ^ []))], (478 ^ _101671) ^ [] : [-(epsilon_connected(466 ^ []))], (398 ^ _101671) ^ [] : [-(ordinal(empty_set))], (335 ^ _101671) ^ [] : [true___, -(true___)], (190 ^ _101671) ^ [_107767] : [empty(_107767), -(function(_107767))], (434 ^ _101671) ^ [] : [-(empty(empty_set))], (428 ^ _101671) ^ [_115008, _115010] : [-(empty(_115010)), empty(set_union2(_115008, _115010))], (518 ^ _101671) ^ [_117760, _117762] : [ordinal(_117762), ordinal(_117760), 525 ^ _101671 : [(532 ^ _101671) ^ [] : [subset(_117762, _117760), -(ordinal_subset(_117762, _117760))], (526 ^ _101671) ^ [] : [ordinal_subset(_117762, _117760), -(subset(_117762, _117760))]]], (512 ^ _101671) ^ [] : [-(relation(510 ^ []))], (624 ^ _101671) ^ [_121113, _121115, _121117] : [-(subset(set_union2(_121117, _121113), _121115)), subset(_121117, _121115), subset(_121113, _121115)], (485 ^ _101671) ^ [] : [-(relation(481 ^ []))], (60 ^ _101671) ^ [_103599, _103601] : [-(relation_empty_yielding(_103599)), _103601 = _103599, relation_empty_yielding(_103601)], (80 ^ _101671) ^ [_104217, _104219, _104221, _104223] : [-(element(_104221, _104217)), element(_104223, _104219), _104223 = _104221, _104219 = _104217], (476 ^ _101671) ^ [] : [-(epsilon_transitive(466 ^ []))], (341 ^ _101671) ^ [] : [true___, -(true___)], (378 ^ _101671) ^ [] : [-(relation_empty_yielding(empty_set))], (480 ^ _101671) ^ [] : [-(ordinal(466 ^ []))], (307 ^ _101671) ^ [_111472] : [309 ^ _101671 : [(312 ^ _101671) ^ [] : [subset(308 ^ [_111472], _111472)], (310 ^ _101671) ^ [] : [-(in(308 ^ [_111472], _111472))]], -(epsilon_transitive(_111472))], (576 ^ _101671) ^ [_119560, _119562] : [subset(_119562, _119560), -(element(_119562, powerset(_119560)))], (548 ^ _101671) ^ [_118587, _118589] : [-(subset(_118589, _118589))], (552 ^ _101671) ^ [_118747] : [-(set_union2(_118747, empty_set) = _118747)], (104 ^ _101671) ^ [_104956, _104958, _104960, _104962] : [-(subset(_104960, _104956)), subset(_104962, _104958), _104962 = _104960, _104958 = _104956], (514 ^ _101671) ^ [] : [-(relation_empty_yielding(510 ^ []))], (614 ^ _101671) ^ [_120822, _120824] : [empty(_120824), -(_120824 = _120822), empty(_120822)], (416 ^ _101671) ^ [_114580] : [ordinal(_114580), 419 ^ _101671 : [(422 ^ _101671) ^ [] : [-(epsilon_transitive(succ(_114580)))], (424 ^ _101671) ^ [] : [-(epsilon_connected(succ(_114580)))], (426 ^ _101671) ^ [] : [-(ordinal(succ(_114580)))], (420 ^ _101671) ^ [] : [empty(succ(_114580))]]], (463 ^ _101671) ^ [] : [-(empty(459 ^ []))], (374 ^ _101671) ^ [] : [-(empty(empty_set))], (10 ^ _101671) ^ [_102106, _102108, _102110] : [-(_102110 = _102106), _102110 = _102108, _102108 = _102106], (382 ^ _101671) ^ [] : [-(empty(empty_set))], (30 ^ _101671) ^ [_102714, _102716] : [-(epsilon_transitive(_102714)), _102716 = _102714, epsilon_transitive(_102716)], (554 ^ _101671) ^ [_118857, _118859] : [in(_118859, _118857), -(element(_118859, _118857))], (608 ^ _101671) ^ [_120615, _120617] : [in(_120617, _120615), empty(_120615)], (316 ^ _101671) ^ [_111840, _111842] : [subset(_111842, _111840), 319 ^ _101671 : [(320 ^ _101671) ^ [_111977] : [in(_111977, _111842), -(in(_111977, _111840))]]], (40 ^ _101671) ^ [_103009, _103011] : [-(epsilon_connected(_103009)), _103011 = _103009, epsilon_connected(_103011)], (353 ^ _101671) ^ [] : [true___, -(true___)], (228 ^ _101671) ^ [_108889] : [-(ordinal(_108889)), epsilon_transitive(_108889), epsilon_connected(_108889)], (500 ^ _101671) ^ [] : [-(epsilon_transitive(496 ^ []))], (128 ^ _101671) ^ [_105695, _105697, _105699, _105701] : [-(in(_105699, _105695)), in(_105701, _105697), _105701 = _105699, _105697 = _105695], (438 ^ _101671) ^ [_115317, _115319] : [-(set_union2(_115319, _115319) = _115319)], (392 ^ _101671) ^ [] : [-(empty(empty_set))], (388 ^ _101671) ^ [] : [-(function(empty_set))], (509 ^ _101671) ^ [] : [-(relation_empty_yielding(505 ^ []))], (394 ^ _101671) ^ [] : [-(epsilon_transitive(empty_set))], (142 ^ _101671) ^ [_106119, _106121, _106123, _106125] : [-(ordinal_subset(_106123, _106119)), ordinal_subset(_106125, _106121), _106125 = _106123, _106121 = _106119], (446 ^ _101671) ^ [] : [-(epsilon_transitive(444 ^ []))], (266 ^ _101671) ^ [_110100, _110102] : [_110100 = singleton(_110102), 269 ^ _101671 : [(276 ^ _101671) ^ [_110442] : [_110442 = _110102, -(in(_110442, _110100))], (270 ^ _101671) ^ [_110270] : [in(_110270, _110100), -(_110270 = _110102)]]], (156 ^ _101671) ^ [_106563, _106565] : [_106565 = _106563, -(singleton(_106565) = singleton(_106563))], (386 ^ _101671) ^ [] : [-(relation_empty_yielding(empty_set))], (365 ^ _101671) ^ [] : [true___, -(true___)], (347 ^ _101671) ^ [] : [true___, -(true___)], (465 ^ _101671) ^ [] : [-(function(459 ^ []))], (210 ^ _101671) ^ [_108396] : [221 ^ _101671 : [(226 ^ _101671) ^ [] : [-(one_to_one(_108396))], (224 ^ _101671) ^ [] : [-(function(_108396))], (222 ^ _101671) ^ [] : [-(relation(_108396))]], relation(_108396), empty(_108396), function(_108396)], (250 ^ _101671) ^ [_109599, _109601] : [ordinal(_109601), ordinal(_109599), -(ordinal_subset(_109601, _109599)), -(ordinal_subset(_109599, _109601))], (570 ^ _101671) ^ [_119394, _119396] : [element(_119396, powerset(_119394)), -(subset(_119396, _119394))], (592 ^ _101671) ^ [_120117, _120119, _120121] : [in(_120121, _120119), element(_120119, powerset(_120117)), empty(_120117)], (502 ^ _101671) ^ [] : [-(epsilon_connected(496 ^ []))], (560 ^ _101671) ^ [_119067, _119069] : [element(_119069, _119067), -(empty(_119067)), -(in(_119069, _119067))], (359 ^ _101671) ^ [] : [true___, -(true___)], (282 ^ _101671) ^ [_110621, _110623] : [-(_110621 = singleton(_110623)), 286 ^ _101671 : [(289 ^ _101671) ^ [] : [283 ^ [_110621, _110623] = _110623], (287 ^ _101671) ^ [] : [-(in(283 ^ [_110621, _110623], _110621))]], 290 ^ _101671 : [(293 ^ _101671) ^ [] : [in(283 ^ [_110621, _110623], _110621)], (291 ^ _101671) ^ [] : [-(283 ^ [_110621, _110623] = _110623)]]], (400 ^ _101671) ^ [_114079, _114081] : [-(relation(set_union2(_114081, _114079))), relation(_114081), relation(_114079)], (372 ^ _101671) ^ [_113235] : [-(element(370 ^ [_113235], _113235))], (94 ^ _101671) ^ [_104633, _104635] : [-(empty(_104633)), _104635 = _104633, empty(_104635)], (495 ^ _101671) ^ [] : [-(one_to_one(489 ^ []))], (516 ^ _101671) ^ [] : [-(function(510 ^ []))], (184 ^ _101671) ^ [_107570, _107572] : [in(_107572, _107570), in(_107570, _107572)], (498 ^ _101671) ^ [] : [empty(496 ^ [])], (602 ^ _101671) ^ [_120413] : [empty(_120413), -(_120413 = empty_set)], (70 ^ _101671) ^ [_103894, _103896] : [-(function(_103894)), _103896 = _103894, function(_103896)], (450 ^ _101671) ^ [] : [-(ordinal(444 ^ []))], (448 ^ _101671) ^ [] : [-(epsilon_connected(444 ^ []))], (2 ^ _101671) ^ [_101795] : [-(_101795 = _101795)], (396 ^ _101671) ^ [] : [-(epsilon_connected(empty_set))], (390 ^ _101671) ^ [] : [-(one_to_one(empty_set))], (550 ^ _101671) ^ [_118667] : [-(in(_118667, succ(_118667)))]], input).
% 62.58/60.60 ncf('1',plain,[642 : -(in(633 ^ [], 636 ^ [])), 646 : -(ordinal_subset(succ(633 ^ []), 636 ^ []))],start(640 ^ 0)).
% 62.58/60.60 ncf('1.1',plain,[in(633 ^ [], 636 ^ []), 301 : -(subset(633 ^ [], 636 ^ [])), 301 : epsilon_transitive(636 ^ [])],extension(297 ^ 3,bind([[_111172, _111303], [636 ^ [], 633 ^ []]]))).
% 62.58/60.60 ncf('1.1.1',plain,[subset(633 ^ [], 636 ^ []), -(subset(set_union2(633 ^ [], singleton(633 ^ [])), 636 ^ [])), subset(singleton(633 ^ []), 636 ^ [])],extension(624 ^ 6,bind([[_121113, _121115, _121117], [singleton(633 ^ []), 636 ^ [], 633 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.1',plain,[subset(set_union2(633 ^ [], singleton(633 ^ [])), 636 ^ []), -(subset(succ(633 ^ []), 636 ^ [])), set_union2(633 ^ [], singleton(633 ^ [])) = succ(633 ^ []), 636 ^ [] = 636 ^ []],extension(104 ^ 7,bind([[_104956, _104958, _104960, _104962], [636 ^ [], 636 ^ [], succ(633 ^ []), set_union2(633 ^ [], singleton(633 ^ []))]]))).
% 62.58/60.60 ncf('1.1.1.1.1',plain,[subset(succ(633 ^ []), 636 ^ []), 532 : -(ordinal_subset(succ(633 ^ []), 636 ^ [])), 532 : ordinal(succ(633 ^ [])), 532 : ordinal(636 ^ [])],extension(518 ^ 8,bind([[_117760, _117762], [636 ^ [], succ(633 ^ [])]]))).
% 62.58/60.60 ncf('1.1.1.1.1.1',plain,[ordinal_subset(succ(633 ^ []), 636 ^ [])],extension(644 ^ 11)).
% 62.58/60.60 ncf('1.1.1.1.1.2',plain,[-(ordinal(succ(633 ^ []))), ordinal(633 ^ [])],extension(416 ^ 9,bind([[_114580], [633 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.1.1.2.1',plain,[-(ordinal(633 ^ []))],extension(635 ^ 10)).
% 62.58/60.60 ncf('1.1.1.1.1.3',plain,[-(ordinal(636 ^ []))],extension(638 ^ 9)).
% 62.58/60.60 ncf('1.1.1.1.2',plain,[-(set_union2(633 ^ [], singleton(633 ^ [])) = succ(633 ^ [])), succ(633 ^ []) = set_union2(633 ^ [], singleton(633 ^ []))],extension(4 ^ 8,bind([[_101902, _101904], [set_union2(633 ^ [], singleton(633 ^ [])), succ(633 ^ [])]]))).
% 62.58/60.60 ncf('1.1.1.1.2.1',plain,[-(succ(633 ^ []) = set_union2(633 ^ [], singleton(633 ^ [])))],extension(264 ^ 9,bind([[_109957], [633 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.1.3',plain,[-(636 ^ [] = 636 ^ []), 636 ^ [] = set_union2(636 ^ [], empty_set), set_union2(636 ^ [], empty_set) = 636 ^ []],extension(10 ^ 8,bind([[_102106, _102108, _102110], [636 ^ [], set_union2(636 ^ [], empty_set), 636 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.1.3.1',plain,[-(636 ^ [] = set_union2(636 ^ [], empty_set)), set_union2(636 ^ [], empty_set) = 636 ^ []],extension(4 ^ 9,bind([[_101902, _101904], [636 ^ [], set_union2(636 ^ [], empty_set)]]))).
% 62.58/60.60 ncf('1.1.1.1.3.1.1',plain,[-(set_union2(636 ^ [], empty_set) = 636 ^ [])],extension(552 ^ 10,bind([[_118747], [636 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.1.3.2',plain,[-(set_union2(636 ^ [], empty_set) = 636 ^ []), 636 ^ [] = set_union2(636 ^ [], empty_set)],extension(4 ^ 9,bind([[_101902, _101904], [set_union2(636 ^ [], empty_set), 636 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.1.3.2.1',plain,[-(636 ^ [] = set_union2(636 ^ [], empty_set))],lemmata('[1, 1, 1, 1].x')).
% 62.58/60.60 ncf('1.1.1.2',plain,[-(subset(singleton(633 ^ []), 636 ^ [])), 331 : in(327 ^ [636 ^ [], singleton(633 ^ [])], 636 ^ [])],extension(326 ^ 7,bind([[_112154, _112156], [636 ^ [], singleton(633 ^ [])]]))).
% 62.58/60.60 ncf('1.1.1.2.1',plain,[-(in(327 ^ [636 ^ [], singleton(633 ^ [])], 636 ^ [])), in(633 ^ [], 636 ^ []), 633 ^ [] = 327 ^ [636 ^ [], singleton(633 ^ [])], 636 ^ [] = 636 ^ []],extension(128 ^ 10,bind([[_105695, _105697, _105699, _105701], [636 ^ [], 636 ^ [], 327 ^ [636 ^ [], singleton(633 ^ [])], 633 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.2.1.1',plain,[-(in(633 ^ [], 636 ^ []))],reduction('1')).
% 62.58/60.60 ncf('1.1.1.2.1.2',plain,[-(633 ^ [] = 327 ^ [636 ^ [], singleton(633 ^ [])]), 327 ^ [636 ^ [], singleton(633 ^ [])] = 633 ^ []],extension(4 ^ 11,bind([[_101902, _101904], [633 ^ [], 327 ^ [636 ^ [], singleton(633 ^ [])]]]))).
% 62.58/60.60 ncf('1.1.1.2.1.2.1',plain,[-(327 ^ [636 ^ [], singleton(633 ^ [])] = 633 ^ []), 270 : in(327 ^ [636 ^ [], singleton(633 ^ [])], singleton(633 ^ [])), 270 : singleton(633 ^ []) = singleton(633 ^ [])],extension(266 ^ 12,bind([[_110100, _110102, _110270], [singleton(633 ^ []), 633 ^ [], 327 ^ [636 ^ [], singleton(633 ^ [])]]]))).
% 62.58/60.60 ncf('1.1.1.2.1.2.1.1',plain,[-(in(327 ^ [636 ^ [], singleton(633 ^ [])], singleton(633 ^ [])))],extension(329 ^ 15)).
% 62.58/60.60 ncf('1.1.1.2.1.2.1.2',plain,[-(singleton(633 ^ []) = singleton(633 ^ []))],extension(2 ^ 13,bind([[_101795], [singleton(633 ^ [])]]))).
% 62.58/60.60 ncf('1.1.1.2.1.3',plain,[-(636 ^ [] = 636 ^ []), 636 ^ [] = set_union2(636 ^ [], empty_set), set_union2(636 ^ [], empty_set) = 636 ^ []],extension(10 ^ 11,bind([[_102106, _102108, _102110], [636 ^ [], set_union2(636 ^ [], empty_set), 636 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.2.1.3.1',plain,[-(636 ^ [] = set_union2(636 ^ [], empty_set)), set_union2(636 ^ [], empty_set) = 636 ^ []],extension(4 ^ 12,bind([[_101902, _101904], [636 ^ [], set_union2(636 ^ [], empty_set)]]))).
% 62.58/60.60 ncf('1.1.1.2.1.3.1.1',plain,[-(set_union2(636 ^ [], empty_set) = 636 ^ [])],extension(552 ^ 13,bind([[_118747], [636 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.2.1.3.2',plain,[-(set_union2(636 ^ [], empty_set) = 636 ^ []), 636 ^ [] = set_union2(636 ^ [], empty_set)],extension(4 ^ 12,bind([[_101902, _101904], [set_union2(636 ^ [], empty_set), 636 ^ []]]))).
% 62.58/60.60 ncf('1.1.1.2.1.3.2.1',plain,[-(636 ^ [] = set_union2(636 ^ [], empty_set))],lemmata('[1, 2, 1, 1, 1].x')).
% 62.58/60.60 ncf('1.1.2',plain,[-(epsilon_transitive(636 ^ [])), ordinal(636 ^ [])],extension(196 ^ 4,bind([[_107953], [636 ^ []]]))).
% 62.58/60.60 ncf('1.1.2.1',plain,[-(ordinal(636 ^ []))],extension(638 ^ 5)).
% 62.58/60.60 ncf('1.2',plain,[ordinal_subset(succ(633 ^ []), 636 ^ []), 526 : -(subset(succ(633 ^ []), 636 ^ [])), 526 : ordinal(succ(633 ^ [])), 526 : ordinal(636 ^ [])],extension(518 ^ 3,bind([[_117760, _117762], [636 ^ [], succ(633 ^ [])]]))).
% 62.58/60.60 ncf('1.2.1',plain,[subset(succ(633 ^ []), 636 ^ []), -(subset(set_union2(succ(633 ^ []), succ(633 ^ [])), 636 ^ [])), subset(succ(633 ^ []), 636 ^ [])],extension(624 ^ 6,bind([[_121113, _121115, _121117], [succ(633 ^ []), 636 ^ [], succ(633 ^ [])]]))).
% 62.58/60.60 ncf('1.2.1.1',plain,[subset(set_union2(succ(633 ^ []), succ(633 ^ [])), 636 ^ []), -(element(set_union2(succ(633 ^ []), succ(633 ^ [])), powerset(636 ^ [])))],extension(576 ^ 7,bind([[_119560, _119562], [636 ^ [], set_union2(succ(633 ^ []), succ(633 ^ []))]]))).
% 62.58/60.60 ncf('1.2.1.1.1',plain,[element(set_union2(succ(633 ^ []), succ(633 ^ [])), powerset(636 ^ [])), in(370 ^ [set_union2(succ(633 ^ []), succ(633 ^ []))], set_union2(succ(633 ^ []), succ(633 ^ []))), empty(636 ^ [])],extension(592 ^ 8,bind([[_120117, _120119, _120121], [636 ^ [], set_union2(succ(633 ^ []), succ(633 ^ [])), 370 ^ [set_union2(succ(633 ^ []), succ(633 ^ []))]]]))).
% 62.58/60.60 ncf('1.2.1.1.1.1',plain,[-(in(370 ^ [set_union2(succ(633 ^ []), succ(633 ^ []))], set_union2(succ(633 ^ []), succ(633 ^ [])))), element(370 ^ [set_union2(succ(633 ^ []), succ(633 ^ []))], set_union2(succ(633 ^ []), succ(633 ^ []))), -(empty(set_union2(succ(633 ^ []), succ(633 ^ []))))],extension(560 ^ 9,bind([[_119067, _119069], [set_union2(succ(633 ^ []), succ(633 ^ [])), 370 ^ [set_union2(succ(633 ^ []), succ(633 ^ []))]]]))).
% 62.58/60.60 ncf('1.2.1.1.1.1.1',plain,[-(element(370 ^ [set_union2(succ(633 ^ []), succ(633 ^ []))], set_union2(succ(633 ^ []), succ(633 ^ []))))],extension(372 ^ 10,bind([[_113235], [set_union2(succ(633 ^ []), succ(633 ^ []))]]))).
% 62.58/60.60 ncf('1.2.1.1.1.1.2',plain,[empty(set_union2(succ(633 ^ []), succ(633 ^ []))), -(empty(succ(633 ^ [])))],extension(410 ^ 10,bind([[_114378, _114380], [succ(633 ^ []), succ(633 ^ [])]]))).
% 62.58/60.60 ncf('1.2.1.1.1.1.2.1',plain,[empty(succ(633 ^ []))],extension(380 ^ 11,bind([[_113480], [633 ^ []]]))).
% 62.58/60.60 ncf('1.2.1.1.1.2',plain,[-(empty(636 ^ [])), element(633 ^ [], 636 ^ []), -(in(633 ^ [], 636 ^ []))],extension(560 ^ 9,bind([[_119067, _119069], [636 ^ [], 633 ^ []]]))).
% 62.58/60.60 ncf('1.2.1.1.1.2.1',plain,[-(element(633 ^ [], 636 ^ [])), in(633 ^ [], succ(633 ^ [])), element(succ(633 ^ []), powerset(636 ^ []))],extension(582 ^ 10,bind([[_119790, _119792, _119794], [636 ^ [], succ(633 ^ []), 633 ^ []]]))).
% 62.58/60.60 ncf('1.2.1.1.1.2.1.1',plain,[-(in(633 ^ [], succ(633 ^ [])))],extension(550 ^ 11,bind([[_118667], [633 ^ []]]))).
% 62.58/60.60 ncf('1.2.1.1.1.2.1.2',plain,[-(element(succ(633 ^ []), powerset(636 ^ []))), subset(succ(633 ^ []), 636 ^ [])],extension(576 ^ 11,bind([[_119560, _119562], [636 ^ [], succ(633 ^ [])]]))).
% 62.58/60.60 ncf('1.2.1.1.1.2.1.2.1',plain,[-(subset(succ(633 ^ []), 636 ^ []))],reduction('1.2')).
% 62.58/60.60 ncf('1.2.1.1.1.2.2',plain,[in(633 ^ [], 636 ^ [])],extension(648 ^ 10)).
% 62.58/60.60 ncf('1.2.1.2',plain,[-(subset(succ(633 ^ []), 636 ^ []))],reduction('1.2')).
% 62.58/60.60 ncf('1.2.2',plain,[-(ordinal(succ(633 ^ []))), ordinal(633 ^ [])],extension(416 ^ 4,bind([[_114580], [633 ^ []]]))).
% 62.58/60.60 ncf('1.2.2.1',plain,[-(ordinal(633 ^ []))],extension(635 ^ 5)).
% 62.58/60.60 ncf('1.2.3',plain,[-(ordinal(636 ^ []))],extension(638 ^ 4)).
% 62.58/60.60 %-----------------------------------------------------
% 62.58/60.60 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------