%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU206+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:39 EDT 2023
% Result : Theorem 0.80s 1.32s
% Output : Proof 0.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SEU206+1 : TPTP v8.1.2. Released v3.3.0.
% 0.10/0.10 % Command : nanocop.sh %s %d
% 0.10/0.28 % Computer : n032.cluster.edu
% 0.10/0.28 % Model : x86_64 x86_64
% 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.28 % Memory : 8042.1875MB
% 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.28 % CPULimit : 300
% 0.10/0.28 % WCLimit : 300
% 0.10/0.28 % DateTime : Thu May 18 12:53:49 EDT 2023
% 0.10/0.28 % CPUTime :
% 0.80/1.32
% 0.80/1.32 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.80/1.32 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.80/1.32 %-----------------------------------------------------
% 0.80/1.32 ncf(matrix, plain, [(528 ^ _73500) ^ [] : [-(relation(526 ^ []))], (530 ^ _73500) ^ [] : [relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_rng(526 ^ [])], (82 ^ _73500) ^ [_76212, _76214, _76216, _76218] : [-(ordered_pair(_76218, _76214) = ordered_pair(_76216, _76212)), _76218 = _76216, _76214 = _76212], (92 ^ _73500) ^ [_76543, _76545] : [_76545 = _76543, -(singleton(_76545) = singleton(_76543))], (98 ^ _73500) ^ [_76789, _76791, _76793, _76795] : [-(unordered_pair(_76795, _76791) = unordered_pair(_76793, _76789)), _76795 = _76793, _76791 = _76789], (108 ^ _73500) ^ [_77120, _77122] : [_77122 = _77120, -(powerset(_77122) = powerset(_77120))], (114 ^ _73500) ^ [_77366, _77368, _77370, _77372] : [-(relation_image(_77372, _77368) = relation_image(_77370, _77366)), _77372 = _77370, _77368 = _77366], (124 ^ _73500) ^ [_77697, _77699] : [_77699 = _77697, -(relation_dom(_77699) = relation_dom(_77697))], (130 ^ _73500) ^ [_77895, _77897] : [_77897 = _77895, -(relation_rng(_77897) = relation_rng(_77895))], (2 ^ _73500) ^ [_73644] : [-(_73644 = _73644)], (4 ^ _73500) ^ [_73751, _73753] : [_73753 = _73751, -(_73751 = _73753)], (10 ^ _73500) ^ [_73955, _73957, _73959] : [-(_73959 = _73955), _73959 = _73957, _73957 = _73955], (20 ^ _73500) ^ [_74296, _74298, _74300, _74302] : [-(subset(_74300, _74296)), subset(_74302, _74298), _74302 = _74300, _74298 = _74296], (34 ^ _73500) ^ [_74740, _74742, _74744, _74746] : [-(element(_74744, _74740)), element(_74746, _74742), _74746 = _74744, _74742 = _74740], (48 ^ _73500) ^ [_75184, _75186, _75188, _75190] : [-(in(_75188, _75184)), in(_75190, _75186), _75190 = _75188, _75186 = _75184], (62 ^ _73500) ^ [_75600, _75602] : [-(empty(_75600)), _75602 = _75600, empty(_75602)], (72 ^ _73500) ^ [_75875, _75877] : [-(relation(_75875)), _75877 = _75875, relation(_75877)], (136 ^ _73500) ^ [_78139, _78141] : [in(_78141, _78139), in(_78139, _78141)], (142 ^ _73500) ^ [_78336] : [empty(_78336), -(relation(_78336))], (148 ^ _73500) ^ [_78521, _78523] : [-(unordered_pair(_78523, _78521) = unordered_pair(_78521, _78523))], (150 ^ _73500) ^ [_78665, _78667] : [_78667 = _78665, 153 ^ _73500 : [(154 ^ _73500) ^ [] : [-(subset(_78667, _78665))], (156 ^ _73500) ^ [] : [-(subset(_78665, _78667))]]], (158 ^ _73500) ^ [_78902, _78904] : [-(_78904 = _78902), subset(_78904, _78902), subset(_78902, _78904)], (168 ^ _73500) ^ [_79189] : [relation(_79189), 171 ^ _73500 : [(195 ^ _73500) ^ [_80302, _80304] : [-(_80302 = relation_image(_79189, _80304)), 208 ^ _73500 : [(209 ^ _73500) ^ [] : [-(in(ordered_pair(207 ^ [_79189, _80302, _80304], 196 ^ [_79189, _80302, _80304]), _79189))], (211 ^ _73500) ^ [] : [-(in(207 ^ [_79189, _80302, _80304], _80304))], (213 ^ _73500) ^ [] : [in(196 ^ [_79189, _80302, _80304], _80302)]], 199 ^ _73500 : [(200 ^ _73500) ^ [] : [-(in(196 ^ [_79189, _80302, _80304], _80302))], (202 ^ _73500) ^ [_80606] : [in(ordered_pair(_80606, 196 ^ [_79189, _80302, _80304]), _79189), in(_80606, _80304)]]], (172 ^ _73500) ^ [_79396, _79398] : [_79396 = relation_image(_79189, _79398), 175 ^ _73500 : [(176 ^ _73500) ^ [_79588] : [in(_79588, _79396), 180 ^ _73500 : [(181 ^ _73500) ^ [] : [-(in(ordered_pair(179 ^ [_79189, _79396, _79398, _79588], _79588), _79189))], (183 ^ _73500) ^ [] : [-(in(179 ^ [_79189, _79396, _79398, _79588], _79398))]]], (185 ^ _73500) ^ [_79942] : [-(in(_79942, _79396)), 186 ^ _73500 : [(187 ^ _73500) ^ [_80047] : [in(ordered_pair(_80047, _79942), _79189), in(_80047, _79398)]]]]]]], (227 ^ _73500) ^ [_81565, _81567] : [229 ^ _73500 : [(230 ^ _73500) ^ [] : [-(in(228 ^ [_81565, _81567], _81567))], (232 ^ _73500) ^ [] : [in(228 ^ [_81565, _81567], _81565)]], -(subset(_81567, _81565))], (217 ^ _73500) ^ [_81251, _81253] : [subset(_81253, _81251), 220 ^ _73500 : [(221 ^ _73500) ^ [_81388] : [in(_81388, _81253), -(in(_81388, _81251))]]], (236 ^ _73500) ^ [_81908] : [relation(_81908), 239 ^ _73500 : [(257 ^ _73500) ^ [_82720] : [-(_82720 = relation_dom(_81908)), 261 ^ _73500 : [(262 ^ _73500) ^ [] : [-(in(258 ^ [_81908, _82720], _82720))], (264 ^ _73500) ^ [_82983] : [in(ordered_pair(258 ^ [_81908, _82720], _82983), _81908)]], 266 ^ _73500 : [(267 ^ _73500) ^ [] : [-(in(ordered_pair(258 ^ [_81908, _82720], 265 ^ [_81908, _82720]), _81908))], (269 ^ _73500) ^ [] : [in(258 ^ [_81908, _82720], _82720)]]], (240 ^ _73500) ^ [_82089] : [_82089 = relation_dom(_81908), 243 ^ _73500 : [(244 ^ _73500) ^ [_82269] : [in(_82269, _82089), -(in(ordered_pair(_82269, 247 ^ [_81908, _82089, _82269]), _81908))], (251 ^ _73500) ^ [_82513] : [252 ^ _73500 : [(253 ^ _73500) ^ [_82592] : [in(ordered_pair(_82513, _82592), _81908)]], -(in(_82513, _82089))]]]]], (273 ^ _73500) ^ [_83349] : [relation(_83349), 276 ^ _73500 : [(294 ^ _73500) ^ [_84161] : [-(_84161 = relation_rng(_83349)), 298 ^ _73500 : [(299 ^ _73500) ^ [] : [-(in(295 ^ [_83349, _84161], _84161))], (301 ^ _73500) ^ [_84424] : [in(ordered_pair(_84424, 295 ^ [_83349, _84161]), _83349)]], 303 ^ _73500 : [(304 ^ _73500) ^ [] : [-(in(ordered_pair(302 ^ [_83349, _84161], 295 ^ [_83349, _84161]), _83349))], (306 ^ _73500) ^ [] : [in(295 ^ [_83349, _84161], _84161)]]], (277 ^ _73500) ^ [_83530] : [_83530 = relation_rng(_83349), 280 ^ _73500 : [(281 ^ _73500) ^ [_83710] : [in(_83710, _83530), -(in(ordered_pair(284 ^ [_83349, _83530, _83710], _83710), _83349))], (288 ^ _73500) ^ [_83954] : [289 ^ _73500 : [(290 ^ _73500) ^ [_84033] : [in(ordered_pair(_84033, _83954), _83349)]], -(in(_83954, _83530))]]]]], (310 ^ _73500) ^ [_84789, _84791] : [-(ordered_pair(_84791, _84789) = unordered_pair(unordered_pair(_84791, _84789), singleton(_84791)))], (312 ^ _73500) ^ [] : [true___, -(true___)], (318 ^ _73500) ^ [] : [true___, -(true___)], (324 ^ _73500) ^ [] : [true___, -(true___)], (330 ^ _73500) ^ [] : [true___, -(true___)], (336 ^ _73500) ^ [] : [true___, -(true___)], (342 ^ _73500) ^ [] : [true___, -(true___)], (348 ^ _73500) ^ [] : [true___, -(true___)], (354 ^ _73500) ^ [] : [true___, -(true___)], (360 ^ _73500) ^ [] : [true___, -(true___)], (367 ^ _73500) ^ [_85990] : [-(element(365 ^ [_85990], _85990))], (369 ^ _73500) ^ [_86072] : [empty(powerset(_86072))], (371 ^ _73500) ^ [] : [-(empty(empty_set))], (373 ^ _73500) ^ [_86217, _86219] : [empty(ordered_pair(_86219, _86217))], (375 ^ _73500) ^ [_86298] : [empty(singleton(_86298))], (377 ^ _73500) ^ [_86390, _86392] : [empty(unordered_pair(_86392, _86390))], (379 ^ _73500) ^ [] : [-(empty(empty_set))], (381 ^ _73500) ^ [] : [-(relation(empty_set))], (383 ^ _73500) ^ [_86595] : [empty(relation_dom(_86595)), -(empty(_86595)), relation(_86595)], (393 ^ _73500) ^ [_86872] : [empty(relation_rng(_86872)), -(empty(_86872)), relation(_86872)], (403 ^ _73500) ^ [_87149] : [empty(_87149), 406 ^ _73500 : [(407 ^ _73500) ^ [] : [-(empty(relation_dom(_87149)))], (409 ^ _73500) ^ [] : [-(relation(relation_dom(_87149)))]]], (411 ^ _73500) ^ [_87414] : [empty(_87414), 414 ^ _73500 : [(415 ^ _73500) ^ [] : [-(empty(relation_rng(_87414)))], (417 ^ _73500) ^ [] : [-(relation(relation_rng(_87414)))]]], (420 ^ _73500) ^ [] : [-(empty(418 ^ []))], (422 ^ _73500) ^ [] : [-(relation(418 ^ []))], (424 ^ _73500) ^ [_87828] : [-(empty(_87828)), 428 ^ _73500 : [(429 ^ _73500) ^ [] : [-(element(427 ^ [_87828], powerset(_87828)))], (431 ^ _73500) ^ [] : [empty(427 ^ [_87828])]]], (434 ^ _73500) ^ [] : [-(empty(432 ^ []))], (437 ^ _73500) ^ [] : [empty(435 ^ [])], (439 ^ _73500) ^ [] : [-(relation(435 ^ []))], (442 ^ _73500) ^ [_88450] : [-(element(440 ^ [_88450], powerset(_88450)))], (444 ^ _73500) ^ [_88501] : [-(empty(440 ^ [_88501]))], (447 ^ _73500) ^ [] : [empty(445 ^ [])], (449 ^ _73500) ^ [_88689, _88691] : [-(subset(_88691, _88691))], (451 ^ _73500) ^ [_88798, _88800] : [relation(_88798), -(subset(relation_image(_88798, _88800), relation_rng(_88798)))], (457 ^ _73500) ^ [_89016, _89018] : [in(_89018, _89016), -(element(_89018, _89016))], (463 ^ _73500) ^ [_89226, _89228] : [element(_89228, _89226), -(empty(_89226)), -(in(_89228, _89226))], (473 ^ _73500) ^ [_89553, _89555] : [element(_89555, powerset(_89553)), -(subset(_89555, _89553))], (479 ^ _73500) ^ [_89719, _89721] : [subset(_89721, _89719), -(element(_89721, powerset(_89719)))], (485 ^ _73500) ^ [_89949, _89951, _89953] : [-(element(_89953, _89949)), in(_89953, _89951), element(_89951, powerset(_89949))], (495 ^ _73500) ^ [_90276, _90278, _90280] : [in(_90280, _90278), element(_90278, powerset(_90276)), empty(_90276)], (505 ^ _73500) ^ [_90572] : [empty(_90572), -(_90572 = empty_set)], (511 ^ _73500) ^ [_90774, _90776] : [in(_90776, _90774), empty(_90774)], (517 ^ _73500) ^ [_90961, _90963] : [empty(_90963), -(_90963 = _90961), empty(_90961)]], input).
% 0.80/1.32 ncf('1',plain,[relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_rng(526 ^ [])],start(530 ^ 0)).
% 0.80/1.32 ncf('1.1',plain,[-(relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_rng(526 ^ [])), 301 : in(ordered_pair(179 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ [])), relation_dom(526 ^ []), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ []), 306 : in(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ []))), 294 : relation(526 ^ [])],extension(273 ^ 1,bind([[_83349, _84161, _84424], [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ [])), 179 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ [])), relation_dom(526 ^ []), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]]]]))).
% 0.80/1.32 ncf('1.1.1',plain,[-(in(ordered_pair(179 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ [])), relation_dom(526 ^ []), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ [])), 176 : in(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ []))), 176 : relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_image(526 ^ [], relation_dom(526 ^ [])), 172 : relation(526 ^ [])],extension(168 ^ 6,bind([[_79189, _79396, _79398, _79588], [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ [])), relation_dom(526 ^ []), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]]]))).
% 0.80/1.32 ncf('1.1.1.1',plain,[-(in(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ [])))), in(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ []))), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))] = 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_image(526 ^ [], relation_dom(526 ^ []))],extension(48 ^ 11,bind([[_75184, _75186, _75188, _75190], [relation_image(526 ^ [], relation_dom(526 ^ [])), relation_image(526 ^ [], relation_dom(526 ^ [])), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]]]))).
% 0.80/1.32 ncf('1.1.1.1.1',plain,[-(in(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ []))))],extension(299 ^ 12)).
% 0.80/1.32 ncf('1.1.1.1.2',plain,[-(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))] = 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))])],extension(2 ^ 12,bind([[_73644], [295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]]]))).
% 0.80/1.32 ncf('1.1.1.1.3',plain,[-(relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_image(526 ^ [], relation_dom(526 ^ [])))],extension(2 ^ 12,bind([[_73644], [relation_image(526 ^ [], relation_dom(526 ^ []))]]))).
% 0.80/1.32 ncf('1.1.1.2',plain,[-(relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_image(526 ^ [], relation_dom(526 ^ []))), 526 ^ [] = 526 ^ [], relation_dom(526 ^ []) = relation_dom(526 ^ [])],extension(114 ^ 9,bind([[_77366, _77368, _77370, _77372], [relation_dom(526 ^ []), relation_dom(526 ^ []), 526 ^ [], 526 ^ []]]))).
% 0.80/1.32 ncf('1.1.1.2.1',plain,[-(526 ^ [] = 526 ^ [])],extension(2 ^ 10,bind([[_73644], [526 ^ []]]))).
% 0.80/1.32 ncf('1.1.1.2.2',plain,[-(relation_dom(526 ^ []) = relation_dom(526 ^ []))],extension(2 ^ 10,bind([[_73644], [relation_dom(526 ^ [])]]))).
% 0.80/1.32 ncf('1.1.1.3',plain,[-(relation(526 ^ []))],extension(528 ^ 7)).
% 0.80/1.32 ncf('1.1.2',plain,[-(in(295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_image(526 ^ [], relation_dom(526 ^ [])))), 187 : in(ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ []), 187 : in(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_dom(526 ^ [])), 185 : relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_image(526 ^ [], relation_dom(526 ^ [])), 172 : relation(526 ^ [])],extension(168 ^ 6,bind([[_79189, _79396, _79398, _79942, _80047], [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ [])), relation_dom(526 ^ []), 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]]]))).
% 0.80/1.32 ncf('1.1.2.1',plain,[-(in(ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ [])), 221 : in(ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ []), 221 : subset(526 ^ [], 526 ^ [])],extension(217 ^ 13,bind([[_81251, _81253, _81388], [526 ^ [], 526 ^ [], ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))])]]))).
% 0.80/1.32 ncf('1.1.2.1.1',plain,[-(in(ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ []))],extension(304 ^ 16)).
% 0.80/1.32 ncf('1.1.2.1.2',plain,[-(subset(526 ^ [], 526 ^ []))],extension(449 ^ 14,bind([[_88689, _88691], [_54404, 526 ^ []]]))).
% 0.80/1.32 ncf('1.1.2.2',plain,[-(in(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], relation_dom(526 ^ []))), 253 : in(ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ []), 251 : relation_dom(526 ^ []) = relation_dom(526 ^ []), 240 : relation(526 ^ [])],extension(236 ^ 13,bind([[_81908, _82089, _82513, _82592], [526 ^ [], relation_dom(526 ^ []), 302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]]]))).
% 0.80/1.32 ncf('1.1.2.2.1',plain,[-(in(ordered_pair(302 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))], 295 ^ [526 ^ [], relation_image(526 ^ [], relation_dom(526 ^ []))]), 526 ^ []))],extension(304 ^ 20)).
% 0.80/1.32 ncf('1.1.2.2.2',plain,[-(relation_dom(526 ^ []) = relation_dom(526 ^ []))],extension(2 ^ 16,bind([[_73644], [relation_dom(526 ^ [])]]))).
% 0.80/1.32 ncf('1.1.2.2.3',plain,[-(relation(526 ^ []))],extension(528 ^ 14)).
% 0.80/1.32 ncf('1.1.2.3',plain,[-(relation_image(526 ^ [], relation_dom(526 ^ [])) = relation_image(526 ^ [], relation_dom(526 ^ []))), 526 ^ [] = 526 ^ [], relation_dom(526 ^ []) = relation_dom(526 ^ [])],extension(114 ^ 9,bind([[_77366, _77368, _77370, _77372], [relation_dom(526 ^ []), relation_dom(526 ^ []), 526 ^ [], 526 ^ []]]))).
% 0.80/1.32 ncf('1.1.2.3.1',plain,[-(526 ^ [] = 526 ^ [])],extension(2 ^ 10,bind([[_73644], [526 ^ []]]))).
% 0.80/1.32 ncf('1.1.2.3.2',plain,[-(relation_dom(526 ^ []) = relation_dom(526 ^ [])), 526 ^ [] = 526 ^ []],extension(124 ^ 10,bind([[_77697, _77699], [526 ^ [], 526 ^ []]]))).
% 0.80/1.32 ncf('1.1.2.3.2.1',plain,[-(526 ^ [] = 526 ^ [])],lemmata('[2, 1, 1].x')).
% 0.80/1.32 ncf('1.1.2.4',plain,[-(relation(526 ^ []))],extension(528 ^ 7)).
% 0.80/1.32 ncf('1.1.3',plain,[-(relation(526 ^ []))],extension(528 ^ 2)).
% 0.80/1.32 %-----------------------------------------------------
% 0.80/1.32 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------