%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU308+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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:05 EDT 2023
% Result : Theorem 49.35s 48.13s
% Output : Proof 49.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU308+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 13:00:35 EDT 2023
% 0.12/0.34 % CPUTime :
% 49.35/48.13
% 49.35/48.13 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 49.35/48.13 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.35/48.13 %-----------------------------------------------------
% 49.35/48.13 ncf(matrix, plain, [(683 ^ _131695) ^ [] : [subset_complement(the_carrier(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ [])], (681 ^ _131695) ^ [] : [-(element(679 ^ [], powerset(the_carrier(676 ^ []))))], (678 ^ _131695) ^ [] : [-(one_sorted_str(676 ^ []))], !, (273 ^ _109215) ^ [] : [-(v1_membered(269 ^ []))], (4 ^ _109215) ^ [_109446, _109448] : [_109448 = _109446, -(_109446 = _109448)], (283 ^ _109215) ^ [_118221] : [v1_membered(_118221), 286 ^ _109215 : [(287 ^ _109215) ^ [_118351] : [element(_118351, _118221), -(v1_xcmplx_0(_118351))]]], (359 ^ _109215) ^ [] : [-(v3_membered(empty_set))], (277 ^ _109215) ^ [] : [-(v3_membered(269 ^ []))], (485 ^ _109215) ^ [_125295, _125297] : [in(_125297, _125295), -(element(_125297, _125295))], (168 ^ _109215) ^ [_114399, _114401, _114403, _114405] : [-(element(_114403, _114399)), element(_114405, _114401), _114405 = _114403, _114401 = _114399], (357 ^ _109215) ^ [] : [-(v2_membered(empty_set))], (264 ^ _109215) ^ [_117645] : [v2_membered(_117645), -(v1_membered(_117645))], (10 ^ _109215) ^ [_109650, _109652, _109654] : [-(_109654 = _109650), _109654 = _109652, _109652 = _109650], (495 ^ _109215) ^ [_125681, _125683, _125685] : [-(element(_125685, _125681)), in(_125685, _125683), element(_125683, powerset(_125681))], (441 ^ _109215) ^ [_123663, _123665] : [v2_membered(_123665), 444 ^ _109215 : [(447 ^ _109215) ^ [] : [-(v2_membered(set_difference(_123665, _123663)))], (445 ^ _109215) ^ [] : [-(v1_membered(set_difference(_123665, _123663)))]]], (182 ^ _109215) ^ [_114877, _114879, _114881, _114883] : [-(set_difference(_114883, _114879) = set_difference(_114881, _114877)), _114883 = _114881, _114879 = _114877], (363 ^ _109215) ^ [] : [-(v5_membered(empty_set))], (387 ^ _109215) ^ [_121730] : [v3_membered(_121730), 390 ^ _109215 : [(391 ^ _109215) ^ [_121872] : [element(_121872, powerset(_121730)), 394 ^ _109215 : [(399 ^ _109215) ^ [] : [-(v3_membered(_121872))], (397 ^ _109215) ^ [] : [-(v2_membered(_121872))], (395 ^ _109215) ^ [] : [-(v1_membered(_121872))]]]]], (589 ^ _109215) ^ [_128853, _128855, _128857] : [-(subset_difference(_128857, _128855, _128853) = set_difference(_128855, _128853)), element(_128855, powerset(_128857)), element(_128853, powerset(_128857))], (208 ^ _109215) ^ [_115841, _115843, _115845, _115847, _115849, _115851] : [-(subset_difference(_115851, _115847, _115843) = subset_difference(_115849, _115845, _115841)), _115851 = _115849, _115847 = _115845, _115843 = _115841], (639 ^ _109215) ^ [] : [true___, -(true___)], (355 ^ _109215) ^ [] : [-(v1_membered(empty_set))], (527 ^ _109215) ^ [_126781] : [-(element(525 ^ [_126781], powerset(_126781)))], (517 ^ _109215) ^ [_126398] : [-(empty(_126398)), 521 ^ _109215 : [(524 ^ _109215) ^ [] : [empty(520 ^ [_126398])], (522 ^ _109215) ^ [] : [-(element(520 ^ [_126398], powerset(_126398)))]]], (584 ^ _109215) ^ [] : [-(one_sorted_str(582 ^ []))], (577 ^ _109215) ^ [_128402, _128404] : [element(_128402, powerset(_128404)), -(subset_complement(_128404, subset_complement(_128404, _128402)) = _128402)], (353 ^ _109215) ^ [] : [-(empty(empty_set))], (228 ^ _109215) ^ [_116499, _116501] : [_116501 = _116499, -(cast_as_carrier_subset(_116501) = cast_as_carrier_subset(_116499))], (611 ^ _109215) ^ [_129503, _129505] : [element(_129503, powerset(_129505)), -(element(subset_complement(_129505, _129503), powerset(_129505)))], (281 ^ _109215) ^ [] : [-(v5_membered(269 ^ []))], (617 ^ _109215) ^ [] : [true___, -(true___)], (417 ^ _109215) ^ [_122791] : [v5_membered(_122791), 420 ^ _109215 : [(421 ^ _109215) ^ [_122943] : [element(_122943, powerset(_122791)), 424 ^ _109215 : [(425 ^ _109215) ^ [] : [-(v1_membered(_122943))], (429 ^ _109215) ^ [] : [-(v3_membered(_122943))], (433 ^ _109215) ^ [] : [-(v5_membered(_122943))], (431 ^ _109215) ^ [] : [-(v4_membered(_122943))], (427 ^ _109215) ^ [] : [-(v2_membered(_122943))]]]]], (493 ^ _109215) ^ [_125557] : [-(set_difference(empty_set, _125557) = empty_set)], (561 ^ _109215) ^ [_127898, _127900] : [in(_127900, _127898), empty(_127898)], (2 ^ _109215) ^ [_109339] : [-(_109339 = _109339)], (120 ^ _109215) ^ [_112941, _112943, _112945, _112947] : [-(in(_112945, _112941)), in(_112947, _112943), _112947 = _112945, _112943 = _112941], (305 ^ _109215) ^ [_118961] : [v3_membered(_118961), 308 ^ _109215 : [(309 ^ _109215) ^ [_119101] : [element(_119101, _118961), 312 ^ _109215 : [(317 ^ _109215) ^ [] : [-(v1_rat_1(_119101))], (315 ^ _109215) ^ [] : [-(v1_xreal_0(_119101))], (313 ^ _109215) ^ [] : [-(v1_xcmplx_0(_119101))]]]]], (645 ^ _109215) ^ [] : [true___, -(true___)], (271 ^ _109215) ^ [] : [empty(269 ^ [])], (258 ^ _109215) ^ [_117459] : [v3_membered(_117459), -(v2_membered(_117459))], (335 ^ _109215) ^ [_120010] : [v5_membered(_120010), 338 ^ _109215 : [(339 ^ _109215) ^ [_120160] : [element(_120160, _120010), 342 ^ _109215 : [(343 ^ _109215) ^ [] : [-(v1_xcmplx_0(_120160))], (347 ^ _109215) ^ [] : [-(v1_xreal_0(_120160))], (351 ^ _109215) ^ [] : [-(v1_rat_1(_120160))], (349 ^ _109215) ^ [] : [-(v1_int_1(_120160))], (345 ^ _109215) ^ [] : [-(natural(_120160))]]]]], (599 ^ _109215) ^ [] : [true___, -(true___)], (279 ^ _109215) ^ [] : [-(v4_membered(269 ^ []))], (529 ^ _109215) ^ [_126832] : [-(empty(525 ^ [_126832]))], (449 ^ _109215) ^ [_123954, _123956] : [v3_membered(_123956), 452 ^ _109215 : [(457 ^ _109215) ^ [] : [-(v3_membered(set_difference(_123956, _123954)))], (455 ^ _109215) ^ [] : [-(v2_membered(set_difference(_123956, _123954)))], (453 ^ _109215) ^ [] : [-(v1_membered(set_difference(_123956, _123954)))]]], (144 ^ _109215) ^ [_113680, _113682, _113684, _113686] : [-(subset(_113684, _113680)), subset(_113686, _113682), _113686 = _113684, _113682 = _113680], (545 ^ _109215) ^ [_127412, _127414] : [element(_127414, _127412), -(empty(_127412)), -(in(_127414, _127412))], (633 ^ _109215) ^ [] : [true___, -(true___)], (246 ^ _109215) ^ [_117087] : [v5_membered(_117087), -(v4_membered(_117087))], (70 ^ _109215) ^ [_111438, _111440] : [-(v1_membered(_111438)), _111440 = _111438, v1_membered(_111440)], (134 ^ _109215) ^ [_113357, _113359] : [-(empty(_113357)), _113359 = _113357, empty(_113359)], (319 ^ _109215) ^ [_119447] : [v4_membered(_119447), 322 ^ _109215 : [(323 ^ _109215) ^ [_119592] : [element(_119592, _119447), 326 ^ _109215 : [(329 ^ _109215) ^ [] : [-(v1_xreal_0(_119592))], (331 ^ _109215) ^ [] : [-(v1_int_1(_119592))], (333 ^ _109215) ^ [] : [-(v1_rat_1(_119592))], (327 ^ _109215) ^ [] : [-(v1_xcmplx_0(_119592))]]]]], (401 ^ _109215) ^ [_122222] : [v4_membered(_122222), 404 ^ _109215 : [(405 ^ _109215) ^ [_122369] : [element(_122369, powerset(_122222)), 408 ^ _109215 : [(411 ^ _109215) ^ [] : [-(v2_membered(_122369))], (413 ^ _109215) ^ [] : [-(v3_membered(_122369))], (415 ^ _109215) ^ [] : [-(v4_membered(_122369))], (409 ^ _109215) ^ [] : [-(v1_membered(_122369))]]]]], (435 ^ _109215) ^ [_123451, _123453] : [v1_membered(_123453), -(v1_membered(set_difference(_123453, _123451)))], (555 ^ _109215) ^ [_127696] : [empty(_127696), -(_127696 = empty_set)], (505 ^ _109215) ^ [_126008, _126010, _126012] : [in(_126012, _126010), element(_126010, powerset(_126008)), empty(_126008)], (158 ^ _109215) ^ [_114096, _114098] : [-(one_sorted_str(_114096)), _114098 = _114096, one_sorted_str(_114098)], (40 ^ _109215) ^ [_110553, _110555] : [-(v1_xreal_0(_110553)), _110555 = _110553, v1_xreal_0(_110555)], (30 ^ _109215) ^ [_110258, _110260] : [-(natural(_110258)), _110260 = _110258, natural(_110260)], (100 ^ _109215) ^ [_112323, _112325] : [-(v4_membered(_112323)), _112325 = _112323, v4_membered(_112325)], (659 ^ _109215) ^ [_130819, _130821] : [subset(_130821, _130819), -(element(_130821, powerset(_130819)))], (80 ^ _109215) ^ [_111733, _111735] : [-(v2_membered(_111733)), _111735 = _111733, v2_membered(_111735)], (587 ^ _109215) ^ [_128727] : [-(element(585 ^ [_128727], _128727))], (240 ^ _109215) ^ [] : [true___, -(true___)], (567 ^ _109215) ^ [_128105, _128107] : [empty(_128107), -(_128107 = _128105), empty(_128105)], (222 ^ _109215) ^ [_116301, _116303] : [_116303 = _116301, -(the_carrier(_116303) = the_carrier(_116301))], (515 ^ _109215) ^ [_126303, _126305] : [-(subset(_126305, _126305))], (375 ^ _109215) ^ [_121315] : [v2_membered(_121315), 378 ^ _109215 : [(379 ^ _109215) ^ [_121452] : [element(_121452, powerset(_121315)), 382 ^ _109215 : [(385 ^ _109215) ^ [] : [-(v2_membered(_121452))], (383 ^ _109215) ^ [] : [-(v1_membered(_121452))]]]]], (20 ^ _109215) ^ [_109963, _109965] : [-(v1_xcmplx_0(_109963)), _109965 = _109963, v1_xcmplx_0(_109965)], (491 ^ _109215) ^ [_125476] : [-(set_difference(_125476, empty_set) = _125476)], (110 ^ _109215) ^ [_112618, _112620] : [-(v5_membered(_112618)), _112620 = _112618, v5_membered(_112620)], (60 ^ _109215) ^ [_111143, _111145] : [-(v1_rat_1(_111143)), _111145 = _111143, v1_rat_1(_111145)], (651 ^ _109215) ^ [_130516] : [empty(powerset(_130516))], (198 ^ _109215) ^ [_115454, _115456, _115458, _115460] : [-(subset_complement(_115460, _115456) = subset_complement(_115458, _115454)), _115460 = _115458, _115456 = _115454], (275 ^ _109215) ^ [] : [-(v2_membered(269 ^ []))], (365 ^ _109215) ^ [_120978] : [v1_membered(_120978), 368 ^ _109215 : [(369 ^ _109215) ^ [_121110] : [element(_121110, powerset(_120978)), -(v1_membered(_121110))]]], (192 ^ _109215) ^ [_115208, _115210] : [_115210 = _115208, -(powerset(_115210) = powerset(_115208))], (605 ^ _109215) ^ [_129289] : [one_sorted_str(_129289), -(element(cast_as_carrier_subset(_129289), powerset(the_carrier(_129289))))], (234 ^ _109215) ^ [_116771, _116773] : [in(_116773, _116771), in(_116771, _116773)], (252 ^ _109215) ^ [_117273] : [v4_membered(_117273), -(v3_membered(_117273))], (471 ^ _109215) ^ [_124770, _124772] : [v5_membered(_124772), 474 ^ _109215 : [(475 ^ _109215) ^ [] : [-(v1_membered(set_difference(_124772, _124770)))], (479 ^ _109215) ^ [] : [-(v3_membered(set_difference(_124772, _124770)))], (483 ^ _109215) ^ [] : [-(v5_membered(set_difference(_124772, _124770)))], (481 ^ _109215) ^ [] : [-(v4_membered(set_difference(_124772, _124770)))], (477 ^ _109215) ^ [] : [-(v2_membered(set_difference(_124772, _124770)))]]], (459 ^ _109215) ^ [_124323, _124325] : [v4_membered(_124325), 462 ^ _109215 : [(465 ^ _109215) ^ [] : [-(v2_membered(set_difference(_124325, _124323)))], (467 ^ _109215) ^ [] : [-(v3_membered(set_difference(_124325, _124323)))], (469 ^ _109215) ^ [] : [-(v4_membered(set_difference(_124325, _124323)))], (463 ^ _109215) ^ [] : [-(v1_membered(set_difference(_124325, _124323)))]]], (623 ^ _109215) ^ [_129860, _129862, _129864] : [-(element(subset_difference(_129864, _129862, _129860), powerset(_129864))), element(_129862, powerset(_129864)), element(_129860, powerset(_129864))], (653 ^ _109215) ^ [_130653, _130655] : [element(_130655, powerset(_130653)), -(subset(_130655, _130653))], (665 ^ _109215) ^ [_131021] : [one_sorted_str(_131021), -(cast_as_carrier_subset(_131021) = the_carrier(_131021))], (50 ^ _109215) ^ [_110848, _110850] : [-(v1_int_1(_110848)), _110850 = _110848, v1_int_1(_110850)], (531 ^ _109215) ^ [_126931] : [empty(_126931), 534 ^ _109215 : [(535 ^ _109215) ^ [] : [-(v1_membered(_126931))], (539 ^ _109215) ^ [] : [-(v3_membered(_126931))], (543 ^ _109215) ^ [] : [-(v5_membered(_126931))], (541 ^ _109215) ^ [] : [-(v4_membered(_126931))], (537 ^ _109215) ^ [] : [-(v2_membered(_126931))]]], (361 ^ _109215) ^ [] : [-(v4_membered(empty_set))], (90 ^ _109215) ^ [_112028, _112030] : [-(v3_membered(_112028)), _112030 = _112028, v3_membered(_112030)], (671 ^ _109215) ^ [_131211, _131213] : [element(_131211, powerset(_131213)), -(subset_complement(_131213, _131211) = set_difference(_131213, _131211))], (293 ^ _109215) ^ [_118552] : [v2_membered(_118552), 296 ^ _109215 : [(297 ^ _109215) ^ [_118687] : [element(_118687, _118552), 300 ^ _109215 : [(303 ^ _109215) ^ [] : [-(v1_xreal_0(_118687))], (301 ^ _109215) ^ [] : [-(v1_xcmplx_0(_118687))]]]]]], input).
% 49.35/48.13 ncf('1',plain,[-(element(679 ^ [], powerset(the_carrier(676 ^ []))))],start(681 ^ 0)).
% 49.35/48.13 ncf('1.1',plain,[element(679 ^ [], powerset(the_carrier(676 ^ []))), -(subset_difference(the_carrier(676 ^ []), the_carrier(676 ^ []), 679 ^ []) = set_difference(the_carrier(676 ^ []), 679 ^ [])), element(the_carrier(676 ^ []), powerset(the_carrier(676 ^ [])))],extension(589 ^ 1,bind([[_128853, _128855, _128857], [679 ^ [], the_carrier(676 ^ []), the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1',plain,[subset_difference(the_carrier(676 ^ []), the_carrier(676 ^ []), 679 ^ []) = set_difference(the_carrier(676 ^ []), 679 ^ []), -(subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []) = set_difference(the_carrier(676 ^ []), 679 ^ [])), subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), the_carrier(676 ^ []), 679 ^ [])],extension(10 ^ 2,bind([[_109650, _109652, _109654], [set_difference(the_carrier(676 ^ []), 679 ^ []), subset_difference(the_carrier(676 ^ []), the_carrier(676 ^ []), 679 ^ []), subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1.1',plain,[subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []) = set_difference(the_carrier(676 ^ []), 679 ^ []), -(set_difference(the_carrier(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []))],extension(4 ^ 3,bind([[_109446, _109448], [set_difference(the_carrier(676 ^ []), 679 ^ []), subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1.1.1',plain,[set_difference(the_carrier(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []), -(subset_complement(the_carrier(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ [])), subset_complement(the_carrier(676 ^ []), 679 ^ []) = set_difference(the_carrier(676 ^ []), 679 ^ [])],extension(10 ^ 4,bind([[_109650, _109652, _109654], [subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []), set_difference(the_carrier(676 ^ []), 679 ^ []), subset_complement(the_carrier(676 ^ []), 679 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1.1.1.1',plain,[subset_complement(the_carrier(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ [])],extension(683 ^ 5)).
% 49.35/48.13 ncf('1.1.1.1.1.2',plain,[-(subset_complement(the_carrier(676 ^ []), 679 ^ []) = set_difference(the_carrier(676 ^ []), 679 ^ [])), element(679 ^ [], powerset(the_carrier(676 ^ [])))],extension(671 ^ 5,bind([[_131211, _131213], [679 ^ [], the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1.1.1.2.1',plain,[-(element(679 ^ [], powerset(the_carrier(676 ^ []))))],reduction('1')).
% 49.35/48.13 ncf('1.1.1.2',plain,[-(subset_difference(the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), 679 ^ []) = subset_difference(the_carrier(676 ^ []), the_carrier(676 ^ []), 679 ^ [])), the_carrier(676 ^ []) = the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []) = the_carrier(676 ^ []), 679 ^ [] = 679 ^ []],extension(208 ^ 3,bind([[_115841, _115843, _115845, _115847, _115849, _115851], [679 ^ [], 679 ^ [], the_carrier(676 ^ []), cast_as_carrier_subset(676 ^ []), the_carrier(676 ^ []), the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1.2.1',plain,[-(the_carrier(676 ^ []) = the_carrier(676 ^ []))],extension(2 ^ 4,bind([[_109339], [the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.1.2.2',plain,[-(cast_as_carrier_subset(676 ^ []) = the_carrier(676 ^ [])), one_sorted_str(676 ^ [])],extension(665 ^ 4,bind([[_131021], [676 ^ []]]))).
% 49.35/48.13 ncf('1.1.1.2.2.1',plain,[-(one_sorted_str(676 ^ []))],extension(678 ^ 5)).
% 49.35/48.13 ncf('1.1.1.2.3',plain,[-(679 ^ [] = 679 ^ [])],extension(2 ^ 4,bind([[_109339], [679 ^ []]]))).
% 49.35/48.13 ncf('1.1.2',plain,[-(element(the_carrier(676 ^ []), powerset(the_carrier(676 ^ [])))), in(the_carrier(676 ^ []), powerset(the_carrier(676 ^ []))), element(powerset(the_carrier(676 ^ [])), powerset(powerset(the_carrier(676 ^ []))))],extension(495 ^ 2,bind([[_125681, _125683, _125685], [powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ [])), the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.2.1',plain,[-(in(the_carrier(676 ^ []), powerset(the_carrier(676 ^ [])))), element(the_carrier(676 ^ []), powerset(the_carrier(676 ^ []))), -(empty(powerset(the_carrier(676 ^ []))))],extension(545 ^ 3,bind([[_127412, _127414], [powerset(the_carrier(676 ^ [])), the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.2.1.1',plain,[-(element(the_carrier(676 ^ []), powerset(the_carrier(676 ^ [])))), subset(the_carrier(676 ^ []), the_carrier(676 ^ []))],extension(659 ^ 4,bind([[_130819, _130821], [the_carrier(676 ^ []), the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.2.1.1.1',plain,[-(subset(the_carrier(676 ^ []), the_carrier(676 ^ [])))],extension(515 ^ 5,bind([[_126303, _126305], [_82227, the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.2.1.2',plain,[empty(powerset(the_carrier(676 ^ [])))],extension(651 ^ 4,bind([[_130516], [the_carrier(676 ^ [])]]))).
% 49.35/48.13 ncf('1.1.2.2',plain,[-(element(powerset(the_carrier(676 ^ [])), powerset(powerset(the_carrier(676 ^ []))))), subset(powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ [])))],extension(659 ^ 3,bind([[_130819, _130821], [powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ []))]]))).
% 49.35/48.13 ncf('1.1.2.2.1',plain,[-(subset(powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ [])))), subset(powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ []))), powerset(the_carrier(676 ^ [])) = powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ [])) = powerset(the_carrier(676 ^ []))],extension(144 ^ 4,bind([[_113680, _113682, _113684, _113686], [powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ []))]]))).
% 49.35/48.13 ncf('1.1.2.2.1.1',plain,[-(subset(powerset(the_carrier(676 ^ [])), powerset(the_carrier(676 ^ []))))],extension(515 ^ 5,bind([[_126303, _126305], [_83591, powerset(the_carrier(676 ^ []))]]))).
% 49.35/48.13 ncf('1.1.2.2.1.2',plain,[-(powerset(the_carrier(676 ^ [])) = powerset(the_carrier(676 ^ [])))],extension(2 ^ 5,bind([[_109339], [powerset(the_carrier(676 ^ []))]]))).
% 49.35/48.13 ncf('1.1.2.2.1.3',plain,[-(powerset(the_carrier(676 ^ [])) = powerset(the_carrier(676 ^ [])))],lemmata('[2, 2, 1, 1].x')).
% 49.35/48.13 %-----------------------------------------------------
% 49.35/48.13 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------