%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU269+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:57 EDT 2023
% Result : Theorem 11.76s 11.73s
% Output : Proof 11.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU269+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 12:27:00 EDT 2023
% 0.13/0.34 % CPUTime :
% 11.76/11.73
% 11.76/11.73 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 11.76/11.73 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.76/11.73 %-----------------------------------------------------
% 11.76/11.73 ncf(matrix, plain, [(668 ^ _95221) ^ [] : [transitive(inclusion_relation(666 ^ []))], (166 ^ _95221) ^ [_100458, _100460, _100462, _100464] : [-(unordered_pair(_100464, _100460) = unordered_pair(_100462, _100458)), _100464 = _100462, _100460 = _100458], (176 ^ _95221) ^ [_100789, _100791] : [_100791 = _100789, -(singleton(_100791) = singleton(_100789))], (182 ^ _95221) ^ [_101007, _101009] : [_101009 = _101007, -(relation_field(_101009) = relation_field(_101007))], (188 ^ _95221) ^ [_101225, _101227] : [_101227 = _101225, -(relation_dom(_101227) = relation_dom(_101225))], (194 ^ _95221) ^ [_101443, _101445] : [_101445 = _101443, -(relation_rng(_101445) = relation_rng(_101443))], (200 ^ _95221) ^ [_101689, _101691, _101693, _101695] : [-(ordered_pair(_101695, _101691) = ordered_pair(_101693, _101689)), _101695 = _101693, _101691 = _101689], (210 ^ _95221) ^ [_102048, _102050, _102052, _102054] : [-(set_union2(_102054, _102050) = set_union2(_102052, _102048)), _102054 = _102052, _102050 = _102048], (220 ^ _95221) ^ [_102379, _102381] : [_102381 = _102379, -(powerset(_102381) = powerset(_102379))], (226 ^ _95221) ^ [_102577, _102579] : [_102579 = _102577, -(inclusion_relation(_102579) = inclusion_relation(_102577))], (2 ^ _95221) ^ [_95365] : [-(_95365 = _95365)], (4 ^ _95221) ^ [_95472, _95474] : [_95474 = _95472, -(_95472 = _95474)], (10 ^ _95221) ^ [_95676, _95678, _95680] : [-(_95680 = _95676), _95680 = _95678, _95678 = _95676], (20 ^ _95221) ^ [_96017, _96019, _96021, _96023] : [-(is_transitive_in(_96021, _96017)), is_transitive_in(_96023, _96019), _96023 = _96021, _96019 = _96017], (34 ^ _95221) ^ [_96433, _96435] : [-(one_to_one(_96433)), _96435 = _96433, one_to_one(_96435)], (44 ^ _95221) ^ [_96728, _96730] : [-(epsilon_transitive(_96728)), _96730 = _96728, epsilon_transitive(_96730)], (54 ^ _95221) ^ [_97023, _97025] : [-(epsilon_connected(_97023)), _97025 = _97023, epsilon_connected(_97025)], (64 ^ _95221) ^ [_97318, _97320] : [-(ordinal(_97318)), _97320 = _97318, ordinal(_97320)], (74 ^ _95221) ^ [_97613, _97615] : [-(relation(_97613)), _97615 = _97613, relation(_97615)], (84 ^ _95221) ^ [_97908, _97910] : [-(relation_empty_yielding(_97908)), _97910 = _97908, relation_empty_yielding(_97910)], (94 ^ _95221) ^ [_98203, _98205] : [-(function(_98203)), _98205 = _98203, function(_98205)], (104 ^ _95221) ^ [_98526, _98528, _98530, _98532] : [-(subset(_98530, _98526)), subset(_98532, _98528), _98532 = _98530, _98528 = _98526], (118 ^ _95221) ^ [_98970, _98972, _98974, _98976] : [-(element(_98974, _98970)), element(_98976, _98972), _98976 = _98974, _98972 = _98970], (132 ^ _95221) ^ [_99414, _99416, _99418, _99420] : [-(in(_99418, _99414)), in(_99420, _99416), _99420 = _99418, _99416 = _99414], (146 ^ _95221) ^ [_99830, _99832] : [-(empty(_99830)), _99832 = _99830, empty(_99832)], (156 ^ _95221) ^ [_100105, _100107] : [-(transitive(_100105)), _100107 = _100105, transitive(_100107)], (232 ^ _95221) ^ [_102861, _102863] : [in(_102863, _102861), in(_102861, _102863)], (238 ^ _95221) ^ [_103058] : [empty(_103058), -(function(_103058))], (244 ^ _95221) ^ [_103244] : [ordinal(_103244), 247 ^ _95221 : [(248 ^ _95221) ^ [] : [-(epsilon_transitive(_103244))], (250 ^ _95221) ^ [] : [-(epsilon_connected(_103244))]]], (252 ^ _95221) ^ [_103501] : [263 ^ _95221 : [(264 ^ _95221) ^ [] : [-(relation(_103501))], (266 ^ _95221) ^ [] : [-(function(_103501))], (268 ^ _95221) ^ [] : [-(one_to_one(_103501))]], relation(_103501), empty(_103501), function(_103501)], (270 ^ _95221) ^ [_103994] : [-(ordinal(_103994)), epsilon_transitive(_103994), epsilon_connected(_103994)], (280 ^ _95221) ^ [_104263] : [empty(_104263), 283 ^ _95221 : [(284 ^ _95221) ^ [] : [-(epsilon_transitive(_104263))], (286 ^ _95221) ^ [] : [-(epsilon_connected(_104263))], (288 ^ _95221) ^ [] : [-(ordinal(_104263))]]], (290 ^ _95221) ^ [_104589, _104591] : [-(unordered_pair(_104591, _104589) = unordered_pair(_104589, _104591))], (292 ^ _95221) ^ [_104689, _104691] : [-(set_union2(_104691, _104689) = set_union2(_104689, _104691))], (294 ^ _95221) ^ [_104790] : [relation(_104790), 297 ^ _95221 : [(298 ^ _95221) ^ [] : [transitive(_104790), -(is_transitive_in(_104790, relation_field(_104790)))], (304 ^ _95221) ^ [] : [is_transitive_in(_104790, relation_field(_104790)), -(transitive(_104790))]]], (310 ^ _95221) ^ [_105235, _105237] : [relation(_105235), 313 ^ _95221 : [(340 ^ _95221) ^ [] : [-(_105235 = inclusion_relation(_105237)), relation_field(_105235) = _105237, 347 ^ _95221 : [(348 ^ _95221) ^ [] : [-(in(345 ^ [_105235, _105237], _105237))], (350 ^ _95221) ^ [] : [-(in(346 ^ [_105235, _105237], _105237))], (352 ^ _95221) ^ [] : [353 ^ _95221 : [(354 ^ _95221) ^ [] : [-(in(ordered_pair(345 ^ [_105235, _105237], 346 ^ [_105235, _105237]), _105235))], (356 ^ _95221) ^ [] : [subset(345 ^ [_105235, _105237], 346 ^ [_105235, _105237])]], 357 ^ _95221 : [(358 ^ _95221) ^ [] : [-(subset(345 ^ [_105235, _105237], 346 ^ [_105235, _105237]))], (360 ^ _95221) ^ [] : [in(ordered_pair(345 ^ [_105235, _105237], 346 ^ [_105235, _105237]), _105235)]]]]], (314 ^ _95221) ^ [] : [_105235 = inclusion_relation(_105237), 317 ^ _95221 : [(318 ^ _95221) ^ [] : [-(relation_field(_105235) = _105237)], (320 ^ _95221) ^ [_105598, _105600] : [in(_105600, _105237), in(_105598, _105237), 327 ^ _95221 : [(328 ^ _95221) ^ [] : [in(ordered_pair(_105600, _105598), _105235), -(subset(_105600, _105598))], (334 ^ _95221) ^ [] : [subset(_105600, _105598), -(in(ordered_pair(_105600, _105598), _105235))]]]]]]], (364 ^ _95221) ^ [_107020, _107022] : [-(ordered_pair(_107022, _107020) = unordered_pair(unordered_pair(_107022, _107020), singleton(_107022)))], (366 ^ _95221) ^ [_107126] : [relation(_107126), -(relation_field(_107126) = set_union2(relation_dom(_107126), relation_rng(_107126)))], (372 ^ _95221) ^ [_107332] : [relation(_107332), 375 ^ _95221 : [(402 ^ _95221) ^ [_108367] : [406 ^ _95221 : [(407 ^ _95221) ^ [] : [-(in(403 ^ [_107332, _108367], _108367))], (409 ^ _95221) ^ [] : [-(in(404 ^ [_107332, _108367], _108367))], (411 ^ _95221) ^ [] : [-(in(405 ^ [_107332, _108367], _108367))], (413 ^ _95221) ^ [] : [-(in(ordered_pair(403 ^ [_107332, _108367], 404 ^ [_107332, _108367]), _107332))], (415 ^ _95221) ^ [] : [-(in(ordered_pair(404 ^ [_107332, _108367], 405 ^ [_107332, _108367]), _107332))], (417 ^ _95221) ^ [] : [in(ordered_pair(403 ^ [_107332, _108367], 405 ^ [_107332, _108367]), _107332)]], -(is_transitive_in(_107332, _108367))], (376 ^ _95221) ^ [_107546] : [is_transitive_in(_107332, _107546), 379 ^ _95221 : [(380 ^ _95221) ^ [_107756, _107758, _107760] : [-(in(ordered_pair(_107760, _107756), _107332)), in(_107760, _107546), in(_107758, _107546), in(_107756, _107546), in(ordered_pair(_107760, _107758), _107332), in(ordered_pair(_107758, _107756), _107332)]]]]], (421 ^ _95221) ^ [] : [true___, -(true___)], (427 ^ _95221) ^ [] : [true___, -(true___)], (433 ^ _95221) ^ [_109600] : [-(relation(inclusion_relation(_109600)))], (435 ^ _95221) ^ [] : [true___, -(true___)], (441 ^ _95221) ^ [] : [true___, -(true___)], (447 ^ _95221) ^ [] : [true___, -(true___)], (453 ^ _95221) ^ [] : [true___, -(true___)], (459 ^ _95221) ^ [] : [true___, -(true___)], (465 ^ _95221) ^ [] : [true___, -(true___)], (471 ^ _95221) ^ [] : [true___, -(true___)], (477 ^ _95221) ^ [] : [true___, -(true___)], (484 ^ _95221) ^ [_110670] : [-(element(482 ^ [_110670], _110670))], (486 ^ _95221) ^ [] : [-(empty(empty_set))], (488 ^ _95221) ^ [_110819, _110821] : [empty(ordered_pair(_110821, _110819))], (490 ^ _95221) ^ [] : [-(relation(empty_set))], (492 ^ _95221) ^ [] : [-(relation_empty_yielding(empty_set))], (494 ^ _95221) ^ [] : [-(function(empty_set))], (496 ^ _95221) ^ [] : [-(one_to_one(empty_set))], (498 ^ _95221) ^ [] : [-(empty(empty_set))], (500 ^ _95221) ^ [] : [-(epsilon_transitive(empty_set))], (502 ^ _95221) ^ [] : [-(epsilon_connected(empty_set))], (504 ^ _95221) ^ [] : [-(ordinal(empty_set))], (506 ^ _95221) ^ [_111368, _111370] : [-(empty(_111370)), empty(set_union2(_111370, _111368))], (512 ^ _95221) ^ [_111584, _111586] : [-(empty(_111586)), empty(set_union2(_111584, _111586))], (518 ^ _95221) ^ [_111785, _111787] : [-(set_union2(_111787, _111787) = _111787)], (521 ^ _95221) ^ [] : [-(relation(519 ^ []))], (523 ^ _95221) ^ [] : [-(function(519 ^ []))], (526 ^ _95221) ^ [] : [-(epsilon_transitive(524 ^ []))], (528 ^ _95221) ^ [] : [-(epsilon_connected(524 ^ []))], (530 ^ _95221) ^ [] : [-(ordinal(524 ^ []))], (533 ^ _95221) ^ [] : [-(empty(531 ^ []))], (536 ^ _95221) ^ [] : [-(relation(534 ^ []))], (538 ^ _95221) ^ [] : [-(empty(534 ^ []))], (540 ^ _95221) ^ [] : [-(function(534 ^ []))], (543 ^ _95221) ^ [] : [-(relation(541 ^ []))], (545 ^ _95221) ^ [] : [-(function(541 ^ []))], (547 ^ _95221) ^ [] : [-(one_to_one(541 ^ []))], (549 ^ _95221) ^ [] : [-(empty(541 ^ []))], (551 ^ _95221) ^ [] : [-(epsilon_transitive(541 ^ []))], (553 ^ _95221) ^ [] : [-(epsilon_connected(541 ^ []))], (555 ^ _95221) ^ [] : [-(ordinal(541 ^ []))], (558 ^ _95221) ^ [] : [empty(556 ^ [])], (561 ^ _95221) ^ [] : [-(relation(559 ^ []))], (563 ^ _95221) ^ [] : [-(function(559 ^ []))], (565 ^ _95221) ^ [] : [-(one_to_one(559 ^ []))], (568 ^ _95221) ^ [] : [empty(566 ^ [])], (570 ^ _95221) ^ [] : [-(epsilon_transitive(566 ^ []))], (572 ^ _95221) ^ [] : [-(epsilon_connected(566 ^ []))], (574 ^ _95221) ^ [] : [-(ordinal(566 ^ []))], (577 ^ _95221) ^ [] : [-(relation(575 ^ []))], (579 ^ _95221) ^ [] : [-(relation_empty_yielding(575 ^ []))], (581 ^ _95221) ^ [] : [-(function(575 ^ []))], (583 ^ _95221) ^ [_113765, _113767] : [-(subset(_113767, _113767))], (585 ^ _95221) ^ [_113845] : [-(set_union2(_113845, empty_set) = _113845)], (587 ^ _95221) ^ [_113955, _113957] : [in(_113957, _113955), -(element(_113957, _113955))], (593 ^ _95221) ^ [_114179, _114181, _114183] : [-(subset(_114183, _114179)), subset(_114183, _114181), subset(_114181, _114179)], (603 ^ _95221) ^ [_114488, _114490] : [element(_114490, _114488), -(empty(_114488)), -(in(_114490, _114488))], (613 ^ _95221) ^ [_114815, _114817] : [element(_114817, powerset(_114815)), -(subset(_114817, _114815))], (619 ^ _95221) ^ [_114981, _114983] : [subset(_114983, _114981), -(element(_114983, powerset(_114981)))], (625 ^ _95221) ^ [_115211, _115213, _115215] : [-(element(_115215, _115211)), in(_115215, _115213), element(_115213, powerset(_115211))], (635 ^ _95221) ^ [_115538, _115540, _115542] : [in(_115542, _115540), element(_115540, powerset(_115538)), empty(_115538)], (645 ^ _95221) ^ [_115834] : [empty(_115834), -(_115834 = empty_set)], (651 ^ _95221) ^ [_116036, _116038] : [in(_116038, _116036), empty(_116036)], (657 ^ _95221) ^ [_116223, _116225] : [empty(_116225), -(_116225 = _116223), empty(_116223)]], input).
% 11.76/11.73 ncf('1',plain,[transitive(inclusion_relation(666 ^ []))],start(668 ^ 0)).
% 11.76/11.73 ncf('1.1',plain,[-(transitive(inclusion_relation(666 ^ []))), 304 : is_transitive_in(inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))), 304 : relation(inclusion_relation(666 ^ []))],extension(294 ^ 1,bind([[_104790], [inclusion_relation(666 ^ [])]]))).
% 11.76/11.73 ncf('1.1.1',plain,[-(is_transitive_in(inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ [])))), 413 : -(in(ordered_pair(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), inclusion_relation(666 ^ []))), 402 : relation(inclusion_relation(666 ^ []))],extension(372 ^ 4,bind([[_107332, _108367], [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]))).
% 11.76/11.73 ncf('1.1.1.1',plain,[in(ordered_pair(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), inclusion_relation(666 ^ [])), 328 : -(subset(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])), 328 : in(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))), 328 : in(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))), 320 : inclusion_relation(666 ^ []) = inclusion_relation(relation_field(inclusion_relation(666 ^ []))), 314 : relation(inclusion_relation(666 ^ []))],extension(310 ^ 9,bind([[_105235, _105237, _105598, _105600], [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ [])), 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1',plain,[subset(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), -(subset(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])), subset(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])],extension(593 ^ 16,bind([[_114179, _114181, _114183], [405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1.1',plain,[subset(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), -(subset(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])), 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))] = 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))] = 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]],extension(104 ^ 17,bind([[_98526, _98528, _98530, _98532], [405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1.1.1',plain,[subset(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), 334 : -(in(ordered_pair(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), inclusion_relation(666 ^ []))), 334 : in(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))), 334 : in(405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ [])))],extension(320 ^ 18,bind([[_105598, _105600], [405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1.1.1.1',plain,[in(ordered_pair(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), inclusion_relation(666 ^ []))],extension(417 ^ 21)).
% 11.76/11.73 ncf('1.1.1.1.1.1.1.2',plain,[-(in(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))))],extension(407 ^ 19)).
% 11.76/11.73 ncf('1.1.1.1.1.1.1.3',plain,[-(in(405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))))],extension(411 ^ 19)).
% 11.76/11.73 ncf('1.1.1.1.1.1.2',plain,[-(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))] = 403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])],extension(2 ^ 18,bind([[_95365], [403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1.1.3',plain,[-(405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))] = 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])],extension(2 ^ 18,bind([[_95365], [405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1.2',plain,[-(subset(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))])), 328 : in(ordered_pair(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), inclusion_relation(666 ^ [])), 328 : in(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))), 328 : in(405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ [])))],extension(320 ^ 17,bind([[_105598, _105600], [405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]]]))).
% 11.76/11.73 ncf('1.1.1.1.1.2.1',plain,[-(in(ordered_pair(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], 405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))]), inclusion_relation(666 ^ [])))],extension(415 ^ 20)).
% 11.76/11.73 ncf('1.1.1.1.1.2.2',plain,[-(in(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))))],extension(409 ^ 18)).
% 11.76/11.73 ncf('1.1.1.1.1.2.3',plain,[-(in(405 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))))],extension(411 ^ 18)).
% 11.76/11.73 ncf('1.1.1.1.2',plain,[-(in(403 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))))],extension(407 ^ 14)).
% 11.76/11.73 ncf('1.1.1.1.3',plain,[-(in(404 ^ [inclusion_relation(666 ^ []), relation_field(inclusion_relation(666 ^ []))], relation_field(inclusion_relation(666 ^ []))))],extension(409 ^ 14)).
% 11.76/11.73 ncf('1.1.1.1.4',plain,[-(inclusion_relation(666 ^ []) = inclusion_relation(relation_field(inclusion_relation(666 ^ [])))), 666 ^ [] = relation_field(inclusion_relation(666 ^ []))],extension(226 ^ 12,bind([[_102577, _102579], [relation_field(inclusion_relation(666 ^ [])), 666 ^ []]]))).
% 11.76/11.73 ncf('1.1.1.1.4.1',plain,[-(666 ^ [] = relation_field(inclusion_relation(666 ^ []))), relation_field(inclusion_relation(666 ^ [])) = 666 ^ []],extension(4 ^ 13,bind([[_95472, _95474], [666 ^ [], relation_field(inclusion_relation(666 ^ []))]]))).
% 11.76/11.73 ncf('1.1.1.1.4.1.1',plain,[-(relation_field(inclusion_relation(666 ^ [])) = 666 ^ []), 314 : inclusion_relation(666 ^ []) = inclusion_relation(666 ^ []), 314 : relation(inclusion_relation(666 ^ []))],extension(310 ^ 14,bind([[_105235, _105237], [inclusion_relation(666 ^ []), 666 ^ []]]))).
% 11.76/11.73 ncf('1.1.1.1.4.1.1.1',plain,[-(inclusion_relation(666 ^ []) = inclusion_relation(666 ^ []))],extension(2 ^ 17,bind([[_95365], [inclusion_relation(666 ^ [])]]))).
% 11.76/11.73 ncf('1.1.1.1.4.1.1.2',plain,[-(relation(inclusion_relation(666 ^ [])))],extension(433 ^ 15,bind([[_109600], [666 ^ []]]))).
% 11.76/11.73 ncf('1.1.1.1.5',plain,[-(relation(inclusion_relation(666 ^ [])))],extension(433 ^ 10,bind([[_109600], [666 ^ []]]))).
% 11.76/11.73 ncf('1.1.1.2',plain,[-(relation(inclusion_relation(666 ^ [])))],extension(433 ^ 5,bind([[_109600], [666 ^ []]]))).
% 11.76/11.73 ncf('1.1.2',plain,[-(relation(inclusion_relation(666 ^ [])))],extension(433 ^ 2,bind([[_109600], [666 ^ []]]))).
% 11.76/11.73 %-----------------------------------------------------
% 11.76/11.73 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------