%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU327+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:03:09 EDT 2023
% Result : Theorem 283.65s 274.36s
% Output : Proof 283.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU327+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 13:12:03 EDT 2023
% 0.13/0.33 % CPUTime :
% 283.65/274.36
% 283.65/274.36 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 283.65/274.36 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 283.65/274.36 %-----------------------------------------------------
% 283.65/274.36 ncf(matrix, plain, [(490 ^ _117479) ^ [_133586, _133588] : [element(_133586, powerset(powerset(_133588))), -(element(union_of_subsets(_133588, _133586), powerset(_133588)))], (529 ^ _117479) ^ [_134936, _134938] : [v1_membered(_134938), -(v1_membered(set_difference(_134938, _134936)))], (744 ^ _117479) ^ [] : [meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))], (4 ^ _117479) ^ [_117730, _117732] : [_117732 = _117730, -(_117730 = _117732)], (110 ^ _117479) ^ [_120902, _120904] : [-(v5_membered(_120902)), _120904 = _120902, v5_membered(_120904)], (535 ^ _117479) ^ [_135148, _135150] : [v2_membered(_135150), 538 ^ _117479 : [(541 ^ _117479) ^ [] : [-(v2_membered(set_difference(_135150, _135148)))], (539 ^ _117479) ^ [] : [-(v1_membered(set_difference(_135150, _135148)))]]], (591 ^ _117479) ^ [_137108, _137110] : [element(_137108, powerset(_137110)), -(subset_complement(_137110, subset_complement(_137110, _137108)) = _137108)], (214 ^ _117479) ^ [_124365, _124367] : [_124367 = _124365, -(powerset(_124367) = powerset(_124365))], (386 ^ _117479) ^ [_130406] : [v4_membered(_130406), 389 ^ _117479 : [(390 ^ _117479) ^ [_130553] : [element(_130553, powerset(_130406)), 393 ^ _117479 : [(396 ^ _117479) ^ [] : [-(v2_membered(_130553))], (398 ^ _117479) ^ [] : [-(v3_membered(_130553))], (400 ^ _117479) ^ [] : [-(v4_membered(_130553))], (394 ^ _117479) ^ [] : [-(v1_membered(_130553))]]]]], (172 ^ _117479) ^ [_122836, _122838] : [_122838 = _122836, -(union(_122838) = union(_122836))], (402 ^ _117479) ^ [_130975] : [v5_membered(_130975), -(v4_membered(_130975))], (512 ^ _117479) ^ [_134385, _134387] : [element(_134385, powerset(powerset(_134387))), -(element(complements_of_subsets(_134387, _134385), powerset(powerset(_134387))))], (204 ^ _117479) ^ [_124034, _124036, _124038, _124040] : [-(set_difference(_124040, _124036) = set_difference(_124038, _124034)), _124040 = _124038, _124036 = _124034], (230 ^ _117479) ^ [_124970, _124972, _124974, _124976] : [-(complements_of_subsets(_124976, _124972) = complements_of_subsets(_124974, _124970)), _124976 = _124974, _124972 = _124970], (70 ^ _117479) ^ [_119722, _119724] : [-(v1_membered(_119722)), _119724 = _119722, v1_membered(_119724)], (426 ^ _117479) ^ [_131807] : [v4_membered(_131807), -(v3_membered(_131807))], (502 ^ _117479) ^ [_134056, _134058, _134060] : [-(element(subset_difference(_134060, _134058, _134056), powerset(_134060))), element(_134058, powerset(_134060)), element(_134056, powerset(_134060))], (597 ^ _117479) ^ [_137334, _137336] : [element(_137334, powerset(powerset(_137336))), -(complements_of_subsets(_137336, complements_of_subsets(_137336, _137334)) = _137334)], (740 ^ _117479) ^ [] : [-(element(738 ^ [], powerset(powerset(737 ^ []))))], (318 ^ _117479) ^ [_128055] : [v5_membered(_128055), 321 ^ _117479 : [(322 ^ _117479) ^ [_128205] : [element(_128205, _128055), 325 ^ _117479 : [(332 ^ _117479) ^ [] : [-(v1_int_1(_128205))], (326 ^ _117479) ^ [] : [-(v1_xcmplx_0(_128205))], (330 ^ _117479) ^ [] : [-(v1_xreal_0(_128205))], (334 ^ _117479) ^ [] : [-(v1_rat_1(_128205))], (328 ^ _117479) ^ [] : [-(natural(_128205))]]]]], (478 ^ _117479) ^ [] : [true___, -(true___)], (672 ^ _117479) ^ [_140000, _140002] : [element(_140002, powerset(_140000)), -(subset(_140002, _140000))], (589 ^ _117479) ^ [] : [-(v5_membered(empty_set))], (696 ^ _117479) ^ [_140817, _140819, _140821] : [-(element(_140821, _140817)), in(_140821, _140819), element(_140819, powerset(_140817))], (606 ^ _117479) ^ [] : [-(v1_membered(602 ^ []))], (608 ^ _117479) ^ [] : [-(v2_membered(602 ^ []))], (684 ^ _117479) ^ [_140382, _140384] : [element(_140382, powerset(powerset(_140384))), -(_140382 = empty_set), -(subset_difference(_140384, cast_to_subset(_140384), union_of_subsets(_140384, _140382)) = meet_of_subsets(_140384, complements_of_subsets(_140384, _140382)))], (742 ^ _117479) ^ [] : [738 ^ [] = empty_set], (148 ^ _117479) ^ [_122085, _122087] : [-(empty(_122085)), _122087 = _122085, empty(_122087)], (458 ^ _117479) ^ [] : [true___, -(true___)], (10 ^ _117479) ^ [_117934, _117936, _117938] : [-(_117938 = _117934), _117938 = _117936, _117936 = _117934], (660 ^ _117479) ^ [_139592, _139594] : [element(_139594, _139592), -(empty(_139592)), -(in(_139594, _139592))], (722 ^ _117479) ^ [_141642, _141644] : [in(_141644, _141642), empty(_141642)], (614 ^ _117479) ^ [] : [-(v5_membered(602 ^ []))], (579 ^ _117479) ^ [] : [-(empty(empty_set))], (432 ^ _117479) ^ [_131993] : [v3_membered(_131993), -(v2_membered(_131993))], (616 ^ _117479) ^ [_137940] : [-(empty(_137940)), 620 ^ _117479 : [(623 ^ _117479) ^ [] : [empty(619 ^ [_137940])], (621 ^ _117479) ^ [] : [-(element(619 ^ [_137940], powerset(_137940)))]]], (652 ^ _117479) ^ [_139273, _139275] : [-(subset(_139275, _139275))], (630 ^ _117479) ^ [_138487, _138489] : [element(_138487, powerset(powerset(_138489))), -(union_of_subsets(_138489, _138487) = union(_138487))], (583 ^ _117479) ^ [] : [-(v2_membered(empty_set))], (678 ^ _117479) ^ [_140166, _140168] : [subset(_140168, _140166), -(element(_140168, powerset(_140166)))], (587 ^ _117479) ^ [] : [-(v4_membered(empty_set))], (360 ^ _117479) ^ [_129499] : [v2_membered(_129499), 363 ^ _117479 : [(364 ^ _117479) ^ [_129636] : [element(_129636, powerset(_129499)), 367 ^ _117479 : [(370 ^ _117479) ^ [] : [-(v2_membered(_129636))], (368 ^ _117479) ^ [] : [-(v1_membered(_129636))]]]]], (408 ^ _117479) ^ [_131161] : [v5_membered(_131161), 411 ^ _117479 : [(412 ^ _117479) ^ [_131313] : [element(_131313, powerset(_131161)), 415 ^ _117479 : [(422 ^ _117479) ^ [] : [-(v4_membered(_131313))], (416 ^ _117479) ^ [] : [-(v1_membered(_131313))], (420 ^ _117479) ^ [] : [-(v3_membered(_131313))], (424 ^ _117479) ^ [] : [-(v5_membered(_131313))], (418 ^ _117479) ^ [] : [-(v2_membered(_131313))]]]]], (120 ^ _117479) ^ [_121225, _121227, _121229, _121231] : [-(subset(_121229, _121225)), subset(_121231, _121227), _121231 = _121229, _121227 = _121225], (612 ^ _117479) ^ [] : [-(v4_membered(602 ^ []))], (50 ^ _117479) ^ [_119132, _119134] : [-(v1_int_1(_119132)), _119134 = _119132, v1_int_1(_119134)], (518 ^ _117479) ^ [] : [true___, -(true___)], (716 ^ _117479) ^ [_141440] : [empty(_141440), -(_141440 = empty_set)], (288 ^ _117479) ^ [_127006] : [v3_membered(_127006), 291 ^ _117479 : [(292 ^ _117479) ^ [_127146] : [element(_127146, _127006), 295 ^ _117479 : [(296 ^ _117479) ^ [] : [-(v1_xcmplx_0(_127146))], (300 ^ _117479) ^ [] : [-(v1_rat_1(_127146))], (298 ^ _117479) ^ [] : [-(v1_xreal_0(_127146))]]]]], (90 ^ _117479) ^ [_120312, _120314] : [-(v3_membered(_120312)), _120314 = _120312, v3_membered(_120314)], (452 ^ _117479) ^ [] : [true___, -(true___)], (527 ^ _117479) ^ [_134828] : [empty(powerset(_134828))], (604 ^ _117479) ^ [] : [empty(602 ^ [])], (198 ^ _117479) ^ [_123788, _123790] : [_123790 = _123788, -(cast_to_subset(_123790) = cast_to_subset(_123788))], (80 ^ _117479) ^ [_120017, _120019] : [-(v2_membered(_120017)), _120019 = _120017, v2_membered(_120019)], (628 ^ _117479) ^ [_138374] : [-(empty(624 ^ [_138374]))], (350 ^ _117479) ^ [_129162] : [v1_membered(_129162), 353 ^ _117479 : [(354 ^ _117479) ^ [_129294] : [element(_129294, powerset(_129162)), -(v1_membered(_129294))]]], (372 ^ _117479) ^ [_129914] : [v3_membered(_129914), 375 ^ _117479 : [(376 ^ _117479) ^ [_130056] : [element(_130056, powerset(_129914)), 379 ^ _117479 : [(380 ^ _117479) ^ [] : [-(v1_membered(_130056))], (384 ^ _117479) ^ [] : [-(v3_membered(_130056))], (382 ^ _117479) ^ [] : [-(v2_membered(_130056))]]]]], (581 ^ _117479) ^ [] : [-(v1_membered(empty_set))], (728 ^ _117479) ^ [_141829, _141831] : [empty(_141831), -(_141831 = _141829), empty(_141829)], (240 ^ _117479) ^ [_125329, _125331, _125333, _125335] : [-(subset_complement(_125335, _125331) = subset_complement(_125333, _125329)), _125335 = _125333, _125331 = _125329], (626 ^ _117479) ^ [_138323] : [-(element(624 ^ [_138323], powerset(_138323)))], (60 ^ _117479) ^ [_119427, _119429] : [-(v1_rat_1(_119427)), _119429 = _119427, v1_rat_1(_119429)], (543 ^ _117479) ^ [_135439, _135441] : [v3_membered(_135441), 546 ^ _117479 : [(547 ^ _117479) ^ [] : [-(v1_membered(set_difference(_135441, _135439)))], (551 ^ _117479) ^ [] : [-(v3_membered(set_difference(_135441, _135439)))], (549 ^ _117479) ^ [] : [-(v2_membered(set_difference(_135441, _135439)))]]], (464 ^ _117479) ^ [] : [true___, -(true___)], (553 ^ _117479) ^ [_135808, _135810] : [v4_membered(_135810), 556 ^ _117479 : [(559 ^ _117479) ^ [] : [-(v2_membered(set_difference(_135810, _135808)))], (561 ^ _117479) ^ [] : [-(v3_membered(set_difference(_135810, _135808)))], (563 ^ _117479) ^ [] : [-(v4_membered(set_difference(_135810, _135808)))], (557 ^ _117479) ^ [] : [-(v1_membered(set_difference(_135810, _135808)))]]], (470 ^ _117479) ^ [_133013] : [-(element(cast_to_subset(_133013), powerset(_133013)))], (30 ^ _117479) ^ [_118542, _118544] : [-(natural(_118542)), _118544 = _118542, natural(_118544)], (20 ^ _117479) ^ [_118247, _118249] : [-(v1_xcmplx_0(_118247)), _118249 = _118247, v1_xcmplx_0(_118249)], (260 ^ _117479) ^ [_126069, _126071] : [in(_126071, _126069), in(_126069, _126071)], (565 ^ _117479) ^ [_136255, _136257] : [v5_membered(_136257), 568 ^ _117479 : [(575 ^ _117479) ^ [] : [-(v4_membered(set_difference(_136257, _136255)))], (569 ^ _117479) ^ [] : [-(v1_membered(set_difference(_136257, _136255)))], (573 ^ _117479) ^ [] : [-(v3_membered(set_difference(_136257, _136255)))], (577 ^ _117479) ^ [] : [-(v5_membered(set_difference(_136257, _136255)))], (571 ^ _117479) ^ [] : [-(v2_membered(set_difference(_136257, _136255)))]]], (444 ^ _117479) ^ [_132350] : [-(cast_to_subset(_132350) = _132350)], (654 ^ _117479) ^ [_139382, _139384] : [in(_139384, _139382), -(element(_139384, _139382))], (642 ^ _117479) ^ [_138957, _138959, _138961] : [-(subset_difference(_138961, _138959, _138957) = set_difference(_138959, _138957)), element(_138959, powerset(_138961)), element(_138957, powerset(_138961))], (438 ^ _117479) ^ [_132179] : [v2_membered(_132179), -(v1_membered(_132179))], (496 ^ _117479) ^ [_133814, _133816] : [element(_133814, powerset(powerset(_133816))), -(element(meet_of_subsets(_133816, _133814), powerset(_133816)))], (134 ^ _117479) ^ [_121669, _121671, _121673, _121675] : [-(in(_121673, _121669)), in(_121675, _121671), _121675 = _121673, _121671 = _121669], (694 ^ _117479) ^ [_140693] : [-(set_difference(empty_set, _140693) = empty_set)], (276 ^ _117479) ^ [_126597] : [v2_membered(_126597), 279 ^ _117479 : [(280 ^ _117479) ^ [_126732] : [element(_126732, _126597), 283 ^ _117479 : [(286 ^ _117479) ^ [] : [-(v1_xreal_0(_126732))], (284 ^ _117479) ^ [] : [-(v1_xcmplx_0(_126732))]]]]], (158 ^ _117479) ^ [_122388, _122390, _122392, _122394] : [-(element(_122392, _122388)), element(_122394, _122390), _122394 = _122392, _122390 = _122388], (472 ^ _117479) ^ [_133124, _133126] : [element(_133124, powerset(_133126)), -(element(subset_complement(_133126, _133124), powerset(_133126)))], (636 ^ _117479) ^ [_138715, _138717] : [element(_138715, powerset(powerset(_138717))), -(meet_of_subsets(_138717, _138715) = set_meet(_138715))], (706 ^ _117479) ^ [_141144, _141146, _141148] : [in(_141148, _141146), element(_141146, powerset(_141144)), empty(_141144)], (446 ^ _117479) ^ [_132459, _132461] : [element(_132459, powerset(_132461)), -(subset_complement(_132461, _132459) = set_difference(_132461, _132459))], (2 ^ _117479) ^ [_117623] : [-(_117623 = _117623)], (100 ^ _117479) ^ [_120607, _120609] : [-(v4_membered(_120607)), _120609 = _120607, v4_membered(_120609)], (302 ^ _117479) ^ [_127492] : [v4_membered(_127492), 305 ^ _117479 : [(306 ^ _117479) ^ [_127637] : [element(_127637, _127492), 309 ^ _117479 : [(312 ^ _117479) ^ [] : [-(v1_xreal_0(_127637))], (314 ^ _117479) ^ [] : [-(v1_int_1(_127637))], (316 ^ _117479) ^ [] : [-(v1_rat_1(_127637))], (310 ^ _117479) ^ [] : [-(v1_xcmplx_0(_127637))]]]]], (670 ^ _117479) ^ [_139861] : [-(set_difference(_139861, empty_set) = _139861)], (178 ^ _117479) ^ [_123054, _123056] : [_123056 = _123054, -(set_meet(_123056) = set_meet(_123054))], (266 ^ _117479) ^ [_126266] : [v1_membered(_126266), 269 ^ _117479 : [(270 ^ _117479) ^ [_126396] : [element(_126396, _126266), -(v1_xcmplx_0(_126396))]]], (610 ^ _117479) ^ [] : [-(v3_membered(602 ^ []))], (220 ^ _117479) ^ [_124611, _124613, _124615, _124617] : [-(meet_of_subsets(_124617, _124613) = meet_of_subsets(_124615, _124611)), _124617 = _124615, _124613 = _124611], (484 ^ _117479) ^ [] : [true___, -(true___)], (525 ^ _117479) ^ [_134746] : [-(element(523 ^ [_134746], _134746))], (184 ^ _117479) ^ [_123328, _123330, _123332, _123334, _123336, _123338] : [-(subset_difference(_123338, _123334, _123330) = subset_difference(_123336, _123332, _123328)), _123338 = _123336, _123334 = _123332, _123330 = _123328], (40 ^ _117479) ^ [_118837, _118839] : [-(v1_xreal_0(_118837)), _118839 = _118837, v1_xreal_0(_118839)], (336 ^ _117479) ^ [_128695] : [empty(_128695), 339 ^ _117479 : [(346 ^ _117479) ^ [] : [-(v4_membered(_128695))], (340 ^ _117479) ^ [] : [-(v1_membered(_128695))], (344 ^ _117479) ^ [] : [-(v3_membered(_128695))], (348 ^ _117479) ^ [] : [-(v5_membered(_128695))], (342 ^ _117479) ^ [] : [-(v2_membered(_128695))]]], (250 ^ _117479) ^ [_125668, _125670, _125672, _125674] : [-(union_of_subsets(_125674, _125670) = union_of_subsets(_125672, _125668)), _125674 = _125672, _125670 = _125668], (585 ^ _117479) ^ [] : [-(v3_membered(empty_set))]], input).
% 283.65/274.36 ncf('1',plain,[meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))],start(744 ^ 0)).
% 283.65/274.36 ncf('1.1',plain,[-(meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))), meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ [])) = subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))],extension(10 ^ 1,bind([[_117934, _117936, _117938], [subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])), meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ []))]]))).
% 283.65/274.36 ncf('1.1.1',plain,[-(meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ [])) = subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ []))), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ []))],extension(4 ^ 2,bind([[_117730, _117732], [meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ [])), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ []))]]))).
% 283.65/274.36 ncf('1.1.1.1',plain,[-(subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = meet_of_subsets(737 ^ [], complements_of_subsets(737 ^ [], 738 ^ []))), element(738 ^ [], powerset(powerset(737 ^ []))), -(738 ^ [] = empty_set)],extension(684 ^ 3,bind([[_140382, _140384], [738 ^ [], 737 ^ []]]))).
% 283.65/274.36 ncf('1.1.1.1.1',plain,[-(element(738 ^ [], powerset(powerset(737 ^ []))))],extension(740 ^ 4)).
% 283.65/274.36 ncf('1.1.1.1.2',plain,[738 ^ [] = empty_set],extension(742 ^ 4)).
% 283.65/274.36 ncf('1.1.2',plain,[-(subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])), set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))],extension(10 ^ 2,bind([[_117934, _117936, _117938], [subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])), set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ []))]]))).
% 283.65/274.36 ncf('1.1.2.1',plain,[-(subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])), set_difference(cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))],extension(10 ^ 3,bind([[_117934, _117936, _117938], [set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])), set_difference(cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])), subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ []))]]))).
% 283.65/274.36 ncf('1.1.2.1.1',plain,[-(subset_difference(737 ^ [], cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ []))), element(cast_to_subset(737 ^ []), powerset(737 ^ [])), element(union_of_subsets(737 ^ [], 738 ^ []), powerset(737 ^ []))],extension(642 ^ 4,bind([[_138957, _138959, _138961], [union_of_subsets(737 ^ [], 738 ^ []), cast_to_subset(737 ^ []), 737 ^ []]]))).
% 283.65/274.36 ncf('1.1.2.1.1.1',plain,[-(element(cast_to_subset(737 ^ []), powerset(737 ^ [])))],extension(470 ^ 5,bind([[_133013], [737 ^ []]]))).
% 283.65/274.36 ncf('1.1.2.1.1.2',plain,[-(element(union_of_subsets(737 ^ [], 738 ^ []), powerset(737 ^ []))), element(738 ^ [], powerset(powerset(737 ^ [])))],extension(490 ^ 5,bind([[_133586, _133588], [738 ^ [], 737 ^ []]]))).
% 283.65/274.36 ncf('1.1.2.1.1.2.1',plain,[-(element(738 ^ [], powerset(powerset(737 ^ []))))],extension(740 ^ 6)).
% 283.65/274.36 ncf('1.1.2.1.2',plain,[-(set_difference(cast_to_subset(737 ^ []), union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))), cast_to_subset(737 ^ []) = 737 ^ [], union_of_subsets(737 ^ [], 738 ^ []) = union_of_subsets(737 ^ [], 738 ^ [])],extension(204 ^ 4,bind([[_124034, _124036, _124038, _124040], [union_of_subsets(737 ^ [], 738 ^ []), union_of_subsets(737 ^ [], 738 ^ []), 737 ^ [], cast_to_subset(737 ^ [])]]))).
% 283.65/274.36 ncf('1.1.2.1.2.1',plain,[-(cast_to_subset(737 ^ []) = 737 ^ [])],extension(444 ^ 5,bind([[_132350], [737 ^ []]]))).
% 283.65/274.36 ncf('1.1.2.1.2.2',plain,[-(union_of_subsets(737 ^ [], 738 ^ []) = union_of_subsets(737 ^ [], 738 ^ []))],extension(2 ^ 5,bind([[_117623], [union_of_subsets(737 ^ [], 738 ^ [])]]))).
% 283.65/274.36 ncf('1.1.2.2',plain,[-(set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])) = subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))), subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))],extension(4 ^ 3,bind([[_117730, _117732], [set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])), subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))]]))).
% 283.65/274.36 ncf('1.1.2.2.1',plain,[-(subset_complement(737 ^ [], union_of_subsets(737 ^ [], 738 ^ [])) = set_difference(737 ^ [], union_of_subsets(737 ^ [], 738 ^ []))), element(union_of_subsets(737 ^ [], 738 ^ []), powerset(737 ^ []))],extension(446 ^ 4,bind([[_132459, _132461], [union_of_subsets(737 ^ [], 738 ^ []), 737 ^ []]]))).
% 283.65/274.36 ncf('1.1.2.2.1.1',plain,[-(element(union_of_subsets(737 ^ [], 738 ^ []), powerset(737 ^ []))), element(738 ^ [], powerset(powerset(737 ^ [])))],extension(490 ^ 5,bind([[_133586, _133588], [738 ^ [], 737 ^ []]]))).
% 283.65/274.36 ncf('1.1.2.2.1.1.1',plain,[-(element(738 ^ [], powerset(powerset(737 ^ []))))],extension(740 ^ 6)).
% 283.65/274.36 %-----------------------------------------------------
% 283.65/274.36 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------