%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU155+2 : 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:25 EDT 2023
% Result : Theorem 0.74s 1.38s
% Output : Proof 0.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU155+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 12:57:57 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.74/1.38
% 0.74/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.74/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.74/1.38 %-----------------------------------------------------
% 0.74/1.38 ncf(matrix, plain, [(906 ^ _120549) ^ [] : [-(in(903 ^ [], 904 ^ []))], (908 ^ _120549) ^ [] : [subset(903 ^ [], union(904 ^ []))], (86 ^ _120549) ^ [_123382, _123384] : [_123384 = _123382, -(powerset(_123384) = powerset(_123382))], (92 ^ _120549) ^ [_123628, _123630, _123632, _123634] : [-(set_intersection2(_123634, _123630) = set_intersection2(_123632, _123628)), _123634 = _123632, _123630 = _123628], (102 ^ _120549) ^ [_123987, _123989, _123991, _123993] : [-(set_difference(_123993, _123989) = set_difference(_123991, _123987)), _123993 = _123991, _123989 = _123987], (112 ^ _120549) ^ [_124346, _124348, _124350, _124352] : [-(set_union2(_124352, _124348) = set_union2(_124350, _124346)), _124352 = _124350, _124348 = _124346], (122 ^ _120549) ^ [_124677, _124679] : [_124679 = _124677, -(singleton(_124679) = singleton(_124677))], (138 ^ _120549) ^ [_125234, _125236] : [_125236 = _125234, -(union(_125236) = union(_125234))], (128 ^ _120549) ^ [_124923, _124925, _124927, _124929] : [-(unordered_pair(_124929, _124925) = unordered_pair(_124927, _124923)), _124929 = _124927, _124925 = _124923], (2 ^ _120549) ^ [_120693] : [-(_120693 = _120693)], (4 ^ _120549) ^ [_120800, _120802] : [_120802 = _120800, -(_120800 = _120802)], (10 ^ _120549) ^ [_121004, _121006, _121008] : [-(_121008 = _121004), _121008 = _121006, _121006 = _121004], (20 ^ _120549) ^ [_121345, _121347, _121349, _121351] : [-(proper_subset(_121349, _121345)), proper_subset(_121351, _121347), _121351 = _121349, _121347 = _121345], (34 ^ _120549) ^ [_121789, _121791, _121793, _121795] : [-(disjoint(_121793, _121789)), disjoint(_121795, _121791), _121795 = _121793, _121791 = _121789], (48 ^ _120549) ^ [_122205, _122207] : [-(empty(_122205)), _122207 = _122205, empty(_122207)], (58 ^ _120549) ^ [_122528, _122530, _122532, _122534] : [-(in(_122532, _122528)), in(_122534, _122530), _122534 = _122532, _122530 = _122528], (72 ^ _120549) ^ [_122952, _122954, _122956, _122958] : [-(subset(_122956, _122952)), subset(_122958, _122954), _122958 = _122956, _122954 = _122952], (144 ^ _120549) ^ [_125478, _125480] : [in(_125480, _125478), in(_125478, _125480)], (150 ^ _120549) ^ [_125689, _125691] : [proper_subset(_125691, _125689), proper_subset(_125689, _125691)], (156 ^ _120549) ^ [_125885, _125887] : [-(unordered_pair(_125887, _125885) = unordered_pair(_125885, _125887))], (158 ^ _120549) ^ [_125985, _125987] : [-(set_union2(_125987, _125985) = set_union2(_125985, _125987))], (160 ^ _120549) ^ [_126085, _126087] : [-(set_intersection2(_126087, _126085) = set_intersection2(_126085, _126087))], (162 ^ _120549) ^ [_126229, _126231] : [_126231 = _126229, 165 ^ _120549 : [(166 ^ _120549) ^ [] : [-(subset(_126231, _126229))], (168 ^ _120549) ^ [] : [-(subset(_126229, _126231))]]], (170 ^ _120549) ^ [_126466, _126468] : [-(_126468 = _126466), subset(_126468, _126466), subset(_126466, _126468)], (196 ^ _120549) ^ [_127317, _127319] : [-(_127317 = singleton(_127319)), 200 ^ _120549 : [(201 ^ _120549) ^ [] : [-(in(197 ^ [_127317, _127319], _127317))], (203 ^ _120549) ^ [] : [197 ^ [_127317, _127319] = _127319]], 204 ^ _120549 : [(205 ^ _120549) ^ [] : [-(197 ^ [_127317, _127319] = _127319)], (207 ^ _120549) ^ [] : [in(197 ^ [_127317, _127319], _127317)]]], (180 ^ _120549) ^ [_126796, _126798] : [_126796 = singleton(_126798), 183 ^ _120549 : [(184 ^ _120549) ^ [_126966] : [in(_126966, _126796), -(_126966 = _126798)], (190 ^ _120549) ^ [_127138] : [_127138 = _126798, -(in(_127138, _126796))]]], (211 ^ _120549) ^ [_127868] : [_127868 = empty_set, 214 ^ _120549 : [(215 ^ _120549) ^ [_127981] : [in(_127981, _127868)]]], (217 ^ _120549) ^ [_128047] : [-(in(218 ^ [_128047], _128047)), -(_128047 = empty_set)], (240 ^ _120549) ^ [_128859, _128861] : [-(_128859 = powerset(_128861)), 244 ^ _120549 : [(245 ^ _120549) ^ [] : [-(in(241 ^ [_128859, _128861], _128859))], (247 ^ _120549) ^ [] : [subset(241 ^ [_128859, _128861], _128861)]], 248 ^ _120549 : [(249 ^ _120549) ^ [] : [-(subset(241 ^ [_128859, _128861], _128861))], (251 ^ _120549) ^ [] : [in(241 ^ [_128859, _128861], _128859)]]], (224 ^ _120549) ^ [_128338, _128340] : [_128338 = powerset(_128340), 227 ^ _120549 : [(228 ^ _120549) ^ [_128508] : [in(_128508, _128338), -(subset(_128508, _128340))], (234 ^ _120549) ^ [_128680] : [subset(_128680, _128340), -(in(_128680, _128338))]]], (277 ^ _120549) ^ [_130163, _130165, _130167] : [-(_130163 = unordered_pair(_130167, _130165)), 281 ^ _120549 : [(282 ^ _120549) ^ [] : [-(in(278 ^ [_130163, _130165, _130167], _130163))], (284 ^ _120549) ^ [] : [278 ^ [_130163, _130165, _130167] = _130167], (286 ^ _120549) ^ [] : [278 ^ [_130163, _130165, _130167] = _130165]], 287 ^ _120549 : [(294 ^ _120549) ^ [] : [in(278 ^ [_130163, _130165, _130167], _130163)], (288 ^ _120549) ^ [] : [-(278 ^ [_130163, _130165, _130167] = _130167), -(278 ^ [_130163, _130165, _130167] = _130165)]]], (255 ^ _120549) ^ [_129438, _129440, _129442] : [_129438 = unordered_pair(_129442, _129440), 258 ^ _120549 : [(269 ^ _120549) ^ [_129898] : [270 ^ _120549 : [(271 ^ _120549) ^ [] : [_129898 = _129442], (273 ^ _120549) ^ [] : [_129898 = _129440]], -(in(_129898, _129438))], (259 ^ _120549) ^ [_129620] : [in(_129620, _129438), -(_129620 = _129442), -(_129620 = _129440)]]], (320 ^ _120549) ^ [_131682, _131684, _131686] : [-(_131682 = set_union2(_131686, _131684)), 324 ^ _120549 : [(325 ^ _120549) ^ [] : [-(in(321 ^ [_131682, _131684, _131686], _131682))], (327 ^ _120549) ^ [] : [in(321 ^ [_131682, _131684, _131686], _131686)], (329 ^ _120549) ^ [] : [in(321 ^ [_131682, _131684, _131686], _131684)]], 330 ^ _120549 : [(337 ^ _120549) ^ [] : [in(321 ^ [_131682, _131684, _131686], _131682)], (331 ^ _120549) ^ [] : [-(in(321 ^ [_131682, _131684, _131686], _131686)), -(in(321 ^ [_131682, _131684, _131686], _131684))]]], (298 ^ _120549) ^ [_130957, _130959, _130961] : [_130957 = set_union2(_130961, _130959), 301 ^ _120549 : [(312 ^ _120549) ^ [_131417] : [313 ^ _120549 : [(314 ^ _120549) ^ [] : [in(_131417, _130961)], (316 ^ _120549) ^ [] : [in(_131417, _130959)]], -(in(_131417, _130957))], (302 ^ _120549) ^ [_131139] : [in(_131139, _130957), -(in(_131139, _130961)), -(in(_131139, _130959))]]], (351 ^ _120549) ^ [_132776, _132778] : [353 ^ _120549 : [(354 ^ _120549) ^ [] : [-(in(352 ^ [_132776, _132778], _132778))], (356 ^ _120549) ^ [] : [in(352 ^ [_132776, _132778], _132776)]], -(subset(_132778, _132776))], (341 ^ _120549) ^ [_132462, _132464] : [subset(_132464, _132462), 344 ^ _120549 : [(345 ^ _120549) ^ [_132599] : [in(_132599, _132464), -(in(_132599, _132462))]]], (382 ^ _120549) ^ [_133901, _133903, _133905] : [-(_133901 = set_intersection2(_133905, _133903)), 394 ^ _120549 : [(395 ^ _120549) ^ [] : [-(in(383 ^ [_133901, _133903, _133905], _133905))], (397 ^ _120549) ^ [] : [-(in(383 ^ [_133901, _133903, _133905], _133903))], (399 ^ _120549) ^ [] : [in(383 ^ [_133901, _133903, _133905], _133901)]], 386 ^ _120549 : [(387 ^ _120549) ^ [] : [-(in(383 ^ [_133901, _133903, _133905], _133901))], (389 ^ _120549) ^ [] : [in(383 ^ [_133901, _133903, _133905], _133905), in(383 ^ [_133901, _133903, _133905], _133903)]]], (360 ^ _120549) ^ [_133176, _133178, _133180] : [_133176 = set_intersection2(_133180, _133178), 363 ^ _120549 : [(364 ^ _120549) ^ [_133358] : [in(_133358, _133176), 367 ^ _120549 : [(368 ^ _120549) ^ [] : [-(in(_133358, _133180))], (370 ^ _120549) ^ [] : [-(in(_133358, _133178))]]], (372 ^ _120549) ^ [_133617] : [-(in(_133617, _133176)), in(_133617, _133180), in(_133617, _133178)]]], (426 ^ _120549) ^ [_135528, _135530] : [-(_135528 = union(_135530)), 439 ^ _120549 : [(440 ^ _120549) ^ [] : [-(in(427 ^ [_135528, _135530], 438 ^ [_135528, _135530]))], (442 ^ _120549) ^ [] : [-(in(438 ^ [_135528, _135530], _135530))], (444 ^ _120549) ^ [] : [in(427 ^ [_135528, _135530], _135528)]], 430 ^ _120549 : [(431 ^ _120549) ^ [] : [-(in(427 ^ [_135528, _135530], _135528))], (433 ^ _120549) ^ [_135811] : [in(427 ^ [_135528, _135530], _135811), in(_135811, _135530)]]], (403 ^ _120549) ^ [_134683, _134685] : [_134683 = union(_134685), 406 ^ _120549 : [(407 ^ _120549) ^ [_134864] : [in(_134864, _134683), 411 ^ _120549 : [(412 ^ _120549) ^ [] : [-(in(_134864, 410 ^ [_134683, _134685, _134864]))], (414 ^ _120549) ^ [] : [-(in(410 ^ [_134683, _134685, _134864], _134685))]]], (416 ^ _120549) ^ [_135191] : [-(in(_135191, _134683)), 417 ^ _120549 : [(418 ^ _120549) ^ [_135289] : [in(_135191, _135289), in(_135289, _134685)]]]]], (470 ^ _120549) ^ [_137149, _137151, _137153] : [-(_137149 = set_difference(_137153, _137151)), 482 ^ _120549 : [(483 ^ _120549) ^ [] : [-(in(471 ^ [_137149, _137151, _137153], _137153))], (485 ^ _120549) ^ [] : [in(471 ^ [_137149, _137151, _137153], _137151)], (487 ^ _120549) ^ [] : [in(471 ^ [_137149, _137151, _137153], _137149)]], 474 ^ _120549 : [(475 ^ _120549) ^ [] : [-(in(471 ^ [_137149, _137151, _137153], _137149))], (477 ^ _120549) ^ [] : [in(471 ^ [_137149, _137151, _137153], _137153), -(in(471 ^ [_137149, _137151, _137153], _137151))]]], (448 ^ _120549) ^ [_136418, _136420, _136422] : [_136418 = set_difference(_136422, _136420), 451 ^ _120549 : [(452 ^ _120549) ^ [_136602] : [in(_136602, _136418), 455 ^ _120549 : [(456 ^ _120549) ^ [] : [-(in(_136602, _136422))], (458 ^ _120549) ^ [] : [in(_136602, _136420)]]], (460 ^ _120549) ^ [_136862] : [-(in(_136862, _136418)), in(_136862, _136422), -(in(_136862, _136420))]]], (491 ^ _120549) ^ [_137935, _137937] : [disjoint(_137937, _137935), -(set_intersection2(_137937, _137935) = empty_set)], (497 ^ _120549) ^ [_138103, _138105] : [set_intersection2(_138105, _138103) = empty_set, -(disjoint(_138105, _138103))], (503 ^ _120549) ^ [_138350, _138352] : [proper_subset(_138352, _138350), 506 ^ _120549 : [(507 ^ _120549) ^ [] : [-(subset(_138352, _138350))], (509 ^ _120549) ^ [] : [_138352 = _138350]]], (511 ^ _120549) ^ [_138588, _138590] : [-(proper_subset(_138590, _138588)), subset(_138590, _138588), -(_138590 = _138588)], (521 ^ _120549) ^ [] : [true___, -(true___)], (527 ^ _120549) ^ [] : [true___, -(true___)], (533 ^ _120549) ^ [] : [true___, -(true___)], (539 ^ _120549) ^ [] : [true___, -(true___)], (545 ^ _120549) ^ [] : [true___, -(true___)], (551 ^ _120549) ^ [] : [true___, -(true___)], (557 ^ _120549) ^ [] : [true___, -(true___)], (563 ^ _120549) ^ [] : [true___, -(true___)], (569 ^ _120549) ^ [] : [-(empty(empty_set))], (571 ^ _120549) ^ [_139897, _139899] : [-(empty(_139899)), empty(set_union2(_139899, _139897))], (577 ^ _120549) ^ [_140113, _140115] : [-(empty(_140115)), empty(set_union2(_140113, _140115))], (583 ^ _120549) ^ [_140314, _140316] : [-(set_union2(_140316, _140316) = _140316)], (585 ^ _120549) ^ [_140411, _140413] : [-(set_intersection2(_140413, _140413) = _140413)], (587 ^ _120549) ^ [_140507, _140509] : [proper_subset(_140509, _140509)], (589 ^ _120549) ^ [_140586] : [singleton(_140586) = empty_set], (591 ^ _120549) ^ [_140695, _140697] : [in(_140697, _140695), -(set_union2(singleton(_140697), _140695) = _140695)], (597 ^ _120549) ^ [_140915, _140917] : [disjoint(singleton(_140917), _140915), in(_140917, _140915)], (603 ^ _120549) ^ [_141128, _141130] : [-(in(_141130, _141128)), -(disjoint(singleton(_141130), _141128))], (609 ^ _120549) ^ [_141374, _141376] : [subset(singleton(_141376), _141374), -(in(_141376, _141374))], (615 ^ _120549) ^ [_141540, _141542] : [in(_141542, _141540), -(subset(singleton(_141542), _141540))], (621 ^ _120549) ^ [_141785, _141787] : [set_difference(_141787, _141785) = empty_set, -(subset(_141787, _141785))], (627 ^ _120549) ^ [_141953, _141955] : [subset(_141955, _141953), -(set_difference(_141955, _141953) = empty_set)], (633 ^ _120549) ^ [_142185, _142187, _142189] : [subset(_142189, _142187), -(in(_142185, _142189)), -(subset(_142189, set_difference(_142187, singleton(_142185))))], (653 ^ _120549) ^ [_142794, _142796] : [654 ^ _120549 : [(655 ^ _120549) ^ [] : [_142796 = empty_set], (657 ^ _120549) ^ [] : [_142796 = singleton(_142794)]], -(subset(_142796, singleton(_142794)))], (643 ^ _120549) ^ [_142534, _142536] : [subset(_142536, singleton(_142534)), -(_142536 = empty_set), -(_142536 = singleton(_142534))], (662 ^ _120549) ^ [] : [-(empty(660 ^ []))], (665 ^ _120549) ^ [] : [empty(663 ^ [])], (667 ^ _120549) ^ [_143252, _143254] : [-(subset(_143254, _143254))], (669 ^ _120549) ^ [_143361, _143363] : [disjoint(_143363, _143361), -(disjoint(_143361, _143363))], (675 ^ _120549) ^ [_143599, _143601, _143603, _143605] : [unordered_pair(_143605, _143603) = unordered_pair(_143601, _143599), -(_143605 = _143601), -(_143605 = _143599)], (685 ^ _120549) ^ [_143935, _143937] : [subset(_143937, _143935), -(set_union2(_143937, _143935) = _143935)], (691 ^ _120549) ^ [_144136, _144138] : [-(subset(set_intersection2(_144138, _144136), _144138))], (693 ^ _120549) ^ [_144262, _144264, _144266] : [-(subset(_144266, set_intersection2(_144264, _144262))), subset(_144266, _144264), subset(_144266, _144262)], (703 ^ _120549) ^ [_144548] : [-(set_union2(_144548, empty_set) = _144548)], (705 ^ _120549) ^ [_144672, _144674, _144676] : [-(subset(_144676, _144672)), subset(_144676, _144674), subset(_144674, _144672)], (715 ^ _120549) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (717 ^ _120549) ^ [_145048, _145050, _145052] : [subset(_145052, _145050), -(subset(set_intersection2(_145052, _145048), set_intersection2(_145050, _145048)))], (723 ^ _120549) ^ [_145276, _145278] : [subset(_145278, _145276), -(set_intersection2(_145278, _145276) = _145278)], (729 ^ _120549) ^ [_145463] : [-(set_intersection2(_145463, empty_set) = empty_set)], (731 ^ _120549) ^ [_145573, _145575] : [-(_145575 = _145573), 735 ^ _120549 : [(736 ^ _120549) ^ [] : [-(in(732 ^ [_145573, _145575], _145575))], (738 ^ _120549) ^ [] : [in(732 ^ [_145573, _145575], _145573)]], 739 ^ _120549 : [(740 ^ _120549) ^ [] : [-(in(732 ^ [_145573, _145575], _145573))], (742 ^ _120549) ^ [] : [in(732 ^ [_145573, _145575], _145575)]]], (746 ^ _120549) ^ [_146074] : [-(subset(empty_set, _146074))], (748 ^ _120549) ^ [_146195, _146197, _146199] : [subset(_146199, _146197), -(subset(set_difference(_146199, _146195), set_difference(_146197, _146195)))], (754 ^ _120549) ^ [_146408, _146410] : [-(subset(set_difference(_146410, _146408), _146410))], (756 ^ _120549) ^ [_146549, _146551] : [set_difference(_146551, _146549) = empty_set, -(subset(_146551, _146549))], (762 ^ _120549) ^ [_146717, _146719] : [subset(_146719, _146717), -(set_difference(_146719, _146717) = empty_set)], (768 ^ _120549) ^ [_146920, _146922] : [-(set_union2(_146922, set_difference(_146920, _146922)) = set_union2(_146922, _146920))], (770 ^ _120549) ^ [_147009] : [-(set_difference(_147009, empty_set) = _147009)], (772 ^ _120549) ^ [_147139, _147141] : [-(disjoint(_147141, _147139)), 776 ^ _120549 : [(777 ^ _120549) ^ [] : [-(in(775 ^ [_147139, _147141], _147141))], (779 ^ _120549) ^ [] : [-(in(775 ^ [_147139, _147141], _147139))]]], (781 ^ _120549) ^ [_147453, _147455] : [disjoint(_147455, _147453), 782 ^ _120549 : [(783 ^ _120549) ^ [_147545] : [in(_147545, _147455), in(_147545, _147453)]]], (791 ^ _120549) ^ [_147802] : [subset(_147802, empty_set), -(_147802 = empty_set)], (797 ^ _120549) ^ [_147991, _147993] : [-(set_difference(set_union2(_147993, _147991), _147991) = set_difference(_147993, _147991))], (799 ^ _120549) ^ [_148109, _148111] : [subset(_148111, _148109), -(_148109 = set_union2(_148111, set_difference(_148109, _148111)))], (805 ^ _120549) ^ [_148316, _148318] : [-(set_difference(_148318, set_difference(_148318, _148316)) = set_intersection2(_148318, _148316))], (807 ^ _120549) ^ [_148405] : [-(set_difference(empty_set, _148405) = empty_set)], (809 ^ _120549) ^ [_148535, _148537] : [-(disjoint(_148537, _148535)), -(in(812 ^ [_148535, _148537], set_intersection2(_148537, _148535)))], (816 ^ _120549) ^ [_148770, _148772] : [817 ^ _120549 : [(818 ^ _120549) ^ [_148843] : [in(_148843, set_intersection2(_148772, _148770))]], disjoint(_148772, _148770)], (822 ^ _120549) ^ [_149009, _149011] : [subset(_149011, _149009), proper_subset(_149009, _149011)], (828 ^ _120549) ^ [_149232, _149234, _149236] : [-(disjoint(_149236, _149232)), subset(_149236, _149234), disjoint(_149234, _149232)], (838 ^ _120549) ^ [_149512] : [-(unordered_pair(_149512, _149512) = singleton(_149512))], (840 ^ _120549) ^ [_149610] : [empty(_149610), -(_149610 = empty_set)], (846 ^ _120549) ^ [_149812, _149814] : [subset(singleton(_149814), singleton(_149812)), -(_149814 = _149812)], (852 ^ _120549) ^ [_150030, _150032] : [in(_150032, _150030), empty(_150030)], (858 ^ _120549) ^ [_150222, _150224] : [-(subset(_150224, set_union2(_150224, _150222)))], (860 ^ _120549) ^ [_150363, _150365] : [disjoint(_150365, _150363), -(set_difference(_150365, _150363) = _150365)], (866 ^ _120549) ^ [_150531, _150533] : [set_difference(_150533, _150531) = _150533, -(disjoint(_150533, _150531))], (872 ^ _120549) ^ [_150749, _150751] : [empty(_150751), -(_150751 = _150749), empty(_150749)], (882 ^ _120549) ^ [_151060, _151062, _151064] : [-(subset(set_union2(_151064, _151060), _151062)), subset(_151064, _151062), subset(_151060, _151062)], (892 ^ _120549) ^ [_151389, _151391, _151393] : [singleton(_151393) = unordered_pair(_151391, _151389), -(_151393 = _151391)], (898 ^ _120549) ^ [_151609, _151611, _151613] : [singleton(_151613) = unordered_pair(_151611, _151609), -(_151611 = _151609)]], input).
% 0.74/1.38 ncf('1',plain,[subset(903 ^ [], union(904 ^ []))],start(908 ^ 0)).
% 0.74/1.38 ncf('1.1',plain,[-(subset(903 ^ [], union(904 ^ []))), 356 : in(352 ^ [union(904 ^ []), 903 ^ []], union(904 ^ []))],extension(351 ^ 1,bind([[_132776, _132778], [union(904 ^ []), 903 ^ []]]))).
% 0.74/1.38 ncf('1.1.1',plain,[-(in(352 ^ [union(904 ^ []), 903 ^ []], union(904 ^ []))), 418 : in(352 ^ [union(904 ^ []), 903 ^ []], 903 ^ []), 418 : in(903 ^ [], 904 ^ []), 416 : union(904 ^ []) = union(904 ^ [])],extension(403 ^ 4,bind([[_134683, _134685, _135191, _135289], [union(904 ^ []), 904 ^ [], 352 ^ [union(904 ^ []), 903 ^ []], 903 ^ []]]))).
% 0.74/1.38 ncf('1.1.1.1',plain,[-(in(352 ^ [union(904 ^ []), 903 ^ []], 903 ^ []))],extension(354 ^ 9)).
% 0.74/1.38 ncf('1.1.1.2',plain,[-(in(903 ^ [], 904 ^ []))],extension(906 ^ 9)).
% 0.74/1.38 ncf('1.1.1.3',plain,[-(union(904 ^ []) = union(904 ^ []))],extension(2 ^ 5,bind([[_120693], [union(904 ^ [])]]))).
% 0.74/1.38 %-----------------------------------------------------
% 0.74/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------