%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU307+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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 102.25s 99.62s
% Output : Proof 102.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU307+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n024.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 12:59:07 EDT 2023
% 0.12/0.34 % CPUTime :
% 102.25/99.62
% 102.25/99.62 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 102.25/99.62 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 102.25/99.62 %-----------------------------------------------------
% 102.25/99.62 ncf(matrix, plain, [(728 ^ _108076) ^ [] : [-(one_sorted_str(726 ^ []))], (731 ^ _108076) ^ [] : [-(element(729 ^ [], powerset(the_carrier(726 ^ []))))], (733 ^ _108076) ^ [] : [subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = 729 ^ []], (182 ^ _108076) ^ [_113758, _113760, _113762, _113764] : [-(set_intersection2(_113764, _113760) = set_intersection2(_113762, _113758)), _113764 = _113762, _113760 = _113758], (192 ^ _108076) ^ [_114089, _114091] : [_114091 = _114089, -(powerset(_114091) = powerset(_114089))], (198 ^ _108076) ^ [_114363, _114365, _114367, _114369, _114371, _114373] : [-(subset_intersection2(_114373, _114369, _114365) = subset_intersection2(_114371, _114367, _114363)), _114373 = _114371, _114369 = _114367, _114365 = _114363], (212 ^ _108076) ^ [_114823, _114825] : [_114825 = _114823, -(the_carrier(_114825) = the_carrier(_114823))], (218 ^ _108076) ^ [_115021, _115023] : [_115023 = _115021, -(cast_as_carrier_subset(_115023) = cast_as_carrier_subset(_115021))], (2 ^ _108076) ^ [_108220] : [-(_108220 = _108220)], (4 ^ _108076) ^ [_108327, _108329] : [_108329 = _108327, -(_108327 = _108329)], (10 ^ _108076) ^ [_108531, _108533, _108535] : [-(_108535 = _108531), _108535 = _108533, _108533 = _108531], (20 ^ _108076) ^ [_108844, _108846] : [-(v1_xcmplx_0(_108844)), _108846 = _108844, v1_xcmplx_0(_108846)], (30 ^ _108076) ^ [_109139, _109141] : [-(natural(_109139)), _109141 = _109139, natural(_109141)], (40 ^ _108076) ^ [_109434, _109436] : [-(v1_xreal_0(_109434)), _109436 = _109434, v1_xreal_0(_109436)], (50 ^ _108076) ^ [_109729, _109731] : [-(v1_int_1(_109729)), _109731 = _109729, v1_int_1(_109731)], (60 ^ _108076) ^ [_110024, _110026] : [-(v1_rat_1(_110024)), _110026 = _110024, v1_rat_1(_110026)], (70 ^ _108076) ^ [_110319, _110321] : [-(v1_membered(_110319)), _110321 = _110319, v1_membered(_110321)], (80 ^ _108076) ^ [_110614, _110616] : [-(v2_membered(_110614)), _110616 = _110614, v2_membered(_110616)], (90 ^ _108076) ^ [_110909, _110911] : [-(v3_membered(_110909)), _110911 = _110909, v3_membered(_110911)], (100 ^ _108076) ^ [_111204, _111206] : [-(v4_membered(_111204)), _111206 = _111204, v4_membered(_111206)], (110 ^ _108076) ^ [_111499, _111501] : [-(v5_membered(_111499)), _111501 = _111499, v5_membered(_111501)], (120 ^ _108076) ^ [_111822, _111824, _111826, _111828] : [-(in(_111826, _111822)), in(_111828, _111824), _111828 = _111826, _111824 = _111822], (134 ^ _108076) ^ [_112238, _112240] : [-(empty(_112238)), _112240 = _112238, empty(_112240)], (144 ^ _108076) ^ [_112561, _112563, _112565, _112567] : [-(subset(_112565, _112561)), subset(_112567, _112563), _112567 = _112565, _112563 = _112561], (158 ^ _108076) ^ [_112977, _112979] : [-(one_sorted_str(_112977)), _112979 = _112977, one_sorted_str(_112979)], (168 ^ _108076) ^ [_113280, _113282, _113284, _113286] : [-(element(_113284, _113280)), element(_113286, _113282), _113286 = _113284, _113282 = _113280], (224 ^ _108076) ^ [_115289, _115291] : [in(_115291, _115289), in(_115289, _115291)], (230 ^ _108076) ^ [] : [true___, -(true___)], (236 ^ _108076) ^ [_115605] : [v5_membered(_115605), -(v4_membered(_115605))], (242 ^ _108076) ^ [_115791] : [v4_membered(_115791), -(v3_membered(_115791))], (248 ^ _108076) ^ [_115977] : [v3_membered(_115977), -(v2_membered(_115977))], (254 ^ _108076) ^ [_116163] : [v2_membered(_116163), -(v1_membered(_116163))], (261 ^ _108076) ^ [] : [empty(259 ^ [])], (263 ^ _108076) ^ [] : [-(v1_membered(259 ^ []))], (265 ^ _108076) ^ [] : [-(v2_membered(259 ^ []))], (267 ^ _108076) ^ [] : [-(v3_membered(259 ^ []))], (269 ^ _108076) ^ [] : [-(v4_membered(259 ^ []))], (271 ^ _108076) ^ [] : [-(v5_membered(259 ^ []))], (273 ^ _108076) ^ [_116739] : [v1_membered(_116739), 276 ^ _108076 : [(277 ^ _108076) ^ [_116869] : [element(_116869, _116739), -(v1_xcmplx_0(_116869))]]], (283 ^ _108076) ^ [_117070] : [v2_membered(_117070), 286 ^ _108076 : [(287 ^ _108076) ^ [_117205] : [element(_117205, _117070), 290 ^ _108076 : [(291 ^ _108076) ^ [] : [-(v1_xcmplx_0(_117205))], (293 ^ _108076) ^ [] : [-(v1_xreal_0(_117205))]]]]], (295 ^ _108076) ^ [_117479] : [v3_membered(_117479), 298 ^ _108076 : [(299 ^ _108076) ^ [_117619] : [element(_117619, _117479), 302 ^ _108076 : [(303 ^ _108076) ^ [] : [-(v1_xcmplx_0(_117619))], (305 ^ _108076) ^ [] : [-(v1_xreal_0(_117619))], (307 ^ _108076) ^ [] : [-(v1_rat_1(_117619))]]]]], (309 ^ _108076) ^ [_117965] : [v4_membered(_117965), 312 ^ _108076 : [(313 ^ _108076) ^ [_118110] : [element(_118110, _117965), 316 ^ _108076 : [(317 ^ _108076) ^ [] : [-(v1_xcmplx_0(_118110))], (319 ^ _108076) ^ [] : [-(v1_xreal_0(_118110))], (321 ^ _108076) ^ [] : [-(v1_int_1(_118110))], (323 ^ _108076) ^ [] : [-(v1_rat_1(_118110))]]]]], (325 ^ _108076) ^ [_118528] : [v5_membered(_118528), 328 ^ _108076 : [(329 ^ _108076) ^ [_118678] : [element(_118678, _118528), 332 ^ _108076 : [(333 ^ _108076) ^ [] : [-(v1_xcmplx_0(_118678))], (335 ^ _108076) ^ [] : [-(natural(_118678))], (337 ^ _108076) ^ [] : [-(v1_xreal_0(_118678))], (339 ^ _108076) ^ [] : [-(v1_int_1(_118678))], (341 ^ _108076) ^ [] : [-(v1_rat_1(_118678))]]]]], (343 ^ _108076) ^ [] : [-(empty(empty_set))], (345 ^ _108076) ^ [] : [-(v1_membered(empty_set))], (347 ^ _108076) ^ [] : [-(v2_membered(empty_set))], (349 ^ _108076) ^ [] : [-(v3_membered(empty_set))], (351 ^ _108076) ^ [] : [-(v4_membered(empty_set))], (353 ^ _108076) ^ [] : [-(v5_membered(empty_set))], (355 ^ _108076) ^ [_119496] : [v1_membered(_119496), 358 ^ _108076 : [(359 ^ _108076) ^ [_119628] : [element(_119628, powerset(_119496)), -(v1_membered(_119628))]]], (365 ^ _108076) ^ [_119833] : [v2_membered(_119833), 368 ^ _108076 : [(369 ^ _108076) ^ [_119970] : [element(_119970, powerset(_119833)), 372 ^ _108076 : [(373 ^ _108076) ^ [] : [-(v1_membered(_119970))], (375 ^ _108076) ^ [] : [-(v2_membered(_119970))]]]]], (377 ^ _108076) ^ [_120248] : [v3_membered(_120248), 380 ^ _108076 : [(381 ^ _108076) ^ [_120390] : [element(_120390, powerset(_120248)), 384 ^ _108076 : [(385 ^ _108076) ^ [] : [-(v1_membered(_120390))], (387 ^ _108076) ^ [] : [-(v2_membered(_120390))], (389 ^ _108076) ^ [] : [-(v3_membered(_120390))]]]]], (391 ^ _108076) ^ [_120740] : [v4_membered(_120740), 394 ^ _108076 : [(395 ^ _108076) ^ [_120887] : [element(_120887, powerset(_120740)), 398 ^ _108076 : [(399 ^ _108076) ^ [] : [-(v1_membered(_120887))], (401 ^ _108076) ^ [] : [-(v2_membered(_120887))], (403 ^ _108076) ^ [] : [-(v3_membered(_120887))], (405 ^ _108076) ^ [] : [-(v4_membered(_120887))]]]]], (407 ^ _108076) ^ [_121309] : [v5_membered(_121309), 410 ^ _108076 : [(411 ^ _108076) ^ [_121461] : [element(_121461, powerset(_121309)), 414 ^ _108076 : [(415 ^ _108076) ^ [] : [-(v1_membered(_121461))], (417 ^ _108076) ^ [] : [-(v2_membered(_121461))], (419 ^ _108076) ^ [] : [-(v3_membered(_121461))], (421 ^ _108076) ^ [] : [-(v4_membered(_121461))], (423 ^ _108076) ^ [] : [-(v5_membered(_121461))]]]]], (425 ^ _108076) ^ [_121969, _121971] : [v1_membered(_121971), -(v1_membered(set_intersection2(_121971, _121969)))], (431 ^ _108076) ^ [_122181, _122183] : [v1_membered(_122183), -(v1_membered(set_intersection2(_122181, _122183)))], (437 ^ _108076) ^ [_122393, _122395] : [v2_membered(_122395), 440 ^ _108076 : [(441 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_122395, _122393)))], (443 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_122395, _122393)))]]], (445 ^ _108076) ^ [_122684, _122686] : [v2_membered(_122686), 448 ^ _108076 : [(449 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_122684, _122686)))], (451 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_122684, _122686)))]]], (453 ^ _108076) ^ [_122975, _122977] : [v3_membered(_122977), 456 ^ _108076 : [(457 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_122977, _122975)))], (459 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_122977, _122975)))], (461 ^ _108076) ^ [] : [-(v3_membered(set_intersection2(_122977, _122975)))]]], (463 ^ _108076) ^ [_123344, _123346] : [v3_membered(_123346), 466 ^ _108076 : [(467 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_123344, _123346)))], (469 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_123344, _123346)))], (471 ^ _108076) ^ [] : [-(v3_membered(set_intersection2(_123344, _123346)))]]], (473 ^ _108076) ^ [_123713, _123715] : [v4_membered(_123715), 476 ^ _108076 : [(477 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_123715, _123713)))], (479 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_123715, _123713)))], (481 ^ _108076) ^ [] : [-(v3_membered(set_intersection2(_123715, _123713)))], (483 ^ _108076) ^ [] : [-(v4_membered(set_intersection2(_123715, _123713)))]]], (485 ^ _108076) ^ [_124160, _124162] : [v4_membered(_124162), 488 ^ _108076 : [(489 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_124160, _124162)))], (491 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_124160, _124162)))], (493 ^ _108076) ^ [] : [-(v3_membered(set_intersection2(_124160, _124162)))], (495 ^ _108076) ^ [] : [-(v4_membered(set_intersection2(_124160, _124162)))]]], (497 ^ _108076) ^ [_124607, _124609] : [v5_membered(_124609), 500 ^ _108076 : [(501 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_124609, _124607)))], (503 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_124609, _124607)))], (505 ^ _108076) ^ [] : [-(v3_membered(set_intersection2(_124609, _124607)))], (507 ^ _108076) ^ [] : [-(v4_membered(set_intersection2(_124609, _124607)))], (509 ^ _108076) ^ [] : [-(v5_membered(set_intersection2(_124609, _124607)))]]], (511 ^ _108076) ^ [_125132, _125134] : [v5_membered(_125134), 514 ^ _108076 : [(515 ^ _108076) ^ [] : [-(v1_membered(set_intersection2(_125132, _125134)))], (517 ^ _108076) ^ [] : [-(v2_membered(set_intersection2(_125132, _125134)))], (519 ^ _108076) ^ [] : [-(v3_membered(set_intersection2(_125132, _125134)))], (521 ^ _108076) ^ [] : [-(v4_membered(set_intersection2(_125132, _125134)))], (523 ^ _108076) ^ [] : [-(v5_membered(set_intersection2(_125132, _125134)))]]], (525 ^ _108076) ^ [_125657, _125659] : [in(_125659, _125657), -(element(_125659, _125657))], (531 ^ _108076) ^ [_125838] : [-(set_intersection2(_125838, empty_set) = empty_set)], (533 ^ _108076) ^ [_125962, _125964, _125966] : [-(element(_125966, _125962)), in(_125966, _125964), element(_125964, powerset(_125962))], (543 ^ _108076) ^ [_126289, _126291, _126293] : [in(_126293, _126291), element(_126291, powerset(_126289)), empty(_126289)], (553 ^ _108076) ^ [_126585] : [-(empty(_126585)), 557 ^ _108076 : [(558 ^ _108076) ^ [] : [-(element(556 ^ [_126585], powerset(_126585)))], (560 ^ _108076) ^ [] : [empty(556 ^ [_126585])]]], (563 ^ _108076) ^ [_126968] : [-(element(561 ^ [_126968], powerset(_126968)))], (565 ^ _108076) ^ [_127019] : [-(empty(561 ^ [_127019]))], (567 ^ _108076) ^ [_127118] : [empty(_127118), 570 ^ _108076 : [(571 ^ _108076) ^ [] : [-(v1_membered(_127118))], (573 ^ _108076) ^ [] : [-(v2_membered(_127118))], (575 ^ _108076) ^ [] : [-(v3_membered(_127118))], (577 ^ _108076) ^ [] : [-(v4_membered(_127118))], (579 ^ _108076) ^ [] : [-(v5_membered(_127118))]]], (581 ^ _108076) ^ [_127599, _127601] : [element(_127601, _127599), -(empty(_127599)), -(in(_127601, _127599))], (591 ^ _108076) ^ [_127883] : [empty(_127883), -(_127883 = empty_set)], (597 ^ _108076) ^ [_128085, _128087] : [in(_128087, _128085), empty(_128085)], (603 ^ _108076) ^ [_128292, _128294] : [empty(_128294), -(_128294 = _128292), empty(_128292)], (613 ^ _108076) ^ [_128574, _128576] : [-(set_intersection2(_128576, _128574) = set_intersection2(_128574, _128576))], (615 ^ _108076) ^ [_128674, _128676] : [-(set_intersection2(_128676, _128676) = _128676)], (617 ^ _108076) ^ [_128800, _128802, _128804] : [-(subset_intersection2(_128804, _128802, _128800) = subset_intersection2(_128804, _128800, _128802)), element(_128802, powerset(_128804)), element(_128800, powerset(_128804))], (627 ^ _108076) ^ [_129147, _129149, _129151] : [-(subset_intersection2(_129151, _129149, _129149) = _129149), element(_129149, powerset(_129151)), element(_129147, powerset(_129151))], (637 ^ _108076) ^ [_129457, _129459] : [-(subset(_129459, _129459))], (640 ^ _108076) ^ [] : [-(one_sorted_str(638 ^ []))], (643 ^ _108076) ^ [_129665] : [-(element(641 ^ [_129665], _129665))], (645 ^ _108076) ^ [_129791, _129793, _129795] : [-(subset_intersection2(_129795, _129793, _129791) = set_intersection2(_129793, _129791)), element(_129793, powerset(_129795)), element(_129791, powerset(_129795))], (655 ^ _108076) ^ [] : [true___, -(true___)], (661 ^ _108076) ^ [_130227] : [one_sorted_str(_130227), -(element(cast_as_carrier_subset(_130227), powerset(the_carrier(_130227))))], (667 ^ _108076) ^ [] : [true___, -(true___)], (673 ^ _108076) ^ [_130574, _130576, _130578] : [-(element(subset_intersection2(_130578, _130576, _130574), powerset(_130578))), element(_130576, powerset(_130578)), element(_130574, powerset(_130578))], (683 ^ _108076) ^ [] : [true___, -(true___)], (689 ^ _108076) ^ [] : [true___, -(true___)], (695 ^ _108076) ^ [] : [true___, -(true___)], (701 ^ _108076) ^ [_131230] : [empty(powerset(_131230))], (703 ^ _108076) ^ [_131367, _131369] : [element(_131369, powerset(_131367)), -(subset(_131369, _131367))], (709 ^ _108076) ^ [_131533, _131535] : [subset(_131535, _131533), -(element(_131535, powerset(_131533)))], (715 ^ _108076) ^ [_131735] : [one_sorted_str(_131735), -(cast_as_carrier_subset(_131735) = the_carrier(_131735))], (721 ^ _108076) ^ [_131925, _131927] : [subset(_131927, _131925), -(set_intersection2(_131927, _131925) = _131927)]], input).
% 102.25/99.62 ncf('1',plain,[subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = 729 ^ []],start(733 ^ 0)).
% 102.25/99.62 ncf('1.1',plain,[-(subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = 729 ^ []), subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])), set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])) = 729 ^ []],extension(10 ^ 1,bind([[_108531, _108533, _108535], [729 ^ [], set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])), subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ []))]]))).
% 102.25/99.62 ncf('1.1.1',plain,[-(subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ []))), subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])), set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ []))],extension(10 ^ 2,bind([[_108531, _108533, _108535], [set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])), set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])), subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ []))]]))).
% 102.25/99.62 ncf('1.1.1.1',plain,[-(subset_intersection2(the_carrier(726 ^ []), 729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ []))), element(729 ^ [], powerset(the_carrier(726 ^ []))), element(cast_as_carrier_subset(726 ^ []), powerset(the_carrier(726 ^ [])))],extension(645 ^ 3,bind([[_129791, _129793, _129795], [cast_as_carrier_subset(726 ^ []), 729 ^ [], the_carrier(726 ^ [])]]))).
% 102.25/99.62 ncf('1.1.1.1.1',plain,[-(element(729 ^ [], powerset(the_carrier(726 ^ []))))],extension(731 ^ 4)).
% 102.25/99.62 ncf('1.1.1.1.2',plain,[-(element(cast_as_carrier_subset(726 ^ []), powerset(the_carrier(726 ^ [])))), one_sorted_str(726 ^ [])],extension(661 ^ 4,bind([[_130227], [726 ^ []]]))).
% 102.25/99.62 ncf('1.1.1.1.2.1',plain,[-(one_sorted_str(726 ^ []))],extension(728 ^ 5)).
% 102.25/99.62 ncf('1.1.1.2',plain,[-(set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ []))), 729 ^ [] = 729 ^ [], cast_as_carrier_subset(726 ^ []) = cast_as_carrier_subset(726 ^ [])],extension(182 ^ 3,bind([[_113758, _113760, _113762, _113764], [cast_as_carrier_subset(726 ^ []), cast_as_carrier_subset(726 ^ []), 729 ^ [], 729 ^ []]]))).
% 102.25/99.62 ncf('1.1.1.2.1',plain,[-(729 ^ [] = 729 ^ [])],extension(2 ^ 4,bind([[_108220], [729 ^ []]]))).
% 102.25/99.62 ncf('1.1.1.2.2',plain,[-(cast_as_carrier_subset(726 ^ []) = cast_as_carrier_subset(726 ^ []))],extension(2 ^ 4,bind([[_108220], [cast_as_carrier_subset(726 ^ [])]]))).
% 102.25/99.62 ncf('1.1.2',plain,[-(set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])) = 729 ^ []), set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], the_carrier(726 ^ [])), set_intersection2(729 ^ [], the_carrier(726 ^ [])) = 729 ^ []],extension(10 ^ 2,bind([[_108531, _108533, _108535], [729 ^ [], set_intersection2(729 ^ [], the_carrier(726 ^ [])), set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ []))]]))).
% 102.25/99.62 ncf('1.1.2.1',plain,[-(set_intersection2(729 ^ [], cast_as_carrier_subset(726 ^ [])) = set_intersection2(729 ^ [], the_carrier(726 ^ []))), 729 ^ [] = 729 ^ [], cast_as_carrier_subset(726 ^ []) = the_carrier(726 ^ [])],extension(182 ^ 3,bind([[_113758, _113760, _113762, _113764], [the_carrier(726 ^ []), cast_as_carrier_subset(726 ^ []), 729 ^ [], 729 ^ []]]))).
% 102.25/99.62 ncf('1.1.2.1.1',plain,[-(729 ^ [] = 729 ^ [])],extension(2 ^ 4,bind([[_108220], [729 ^ []]]))).
% 102.25/99.62 ncf('1.1.2.1.2',plain,[-(cast_as_carrier_subset(726 ^ []) = the_carrier(726 ^ [])), one_sorted_str(726 ^ [])],extension(715 ^ 4,bind([[_131735], [726 ^ []]]))).
% 102.25/99.62 ncf('1.1.2.1.2.1',plain,[-(one_sorted_str(726 ^ []))],extension(728 ^ 5)).
% 102.25/99.62 ncf('1.1.2.2',plain,[-(set_intersection2(729 ^ [], the_carrier(726 ^ [])) = 729 ^ []), subset(729 ^ [], the_carrier(726 ^ []))],extension(721 ^ 3,bind([[_131925, _131927], [the_carrier(726 ^ []), 729 ^ []]]))).
% 102.25/99.62 ncf('1.1.2.2.1',plain,[-(subset(729 ^ [], the_carrier(726 ^ []))), element(729 ^ [], powerset(the_carrier(726 ^ [])))],extension(703 ^ 4,bind([[_131367, _131369], [the_carrier(726 ^ []), 729 ^ []]]))).
% 102.25/99.62 ncf('1.1.2.2.1.1',plain,[-(element(729 ^ [], powerset(the_carrier(726 ^ []))))],extension(731 ^ 5)).
% 102.25/99.62 %-----------------------------------------------------
% 102.25/99.62 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------