%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET990+1 : TPTP v8.1.2. Released v3.2.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 11:56:47 EDT 2023
% Result : Theorem 231.05s 223.75s
% Output : Proof 231.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET990+1 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n014.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 18:59:42 EDT 2023
% 0.12/0.35 % CPUTime :
% 231.05/223.75
% 231.05/223.75 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 231.05/223.75 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 231.05/223.75 %-----------------------------------------------------
% 231.05/223.75 ncf(matrix, plain, [(471 ^ _120870) ^ [] : [452 ^ [] = 457 ^ []], (459 ^ _120870) ^ [] : [-(relation(457 ^ []))], (461 ^ _120870) ^ [] : [-(function(457 ^ []))], (454 ^ _120870) ^ [] : [-(relation(452 ^ []))], (465 ^ _120870) ^ [_121296] : [in(_121296, relation_dom(452 ^ [])), -(apply(452 ^ [], _121296) = apply(457 ^ [], _121296))], (463 ^ _120870) ^ [] : [-(relation_dom(452 ^ []) = relation_dom(457 ^ []))], (456 ^ _120870) ^ [] : [-(function(452 ^ []))], !, (351 ^ _105123) ^ [_117088, _117090] : [-(subset(_117090, _117090))], (102 ^ _105123) ^ [_108381, _108383] : [_108383 = _108381, -(singleton(_108383) = singleton(_108381))], (383 ^ _105123) ^ [_118466, _118468] : [in(_118468, _118466), -(element(_118468, _118466))], (275 ^ _105123) ^ [] : [-(relation(empty_set))], (283 ^ _105123) ^ [_114860, _114862] : [empty(ordered_pair(_114862, _114860))], (289 ^ _105123) ^ [] : [-(empty(empty_set))], (411 ^ _105123) ^ [_119399, _119401, _119403] : [-(element(_119403, _119399)), in(_119403, _119401), element(_119401, powerset(_119399))], (281 ^ _105123) ^ [] : [-(empty(empty_set))], (44 ^ _105123) ^ [_106638, _106640, _106642, _106644] : [-(element(_106642, _106638)), element(_106644, _106640), _106644 = _106642, _106640 = _106638], (108 ^ _105123) ^ [_108627, _108629, _108631, _108633] : [-(unordered_pair(_108633, _108629) = unordered_pair(_108631, _108627)), _108633 = _108631, _108629 = _108627], (191 ^ _105123) ^ [_111667] : [relation(_111667), function(_111667), 198 ^ _105123 : [(215 ^ _105123) ^ [_112411, _112413] : [-(in(_112413, relation_dom(_111667))), 218 ^ _105123 : [(225 ^ _105123) ^ [] : [_112411 = empty_set, -(_112411 = apply(_111667, _112413))], (219 ^ _105123) ^ [] : [_112411 = apply(_111667, _112413), -(_112411 = empty_set)]]], (199 ^ _105123) ^ [_111959, _111961] : [in(_111961, relation_dom(_111667)), 202 ^ _105123 : [(209 ^ _105123) ^ [] : [in(ordered_pair(_111961, _111959), _111667), -(_111959 = apply(_111667, _111961))], (203 ^ _105123) ^ [] : [_111959 = apply(_111667, _111961), -(in(ordered_pair(_111961, _111959), _111667))]]]]], (231 ^ _105123) ^ [_112900] : [relation(_112900), 234 ^ _105123 : [(235 ^ _105123) ^ [_113081] : [_113081 = relation_dom(_112900), 238 ^ _105123 : [(246 ^ _105123) ^ [_113505] : [247 ^ _105123 : [(248 ^ _105123) ^ [_113584] : [in(ordered_pair(_113505, _113584), _112900)]], -(in(_113505, _113081))], (239 ^ _105123) ^ [_113261] : [in(_113261, _113081), -(in(ordered_pair(_113261, 242 ^ [_112900, _113081, _113261]), _112900))]]], (252 ^ _105123) ^ [_113712] : [-(_113712 = relation_dom(_112900)), 256 ^ _105123 : [(259 ^ _105123) ^ [_113975] : [in(ordered_pair(253 ^ [_112900, _113712], _113975), _112900)], (257 ^ _105123) ^ [] : [-(in(253 ^ [_112900, _113712], _113712))]], 261 ^ _105123 : [(264 ^ _105123) ^ [] : [in(253 ^ [_112900, _113712], _113712)], (262 ^ _105123) ^ [] : [-(in(ordered_pair(253 ^ [_112900, _113712], 260 ^ [_112900, _113712]), _112900))]]]]], (431 ^ _105123) ^ [_120022] : [empty(_120022), -(_120022 = empty_set)], (405 ^ _105123) ^ [_119169, _119171] : [subset(_119171, _119169), -(element(_119171, powerset(_119169)))], (273 ^ _105123) ^ [] : [-(empty(empty_set))], (128 ^ _105123) ^ [_109317, _109319] : [_109319 = _109317, -(powerset(_109319) = powerset(_109317))], (312 ^ _105123) ^ [] : [-(relation(310 ^ []))], (399 ^ _105123) ^ [_119003, _119005] : [element(_119005, powerset(_119003)), -(subset(_119005, _119003))], (68 ^ _105123) ^ [_107349, _107351] : [-(relation(_107349)), _107351 = _107349, relation(_107351)], (341 ^ _105123) ^ [_116751] : [-(empty(337 ^ [_116751]))], (168 ^ _105123) ^ [_110682, _110684] : [-(unordered_pair(_110684, _110682) = unordered_pair(_110682, _110684))], (336 ^ _105123) ^ [] : [-(relation(332 ^ []))], (314 ^ _105123) ^ [] : [-(function(310 ^ []))], (182 ^ _105123) ^ [_111273] : [184 ^ _105123 : [(187 ^ _105123) ^ [_111510, _111512] : [183 ^ [_111273] = ordered_pair(_111512, _111510)], (185 ^ _105123) ^ [] : [-(in(183 ^ [_111273], _111273))]], -(relation(_111273))], (443 ^ _105123) ^ [_120411, _120413] : [empty(_120413), -(_120413 = _120411), empty(_120411)], (134 ^ _105123) ^ [_109535, _109537] : [_109537 = _109535, -(relation_dom(_109537) = relation_dom(_109535))], (20 ^ _105123) ^ [_105871, _105873] : [-(relation_empty_yielding(_105871)), _105873 = _105871, relation_empty_yielding(_105873)], (170 ^ _105123) ^ [_110812] : [relation(_110812), 173 ^ _105123 : [(174 ^ _105123) ^ [_110960] : [in(_110960, _110812), -(_110960 = ordered_pair(177 ^ [_110812, _110960], 178 ^ [_110812, _110960]))]]], (331 ^ _105123) ^ [] : [-(empty(329 ^ []))], (268 ^ _105123) ^ [_114340, _114342] : [-(ordered_pair(_114342, _114340) = unordered_pair(unordered_pair(_114342, _114340), singleton(_114342)))], (156 ^ _105123) ^ [_110311] : [empty(_110311), -(function(_110311))], (293 ^ _105123) ^ [_115238] : [empty(relation_dom(_115238)), -(empty(_115238)), relation(_115238)], (279 ^ _105123) ^ [_114715] : [empty(powerset(_114715))], (30 ^ _105123) ^ [_106194, _106196, _106198, _106200] : [-(subset(_106198, _106194)), subset(_106200, _106196), _106200 = _106198, _106196 = _106194], (285 ^ _105123) ^ [_114941] : [empty(singleton(_114941))], (277 ^ _105123) ^ [] : [-(relation_empty_yielding(empty_set))], (291 ^ _105123) ^ [] : [-(relation(empty_set))], (339 ^ _105123) ^ [_116700] : [-(element(337 ^ [_116700], powerset(_116700)))], (140 ^ _105123) ^ [_109761, _109763, _109765, _109767] : [-(apply(_109767, _109763) = apply(_109765, _109761)), _109767 = _109765, _109763 = _109761], (303 ^ _105123) ^ [_115515] : [empty(_115515), 306 ^ _105123 : [(309 ^ _105123) ^ [] : [-(relation(relation_dom(_115515)))], (307 ^ _105123) ^ [] : [-(empty(relation_dom(_115515)))]]], (389 ^ _105123) ^ [_118676, _118678] : [element(_118678, _118676), -(empty(_118676)), -(in(_118678, _118676))], (162 ^ _105123) ^ [_110497] : [empty(_110497), -(relation(_110497))], (88 ^ _105123) ^ [_107947, _107949, _107951, _107953] : [-(in(_107951, _107947)), in(_107953, _107949), _107953 = _107951, _107949 = _107947], (421 ^ _105123) ^ [_119726, _119728, _119730] : [in(_119730, _119728), element(_119728, powerset(_119726)), empty(_119726)], (317 ^ _105123) ^ [] : [-(empty(315 ^ []))], (321 ^ _105123) ^ [_116078] : [-(empty(_116078)), 325 ^ _105123 : [(328 ^ _105123) ^ [] : [empty(324 ^ [_116078])], (326 ^ _105123) ^ [] : [-(element(324 ^ [_116078], powerset(_116078)))]]], (2 ^ _105123) ^ [_105247] : [-(_105247 = _105247)], (271 ^ _105123) ^ [_114470] : [-(element(269 ^ [_114470], _114470))], (287 ^ _105123) ^ [_115033, _115035] : [empty(unordered_pair(_115035, _115033))], (78 ^ _105123) ^ [_107644, _107646] : [-(function(_107644)), _107646 = _107644, function(_107646)], (319 ^ _105123) ^ [] : [-(relation(315 ^ []))], (347 ^ _105123) ^ [] : [-(relation(345 ^ []))], (58 ^ _105123) ^ [_107054, _107056] : [-(empty(_107054)), _107056 = _107054, empty(_107056)], (334 ^ _105123) ^ [] : [empty(332 ^ [])], (349 ^ _105123) ^ [] : [-(relation_empty_yielding(345 ^ []))], (353 ^ _105123) ^ [_117197, _117199] : [-(_117199 = _117197), 357 ^ _105123 : [(360 ^ _105123) ^ [_117541, _117543] : [356 ^ [_117197, _117199] = ordered_pair(_117543, _117541)], (358 ^ _105123) ^ [] : [-(in(356 ^ [_117197, _117199], _117199))]], 364 ^ _105123 : [(367 ^ _105123) ^ [_117805, _117807] : [363 ^ [_117197, _117199] = ordered_pair(_117807, _117805)], (365 ^ _105123) ^ [] : [-(in(363 ^ [_117197, _117199], _117197))]], 372 ^ _105123 : [(375 ^ _105123) ^ [] : [in(ordered_pair(368 ^ [_117197, _117199], 369 ^ [_117197, _117199]), _117197)], (373 ^ _105123) ^ [] : [-(in(ordered_pair(368 ^ [_117197, _117199], 369 ^ [_117197, _117199]), _117199))]], 376 ^ _105123 : [(379 ^ _105123) ^ [] : [in(ordered_pair(368 ^ [_117197, _117199], 369 ^ [_117197, _117199]), _117199)], (377 ^ _105123) ^ [] : [-(in(ordered_pair(368 ^ [_117197, _117199], 369 ^ [_117197, _117199]), _117197))]]], (4 ^ _105123) ^ [_105354, _105356] : [_105356 = _105354, -(_105354 = _105356)], (118 ^ _105123) ^ [_108986, _108988, _108990, _108992] : [-(ordered_pair(_108992, _108988) = ordered_pair(_108990, _108986)), _108992 = _108990, _108988 = _108986], (10 ^ _105123) ^ [_105558, _105560, _105562] : [-(_105562 = _105558), _105562 = _105560, _105560 = _105558], (344 ^ _105123) ^ [] : [empty(342 ^ [])], (150 ^ _105123) ^ [_110114, _110116] : [in(_110116, _110114), in(_110114, _110116)], (437 ^ _105123) ^ [_120224, _120226] : [in(_120226, _120224), empty(_120224)]], input).
% 231.05/223.75 ncf('1',plain,[452 ^ [] = 457 ^ []],start(471 ^ 0)).
% 231.05/223.75 ncf('1.1',plain,[-(452 ^ [] = 457 ^ []), 360 : 356 ^ [457 ^ [], 452 ^ []] = ordered_pair(177 ^ [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]], 178 ^ [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]]), 367 : 363 ^ [457 ^ [], 452 ^ []] = ordered_pair(177 ^ [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]], 178 ^ [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]), 375 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []), 377 : -(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []))],extension(353 ^ 1,bind([[_117197, _117199, _117541, _117543, _117805, _117807], [457 ^ [], 452 ^ [], 178 ^ [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]], 177 ^ [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]], 178 ^ [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]], 177 ^ [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]]]))).
% 231.05/223.75 ncf('1.1.1',plain,[-(356 ^ [457 ^ [], 452 ^ []] = ordered_pair(177 ^ [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]], 178 ^ [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]])), 174 : in(356 ^ [457 ^ [], 452 ^ []], 452 ^ []), 174 : relation(452 ^ [])],extension(170 ^ 4,bind([[_110812, _110960], [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.1',plain,[-(in(356 ^ [457 ^ [], 452 ^ []], 452 ^ [])), element(356 ^ [457 ^ [], 452 ^ []], 452 ^ []), -(empty(452 ^ []))],extension(389 ^ 7,bind([[_118676, _118678], [452 ^ [], 356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.1.1',plain,[-(element(356 ^ [457 ^ [], 452 ^ []], 452 ^ [])), in(356 ^ [457 ^ [], 452 ^ []], 452 ^ []), element(452 ^ [], powerset(452 ^ []))],extension(411 ^ 8,bind([[_119399, _119401, _119403], [452 ^ [], 452 ^ [], 356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.1.1.1',plain,[-(in(356 ^ [457 ^ [], 452 ^ []], 452 ^ [])), in(356 ^ [457 ^ [], 452 ^ []], 452 ^ []), 356 ^ [457 ^ [], 452 ^ []] = 356 ^ [457 ^ [], 452 ^ []], 452 ^ [] = 452 ^ []],extension(88 ^ 9,bind([[_107947, _107949, _107951, _107953], [452 ^ [], 452 ^ [], 356 ^ [457 ^ [], 452 ^ []], 356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.1.1.1.1',plain,[-(in(356 ^ [457 ^ [], 452 ^ []], 452 ^ []))],extension(358 ^ 10)).
% 231.05/223.75 ncf('1.1.1.1.1.1.2',plain,[-(356 ^ [457 ^ [], 452 ^ []] = 356 ^ [457 ^ [], 452 ^ []])],extension(2 ^ 10,bind([[_105247], [356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.1.1.1.3',plain,[-(452 ^ [] = 452 ^ [])],extension(2 ^ 10,bind([[_105247], [452 ^ []]]))).
% 231.05/223.75 ncf('1.1.1.1.1.2',plain,[-(element(452 ^ [], powerset(452 ^ []))), subset(452 ^ [], 452 ^ [])],extension(405 ^ 9,bind([[_119169, _119171], [452 ^ [], 452 ^ []]]))).
% 231.05/223.75 ncf('1.1.1.1.1.2.1',plain,[-(subset(452 ^ [], 452 ^ []))],extension(351 ^ 10,bind([[_117088, _117090], [_61511, 452 ^ []]]))).
% 231.05/223.75 ncf('1.1.1.1.2',plain,[empty(452 ^ []), empty(452 ^ []), -(452 ^ [] = 452 ^ [])],extension(443 ^ 8,bind([[_120411, _120413], [452 ^ [], 452 ^ []]]))).
% 231.05/223.75 ncf('1.1.1.1.2.1',plain,[-(empty(452 ^ []))],reduction('1.1.1.1')).
% 231.05/223.75 ncf('1.1.1.1.2.2',plain,[452 ^ [] = 452 ^ [], -(in(356 ^ [457 ^ [], 452 ^ []], 452 ^ [])), in(356 ^ [457 ^ [], 452 ^ []], 452 ^ []), 356 ^ [457 ^ [], 452 ^ []] = 356 ^ [457 ^ [], 452 ^ []]],extension(88 ^ 9,bind([[_107947, _107949, _107951, _107953], [452 ^ [], 452 ^ [], 356 ^ [457 ^ [], 452 ^ []], 356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.1.2.2.1',plain,[in(356 ^ [457 ^ [], 452 ^ []], 452 ^ [])],reduction('1.1.1')).
% 231.05/223.75 ncf('1.1.1.1.2.2.2',plain,[-(in(356 ^ [457 ^ [], 452 ^ []], 452 ^ []))],extension(358 ^ 10)).
% 231.05/223.75 ncf('1.1.1.1.2.2.3',plain,[-(356 ^ [457 ^ [], 452 ^ []] = 356 ^ [457 ^ [], 452 ^ []])],extension(2 ^ 10,bind([[_105247], [356 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.1.2',plain,[-(relation(452 ^ []))],extension(454 ^ 5)).
% 231.05/223.75 ncf('1.1.2',plain,[-(363 ^ [457 ^ [], 452 ^ []] = ordered_pair(177 ^ [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]], 178 ^ [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]])), 174 : in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []), 174 : relation(457 ^ [])],extension(170 ^ 4,bind([[_110812, _110960], [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.2.1',plain,[-(in(363 ^ [457 ^ [], 452 ^ []], 457 ^ [])), element(363 ^ [457 ^ [], 452 ^ []], 457 ^ []), -(empty(457 ^ []))],extension(389 ^ 7,bind([[_118676, _118678], [457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.2.1.1',plain,[-(element(363 ^ [457 ^ [], 452 ^ []], 457 ^ [])), in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []), element(457 ^ [], powerset(457 ^ []))],extension(411 ^ 8,bind([[_119399, _119401, _119403], [457 ^ [], 457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.2.1.1.1',plain,[-(in(363 ^ [457 ^ [], 452 ^ []], 457 ^ [])), in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []), 363 ^ [457 ^ [], 452 ^ []] = 363 ^ [457 ^ [], 452 ^ []], 457 ^ [] = 457 ^ []],extension(88 ^ 9,bind([[_107947, _107949, _107951, _107953], [457 ^ [], 457 ^ [], 363 ^ [457 ^ [], 452 ^ []], 363 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.2.1.1.1.1',plain,[-(in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []))],extension(365 ^ 10)).
% 231.05/223.75 ncf('1.1.2.1.1.1.2',plain,[-(363 ^ [457 ^ [], 452 ^ []] = 363 ^ [457 ^ [], 452 ^ []])],extension(2 ^ 10,bind([[_105247], [363 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.2.1.1.1.3',plain,[-(457 ^ [] = 457 ^ [])],extension(2 ^ 10,bind([[_105247], [457 ^ []]]))).
% 231.05/223.75 ncf('1.1.2.1.1.2',plain,[-(element(457 ^ [], powerset(457 ^ []))), subset(457 ^ [], 457 ^ [])],extension(405 ^ 9,bind([[_119169, _119171], [457 ^ [], 457 ^ []]]))).
% 231.05/223.75 ncf('1.1.2.1.1.2.1',plain,[-(subset(457 ^ [], 457 ^ []))],extension(351 ^ 10,bind([[_117088, _117090], [_66327, 457 ^ []]]))).
% 231.05/223.75 ncf('1.1.2.1.2',plain,[empty(457 ^ []), -(457 ^ [] = relation_dom(457 ^ [])), empty(relation_dom(457 ^ []))],extension(443 ^ 8,bind([[_120411, _120413], [relation_dom(457 ^ []), 457 ^ []]]))).
% 231.05/223.75 ncf('1.1.2.1.2.1',plain,[457 ^ [] = relation_dom(457 ^ []), 239 : in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []), 239 : -(in(ordered_pair(363 ^ [457 ^ [], 452 ^ []], 242 ^ [457 ^ [], 457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]), 457 ^ [])), 235 : relation(457 ^ [])],extension(231 ^ 9,bind([[_112900, _113081, _113261], [457 ^ [], 457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.2.1.2.1.1',plain,[-(in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []))],extension(365 ^ 14)).
% 231.05/223.75 ncf('1.1.2.1.2.1.2',plain,[in(ordered_pair(363 ^ [457 ^ [], 452 ^ []], 242 ^ [457 ^ [], 457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]), 457 ^ []), -(in(363 ^ [457 ^ [], 452 ^ []], 457 ^ []))],extension(246 ^ 14,bind([[_113505, _113584], [363 ^ [457 ^ [], 452 ^ []], 242 ^ [457 ^ [], 457 ^ [], 363 ^ [457 ^ [], 452 ^ []]]]]))).
% 231.05/223.75 ncf('1.1.2.1.2.1.2.1',plain,[in(363 ^ [457 ^ [], 452 ^ []], 457 ^ [])],reduction('1.1.2')).
% 231.05/223.75 ncf('1.1.2.1.2.1.3',plain,[-(relation(457 ^ []))],extension(459 ^ 10)).
% 231.05/223.75 ncf('1.1.2.1.2.2',plain,[-(empty(relation_dom(457 ^ []))), empty(457 ^ [])],extension(303 ^ 9,bind([[_115515], [457 ^ []]]))).
% 231.05/223.75 ncf('1.1.2.1.2.2.1',plain,[-(empty(457 ^ []))],reduction('1.1.2.1')).
% 231.05/223.75 ncf('1.1.2.2',plain,[-(relation(457 ^ []))],extension(459 ^ 5)).
% 231.05/223.75 ncf('1.1.3',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ [])), 203 : 369 ^ [457 ^ [], 452 ^ []] = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]), 203 : in(368 ^ [457 ^ [], 452 ^ []], relation_dom(457 ^ [])), 199 : relation(457 ^ []), 199 : function(457 ^ [])],extension(191 ^ 4,bind([[_111667, _111959, _111961], [457 ^ [], 369 ^ [457 ^ [], 452 ^ []], 368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.1',plain,[-(369 ^ [457 ^ [], 452 ^ []] = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []])), 369 ^ [457 ^ [], 452 ^ []] = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []])],extension(10 ^ 9,bind([[_105558, _105560, _105562], [apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]), apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.1.1',plain,[-(369 ^ [457 ^ [], 452 ^ []] = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])), 209 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []), 209 : in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ [])), 199 : relation(452 ^ []), 199 : function(452 ^ [])],extension(191 ^ 10,bind([[_111667, _111959, _111961], [452 ^ [], 369 ^ [457 ^ [], 452 ^ []], 368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.1.1.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ [])), in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []), ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]) = ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ [] = 452 ^ []],extension(88 ^ 15,bind([[_107947, _107949, _107951, _107953], [452 ^ [], 452 ^ [], ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []])]]))).
% 231.05/223.75 ncf('1.1.3.1.1.1.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []))],extension(373 ^ 16)).
% 231.05/223.75 ncf('1.1.3.1.1.1.2',plain,[-(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]) = ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]))],extension(2 ^ 16,bind([[_105247], [ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []])]]))).
% 231.05/223.75 ncf('1.1.3.1.1.1.3',plain,[-(452 ^ [] = 452 ^ [])],extension(2 ^ 16,bind([[_105247], [452 ^ []]]))).
% 231.05/223.75 ncf('1.1.3.1.1.2',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []), 246 : relation_dom(452 ^ []) = relation_dom(452 ^ []), 235 : relation(452 ^ [])],extension(231 ^ 13,bind([[_112900, _113081, _113505, _113584], [452 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.1.1.2.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []))],extension(373 ^ 20)).
% 231.05/223.75 ncf('1.1.3.1.1.2.2',plain,[-(relation_dom(452 ^ []) = relation_dom(452 ^ []))],extension(2 ^ 16,bind([[_105247], [relation_dom(452 ^ [])]]))).
% 231.05/223.75 ncf('1.1.3.1.1.2.3',plain,[-(relation(452 ^ []))],extension(454 ^ 14)).
% 231.05/223.75 ncf('1.1.3.1.1.3',plain,[-(relation(452 ^ []))],extension(454 ^ 11)).
% 231.05/223.75 ncf('1.1.3.1.1.4',plain,[-(function(452 ^ []))],extension(456 ^ 11)).
% 231.05/223.75 ncf('1.1.3.1.2',plain,[-(apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []])), in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))],extension(465 ^ 10,bind([[_121296], [368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.1.2.1',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []), 246 : relation_dom(452 ^ []) = relation_dom(452 ^ []), 235 : relation(452 ^ [])],extension(231 ^ 11,bind([[_112900, _113081, _113505, _113584], [452 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.1.2.1.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []))],extension(373 ^ 18)).
% 231.05/223.75 ncf('1.1.3.1.2.1.2',plain,[-(relation_dom(452 ^ []) = relation_dom(452 ^ []))],extension(2 ^ 14,bind([[_105247], [relation_dom(452 ^ [])]]))).
% 231.05/223.75 ncf('1.1.3.1.2.1.3',plain,[-(relation(452 ^ []))],extension(454 ^ 12)).
% 231.05/223.75 ncf('1.1.3.2',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(457 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 242 ^ [452 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []]]), 452 ^ []), 246 : relation_dom(457 ^ []) = relation_dom(452 ^ []), 235 : relation(452 ^ [])],extension(231 ^ 7,bind([[_112900, _113081, _113505, _113584], [452 ^ [], relation_dom(457 ^ []), 368 ^ [457 ^ [], 452 ^ []], 242 ^ [452 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []]]]]))).
% 231.05/223.75 ncf('1.1.3.2.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 242 ^ [452 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []]]), 452 ^ [])), 239 : in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ [])), 239 : relation_dom(452 ^ []) = relation_dom(452 ^ [])],extension(235 ^ 14,bind([[_113081, _113261], [relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.2.1.1',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ [])],extension(246 ^ 17,bind([[_113505, _113584], [368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.3.2.1.1.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ []))],extension(373 ^ 20)).
% 231.05/223.75 ncf('1.1.3.2.1.2',plain,[-(relation_dom(452 ^ []) = relation_dom(452 ^ [])), 452 ^ [] = 452 ^ []],extension(134 ^ 15,bind([[_109535, _109537], [452 ^ [], 452 ^ []]]))).
% 231.05/223.75 ncf('1.1.3.2.1.2.1',plain,[-(452 ^ [] = 452 ^ [])],extension(2 ^ 16,bind([[_105247], [452 ^ []]]))).
% 231.05/223.75 ncf('1.1.3.2.2',plain,[-(relation_dom(457 ^ []) = relation_dom(452 ^ [])), relation_dom(452 ^ []) = relation_dom(457 ^ [])],extension(4 ^ 10,bind([[_105354, _105356], [relation_dom(457 ^ []), relation_dom(452 ^ [])]]))).
% 231.05/223.75 ncf('1.1.3.2.2.1',plain,[-(relation_dom(452 ^ []) = relation_dom(457 ^ []))],extension(463 ^ 11)).
% 231.05/223.75 ncf('1.1.3.2.3',plain,[-(relation(452 ^ []))],extension(454 ^ 8)).
% 231.05/223.75 ncf('1.1.3.3',plain,[-(relation(457 ^ []))],extension(459 ^ 5)).
% 231.05/223.75 ncf('1.1.3.4',plain,[-(function(457 ^ []))],extension(461 ^ 5)).
% 231.05/223.75 ncf('1.1.4',plain,[in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []), 209 : -(369 ^ [457 ^ [], 452 ^ []] = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []])), 209 : in(368 ^ [457 ^ [], 452 ^ []], relation_dom(457 ^ [])), 199 : relation(457 ^ []), 199 : function(457 ^ [])],extension(191 ^ 4,bind([[_111667, _111959, _111961], [457 ^ [], 369 ^ [457 ^ [], 452 ^ []], 368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1',plain,[369 ^ [457 ^ [], 452 ^ []] = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]), -(369 ^ [457 ^ [], 452 ^ []] = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])), apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])],extension(10 ^ 9,bind([[_105558, _105560, _105562], [apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]), 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.1',plain,[369 ^ [457 ^ [], 452 ^ []] = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), -(369 ^ [457 ^ [], 452 ^ []] = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])), apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])],extension(10 ^ 10,bind([[_105558, _105560, _105562], [apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.1.1',plain,[369 ^ [457 ^ [], 452 ^ []] = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]), 203 : -(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ [])), 203 : in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ [])), 199 : relation(452 ^ []), 199 : function(452 ^ [])],extension(191 ^ 11,bind([[_111667, _111959, _111961], [452 ^ [], 369 ^ [457 ^ [], 452 ^ []], 368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.1.1.1',plain,[in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 452 ^ [])],extension(379 ^ 16)).
% 231.05/223.75 ncf('1.1.4.1.1.1.2',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []), 246 : relation_dom(452 ^ []) = relation_dom(457 ^ []), 235 : relation(457 ^ [])],extension(231 ^ 14,bind([[_112900, _113081, _113505, _113584], [457 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.1.1.2.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []))],reduction('1.1')).
% 231.05/223.75 ncf('1.1.4.1.1.1.2.2',plain,[-(relation_dom(452 ^ []) = relation_dom(457 ^ []))],extension(463 ^ 17)).
% 231.05/223.75 ncf('1.1.4.1.1.1.2.3',plain,[-(relation(457 ^ []))],extension(459 ^ 15)).
% 231.05/223.75 ncf('1.1.4.1.1.1.3',plain,[-(relation(452 ^ []))],extension(454 ^ 12)).
% 231.05/223.75 ncf('1.1.4.1.1.1.4',plain,[-(function(452 ^ []))],extension(456 ^ 12)).
% 231.05/223.75 ncf('1.1.4.1.1.2',plain,[-(apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])), 452 ^ [] = 452 ^ [], 368 ^ [457 ^ [], 452 ^ []] = 368 ^ [457 ^ [], 452 ^ []]],extension(140 ^ 11,bind([[_109761, _109763, _109765, _109767], [368 ^ [457 ^ [], 452 ^ []], 368 ^ [457 ^ [], 452 ^ []], 452 ^ [], 452 ^ []]]))).
% 231.05/223.75 ncf('1.1.4.1.1.2.1',plain,[-(452 ^ [] = 452 ^ [])],extension(2 ^ 12,bind([[_105247], [452 ^ []]]))).
% 231.05/223.75 ncf('1.1.4.1.1.2.2',plain,[-(368 ^ [457 ^ [], 452 ^ []] = 368 ^ [457 ^ [], 452 ^ []])],extension(2 ^ 12,bind([[_105247], [368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.2',plain,[-(apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])), apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []])],extension(4 ^ 10,bind([[_105354, _105356], [apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []]), apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []])]]))).
% 231.05/223.75 ncf('1.1.4.1.2.1',plain,[-(apply(452 ^ [], 368 ^ [457 ^ [], 452 ^ []]) = apply(457 ^ [], 368 ^ [457 ^ [], 452 ^ []])), in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))],extension(465 ^ 11,bind([[_121296], [368 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.2.1.1',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(452 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []), 246 : relation_dom(452 ^ []) = relation_dom(457 ^ []), 235 : relation(457 ^ [])],extension(231 ^ 12,bind([[_112900, _113081, _113505, _113584], [457 ^ [], relation_dom(452 ^ []), 368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.1.2.1.1.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []))],reduction('1.1')).
% 231.05/223.75 ncf('1.1.4.1.2.1.1.2',plain,[-(relation_dom(452 ^ []) = relation_dom(457 ^ []))],extension(463 ^ 15)).
% 231.05/223.75 ncf('1.1.4.1.2.1.1.3',plain,[-(relation(457 ^ []))],extension(459 ^ 13)).
% 231.05/223.75 ncf('1.1.4.2',plain,[-(in(368 ^ [457 ^ [], 452 ^ []], relation_dom(457 ^ []))), 248 : in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []), 246 : relation_dom(457 ^ []) = relation_dom(457 ^ []), 235 : relation(457 ^ [])],extension(231 ^ 7,bind([[_112900, _113081, _113505, _113584], [457 ^ [], relation_dom(457 ^ []), 368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]]]))).
% 231.05/223.75 ncf('1.1.4.2.1',plain,[-(in(ordered_pair(368 ^ [457 ^ [], 452 ^ []], 369 ^ [457 ^ [], 452 ^ []]), 457 ^ []))],reduction('1.1')).
% 231.05/223.75 ncf('1.1.4.2.2',plain,[-(relation_dom(457 ^ []) = relation_dom(457 ^ [])), 457 ^ [] = 457 ^ []],extension(134 ^ 10,bind([[_109535, _109537], [457 ^ [], 457 ^ []]]))).
% 231.05/223.75 ncf('1.1.4.2.2.1',plain,[-(457 ^ [] = 457 ^ [])],extension(2 ^ 11,bind([[_105247], [457 ^ []]]))).
% 231.05/223.75 ncf('1.1.4.2.3',plain,[-(relation(457 ^ []))],extension(459 ^ 8)).
% 231.05/223.75 ncf('1.1.4.3',plain,[-(relation(457 ^ []))],extension(459 ^ 5)).
% 231.05/223.75 ncf('1.1.4.4',plain,[-(function(457 ^ []))],extension(461 ^ 5)).
% 231.05/223.75 %-----------------------------------------------------
% 231.05/223.75 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------