%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU268+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:56 EDT 2023
% Result : Theorem 4.94s 5.51s
% Output : Proof 4.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU268+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n003.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:50:15 EDT 2023
% 0.12/0.33 % CPUTime :
% 4.94/5.51
% 4.94/5.51 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 4.94/5.51 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.94/5.51 %-----------------------------------------------------
% 4.94/5.51 ncf(matrix, plain, [(632 ^ _87308) ^ [] : [reflexive(inclusion_relation(630 ^ []))], (166 ^ _87308) ^ [_92545, _92547, _92549, _92551] : [-(unordered_pair(_92551, _92547) = unordered_pair(_92549, _92545)), _92551 = _92549, _92547 = _92545], (176 ^ _87308) ^ [_92876, _92878] : [_92878 = _92876, -(singleton(_92878) = singleton(_92876))], (182 ^ _87308) ^ [_93094, _93096] : [_93096 = _93094, -(relation_dom(_93096) = relation_dom(_93094))], (188 ^ _87308) ^ [_93312, _93314] : [_93314 = _93312, -(relation_rng(_93314) = relation_rng(_93312))], (194 ^ _87308) ^ [_93530, _93532] : [_93532 = _93530, -(relation_field(_93532) = relation_field(_93530))], (200 ^ _87308) ^ [_93776, _93778, _93780, _93782] : [-(ordered_pair(_93782, _93778) = ordered_pair(_93780, _93776)), _93782 = _93780, _93778 = _93776], (210 ^ _87308) ^ [_94135, _94137, _94139, _94141] : [-(set_union2(_94141, _94137) = set_union2(_94139, _94135)), _94141 = _94139, _94137 = _94135], (220 ^ _87308) ^ [_94466, _94468] : [_94468 = _94466, -(powerset(_94468) = powerset(_94466))], (226 ^ _87308) ^ [_94664, _94666] : [_94666 = _94664, -(inclusion_relation(_94666) = inclusion_relation(_94664))], (2 ^ _87308) ^ [_87452] : [-(_87452 = _87452)], (4 ^ _87308) ^ [_87559, _87561] : [_87561 = _87559, -(_87559 = _87561)], (10 ^ _87308) ^ [_87763, _87765, _87767] : [-(_87767 = _87763), _87767 = _87765, _87765 = _87763], (20 ^ _87308) ^ [_88104, _88106, _88108, _88110] : [-(is_reflexive_in(_88108, _88104)), is_reflexive_in(_88110, _88106), _88110 = _88108, _88106 = _88104], (34 ^ _87308) ^ [_88520, _88522] : [-(one_to_one(_88520)), _88522 = _88520, one_to_one(_88522)], (44 ^ _87308) ^ [_88815, _88817] : [-(epsilon_transitive(_88815)), _88817 = _88815, epsilon_transitive(_88817)], (54 ^ _87308) ^ [_89110, _89112] : [-(epsilon_connected(_89110)), _89112 = _89110, epsilon_connected(_89112)], (64 ^ _87308) ^ [_89405, _89407] : [-(ordinal(_89405)), _89407 = _89405, ordinal(_89407)], (74 ^ _87308) ^ [_89700, _89702] : [-(relation(_89700)), _89702 = _89700, relation(_89702)], (84 ^ _87308) ^ [_89995, _89997] : [-(relation_empty_yielding(_89995)), _89997 = _89995, relation_empty_yielding(_89997)], (94 ^ _87308) ^ [_90290, _90292] : [-(function(_90290)), _90292 = _90290, function(_90292)], (104 ^ _87308) ^ [_90613, _90615, _90617, _90619] : [-(subset(_90617, _90613)), subset(_90619, _90615), _90619 = _90617, _90615 = _90613], (118 ^ _87308) ^ [_91057, _91059, _91061, _91063] : [-(element(_91061, _91057)), element(_91063, _91059), _91063 = _91061, _91059 = _91057], (132 ^ _87308) ^ [_91501, _91503, _91505, _91507] : [-(in(_91505, _91501)), in(_91507, _91503), _91507 = _91505, _91503 = _91501], (146 ^ _87308) ^ [_91917, _91919] : [-(empty(_91917)), _91919 = _91917, empty(_91919)], (156 ^ _87308) ^ [_92192, _92194] : [-(reflexive(_92192)), _92194 = _92192, reflexive(_92194)], (232 ^ _87308) ^ [_94948, _94950] : [in(_94950, _94948), in(_94948, _94950)], (238 ^ _87308) ^ [_95145] : [empty(_95145), -(function(_95145))], (244 ^ _87308) ^ [_95331] : [ordinal(_95331), 247 ^ _87308 : [(248 ^ _87308) ^ [] : [-(epsilon_transitive(_95331))], (250 ^ _87308) ^ [] : [-(epsilon_connected(_95331))]]], (252 ^ _87308) ^ [_95588] : [263 ^ _87308 : [(264 ^ _87308) ^ [] : [-(relation(_95588))], (266 ^ _87308) ^ [] : [-(function(_95588))], (268 ^ _87308) ^ [] : [-(one_to_one(_95588))]], relation(_95588), empty(_95588), function(_95588)], (270 ^ _87308) ^ [_96081] : [-(ordinal(_96081)), epsilon_transitive(_96081), epsilon_connected(_96081)], (280 ^ _87308) ^ [_96350] : [empty(_96350), 283 ^ _87308 : [(284 ^ _87308) ^ [] : [-(epsilon_transitive(_96350))], (286 ^ _87308) ^ [] : [-(epsilon_connected(_96350))], (288 ^ _87308) ^ [] : [-(ordinal(_96350))]]], (290 ^ _87308) ^ [_96676, _96678] : [-(unordered_pair(_96678, _96676) = unordered_pair(_96676, _96678))], (292 ^ _87308) ^ [_96776, _96778] : [-(set_union2(_96778, _96776) = set_union2(_96776, _96778))], (294 ^ _87308) ^ [_96877] : [relation(_96877), 297 ^ _87308 : [(308 ^ _87308) ^ [_97376] : [310 ^ _87308 : [(311 ^ _87308) ^ [] : [-(in(309 ^ [_96877, _97376], _97376))], (313 ^ _87308) ^ [] : [in(ordered_pair(309 ^ [_96877, _97376], 309 ^ [_96877, _97376]), _96877)]], -(is_reflexive_in(_96877, _97376))], (298 ^ _87308) ^ [_97051] : [is_reflexive_in(_96877, _97051), 301 ^ _87308 : [(302 ^ _87308) ^ [_97193] : [in(_97193, _97051), -(in(ordered_pair(_97193, _97193), _96877))]]]]], (317 ^ _87308) ^ [_97756, _97758] : [relation(_97756), 320 ^ _87308 : [(347 ^ _87308) ^ [] : [-(_97756 = inclusion_relation(_97758)), relation_field(_97756) = _97758, 354 ^ _87308 : [(355 ^ _87308) ^ [] : [-(in(352 ^ [_97756, _97758], _97758))], (357 ^ _87308) ^ [] : [-(in(353 ^ [_97756, _97758], _97758))], (359 ^ _87308) ^ [] : [360 ^ _87308 : [(361 ^ _87308) ^ [] : [-(in(ordered_pair(352 ^ [_97756, _97758], 353 ^ [_97756, _97758]), _97756))], (363 ^ _87308) ^ [] : [subset(352 ^ [_97756, _97758], 353 ^ [_97756, _97758])]], 364 ^ _87308 : [(365 ^ _87308) ^ [] : [-(subset(352 ^ [_97756, _97758], 353 ^ [_97756, _97758]))], (367 ^ _87308) ^ [] : [in(ordered_pair(352 ^ [_97756, _97758], 353 ^ [_97756, _97758]), _97756)]]]]], (321 ^ _87308) ^ [] : [_97756 = inclusion_relation(_97758), 324 ^ _87308 : [(325 ^ _87308) ^ [] : [-(relation_field(_97756) = _97758)], (327 ^ _87308) ^ [_98119, _98121] : [in(_98121, _97758), in(_98119, _97758), 334 ^ _87308 : [(335 ^ _87308) ^ [] : [in(ordered_pair(_98121, _98119), _97756), -(subset(_98121, _98119))], (341 ^ _87308) ^ [] : [subset(_98121, _98119), -(in(ordered_pair(_98121, _98119), _97756))]]]]]]], (371 ^ _87308) ^ [_99541, _99543] : [-(ordered_pair(_99543, _99541) = unordered_pair(unordered_pair(_99543, _99541), singleton(_99543)))], (373 ^ _87308) ^ [_99647] : [relation(_99647), -(relation_field(_99647) = set_union2(relation_dom(_99647), relation_rng(_99647)))], (379 ^ _87308) ^ [_99853] : [relation(_99853), 382 ^ _87308 : [(383 ^ _87308) ^ [] : [reflexive(_99853), -(is_reflexive_in(_99853, relation_field(_99853)))], (389 ^ _87308) ^ [] : [is_reflexive_in(_99853, relation_field(_99853)), -(reflexive(_99853))]]], (395 ^ _87308) ^ [] : [true___, -(true___)], (401 ^ _87308) ^ [] : [true___, -(true___)], (407 ^ _87308) ^ [_100507] : [-(relation(inclusion_relation(_100507)))], (409 ^ _87308) ^ [] : [true___, -(true___)], (415 ^ _87308) ^ [] : [true___, -(true___)], (421 ^ _87308) ^ [] : [true___, -(true___)], (427 ^ _87308) ^ [] : [true___, -(true___)], (433 ^ _87308) ^ [] : [true___, -(true___)], (439 ^ _87308) ^ [] : [true___, -(true___)], (445 ^ _87308) ^ [] : [true___, -(true___)], (451 ^ _87308) ^ [] : [true___, -(true___)], (458 ^ _87308) ^ [_101577] : [-(element(456 ^ [_101577], _101577))], (460 ^ _87308) ^ [] : [-(empty(empty_set))], (462 ^ _87308) ^ [_101726, _101728] : [empty(ordered_pair(_101728, _101726))], (464 ^ _87308) ^ [] : [-(relation(empty_set))], (466 ^ _87308) ^ [] : [-(relation_empty_yielding(empty_set))], (468 ^ _87308) ^ [] : [-(function(empty_set))], (470 ^ _87308) ^ [] : [-(one_to_one(empty_set))], (472 ^ _87308) ^ [] : [-(empty(empty_set))], (474 ^ _87308) ^ [] : [-(epsilon_transitive(empty_set))], (476 ^ _87308) ^ [] : [-(epsilon_connected(empty_set))], (478 ^ _87308) ^ [] : [-(ordinal(empty_set))], (480 ^ _87308) ^ [_102275, _102277] : [-(empty(_102277)), empty(set_union2(_102277, _102275))], (486 ^ _87308) ^ [_102491, _102493] : [-(empty(_102493)), empty(set_union2(_102491, _102493))], (492 ^ _87308) ^ [_102692, _102694] : [-(set_union2(_102694, _102694) = _102694)], (495 ^ _87308) ^ [] : [-(relation(493 ^ []))], (497 ^ _87308) ^ [] : [-(function(493 ^ []))], (500 ^ _87308) ^ [] : [-(epsilon_transitive(498 ^ []))], (502 ^ _87308) ^ [] : [-(epsilon_connected(498 ^ []))], (504 ^ _87308) ^ [] : [-(ordinal(498 ^ []))], (507 ^ _87308) ^ [] : [-(empty(505 ^ []))], (510 ^ _87308) ^ [] : [-(relation(508 ^ []))], (512 ^ _87308) ^ [] : [-(empty(508 ^ []))], (514 ^ _87308) ^ [] : [-(function(508 ^ []))], (517 ^ _87308) ^ [] : [-(relation(515 ^ []))], (519 ^ _87308) ^ [] : [-(function(515 ^ []))], (521 ^ _87308) ^ [] : [-(one_to_one(515 ^ []))], (523 ^ _87308) ^ [] : [-(empty(515 ^ []))], (525 ^ _87308) ^ [] : [-(epsilon_transitive(515 ^ []))], (527 ^ _87308) ^ [] : [-(epsilon_connected(515 ^ []))], (529 ^ _87308) ^ [] : [-(ordinal(515 ^ []))], (532 ^ _87308) ^ [] : [empty(530 ^ [])], (535 ^ _87308) ^ [] : [-(relation(533 ^ []))], (537 ^ _87308) ^ [] : [-(function(533 ^ []))], (539 ^ _87308) ^ [] : [-(one_to_one(533 ^ []))], (542 ^ _87308) ^ [] : [empty(540 ^ [])], (544 ^ _87308) ^ [] : [-(epsilon_transitive(540 ^ []))], (546 ^ _87308) ^ [] : [-(epsilon_connected(540 ^ []))], (548 ^ _87308) ^ [] : [-(ordinal(540 ^ []))], (551 ^ _87308) ^ [] : [-(relation(549 ^ []))], (553 ^ _87308) ^ [] : [-(relation_empty_yielding(549 ^ []))], (555 ^ _87308) ^ [] : [-(function(549 ^ []))], (557 ^ _87308) ^ [_104672, _104674] : [-(subset(_104674, _104674))], (559 ^ _87308) ^ [_104752] : [-(set_union2(_104752, empty_set) = _104752)], (561 ^ _87308) ^ [_104862, _104864] : [in(_104864, _104862), -(element(_104864, _104862))], (567 ^ _87308) ^ [_105072, _105074] : [element(_105074, _105072), -(empty(_105072)), -(in(_105074, _105072))], (577 ^ _87308) ^ [_105399, _105401] : [element(_105401, powerset(_105399)), -(subset(_105401, _105399))], (583 ^ _87308) ^ [_105565, _105567] : [subset(_105567, _105565), -(element(_105567, powerset(_105565)))], (589 ^ _87308) ^ [_105795, _105797, _105799] : [-(element(_105799, _105795)), in(_105799, _105797), element(_105797, powerset(_105795))], (599 ^ _87308) ^ [_106122, _106124, _106126] : [in(_106126, _106124), element(_106124, powerset(_106122)), empty(_106122)], (609 ^ _87308) ^ [_106418] : [empty(_106418), -(_106418 = empty_set)], (615 ^ _87308) ^ [_106620, _106622] : [in(_106622, _106620), empty(_106620)], (621 ^ _87308) ^ [_106807, _106809] : [empty(_106809), -(_106809 = _106807), empty(_106807)]], input).
% 4.94/5.51 ncf('1',plain,[reflexive(inclusion_relation(630 ^ []))],start(632 ^ 0)).
% 4.94/5.51 ncf('1.1',plain,[-(reflexive(inclusion_relation(630 ^ []))), 389 : is_reflexive_in(inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))), 389 : relation(inclusion_relation(630 ^ []))],extension(379 ^ 1,bind([[_99853], [inclusion_relation(630 ^ [])]]))).
% 4.94/5.51 ncf('1.1.1',plain,[-(is_reflexive_in(inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ [])))), 311 : -(in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ [])))), 308 : relation(inclusion_relation(630 ^ []))],extension(294 ^ 4,bind([[_96877, _97376], [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]))).
% 4.94/5.51 ncf('1.1.1.1',plain,[in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))), 327 : in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))), 335 : in(ordered_pair(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), inclusion_relation(630 ^ [])), 335 : -(subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])), 327 : inclusion_relation(630 ^ []) = inclusion_relation(relation_field(inclusion_relation(630 ^ []))), 321 : relation(inclusion_relation(630 ^ []))],extension(317 ^ 9,bind([[_97756, _97758, _98119, _98121], [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ [])), 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.1',plain,[-(in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))))],reduction('1.1.1')).
% 4.94/5.51 ncf('1.1.1.1.2',plain,[-(in(ordered_pair(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), inclusion_relation(630 ^ []))), 302 : in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))), 302 : is_reflexive_in(inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))), 298 : relation(inclusion_relation(630 ^ []))],extension(294 ^ 16,bind([[_96877, _97051, _97193], [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ [])), 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.2.1',plain,[-(in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))))],reduction('1.1.1')).
% 4.94/5.51 ncf('1.1.1.1.2.2',plain,[-(is_reflexive_in(inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ [])))), 311 : -(in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))))],extension(308 ^ 19,bind([[_97376], [relation_field(inclusion_relation(630 ^ []))]]))).
% 4.94/5.51 ncf('1.1.1.1.2.2.1',plain,[in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))), in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))), 341 : subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), 341 : -(in(ordered_pair(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), inclusion_relation(630 ^ [])))],extension(327 ^ 22,bind([[_98119, _98121], [309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.2.2.1.1',plain,[-(in(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], relation_field(inclusion_relation(630 ^ []))))],reduction('1.1.1.1.2.2')).
% 4.94/5.51 ncf('1.1.1.1.2.2.1.2',plain,[-(subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]))],extension(557 ^ 25,bind([[_104672, _104674], [_61545, 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.2.2.1.3',plain,[in(ordered_pair(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), inclusion_relation(630 ^ []))],reduction('1.1.1.1')).
% 4.94/5.51 ncf('1.1.1.1.2.3',plain,[-(relation(inclusion_relation(630 ^ [])))],extension(407 ^ 17,bind([[_100507], [630 ^ []]]))).
% 4.94/5.51 ncf('1.1.1.1.3',plain,[subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), -(subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])), 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]],extension(104 ^ 16,bind([[_90613, _90615, _90617, _90619], [309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.3.1',plain,[subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), -(subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])), 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]],extension(104 ^ 17,bind([[_90613, _90615, _90617, _90619], [309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.3.1.1',plain,[subset(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), -(in(ordered_pair(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), inclusion_relation(630 ^ [])))],extension(341 ^ 18)).
% 4.94/5.51 ncf('1.1.1.1.3.1.1.1',plain,[in(ordered_pair(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))], 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]), inclusion_relation(630 ^ []))],extension(313 ^ 19)).
% 4.94/5.51 ncf('1.1.1.1.3.1.2',plain,[-(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])],extension(2 ^ 18,bind([[_87452], [309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.3.1.3',plain,[-(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])],extension(2 ^ 18,bind([[_87452], [309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.3.2',plain,[-(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])],extension(2 ^ 17,bind([[_87452], [309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))]]]))).
% 4.94/5.51 ncf('1.1.1.1.3.3',plain,[-(309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))] = 309 ^ [inclusion_relation(630 ^ []), relation_field(inclusion_relation(630 ^ []))])],lemmata('[1, 1, 1, 1].x')).
% 4.94/5.51 ncf('1.1.1.1.4',plain,[-(inclusion_relation(630 ^ []) = inclusion_relation(relation_field(inclusion_relation(630 ^ [])))), 630 ^ [] = relation_field(inclusion_relation(630 ^ []))],extension(226 ^ 12,bind([[_94664, _94666], [relation_field(inclusion_relation(630 ^ [])), 630 ^ []]]))).
% 4.94/5.51 ncf('1.1.1.1.4.1',plain,[-(630 ^ [] = relation_field(inclusion_relation(630 ^ []))), relation_field(inclusion_relation(630 ^ [])) = 630 ^ []],extension(4 ^ 13,bind([[_87559, _87561], [630 ^ [], relation_field(inclusion_relation(630 ^ []))]]))).
% 4.94/5.51 ncf('1.1.1.1.4.1.1',plain,[-(relation_field(inclusion_relation(630 ^ [])) = 630 ^ []), 321 : inclusion_relation(630 ^ []) = inclusion_relation(630 ^ []), 321 : relation(inclusion_relation(630 ^ []))],extension(317 ^ 14,bind([[_97756, _97758], [inclusion_relation(630 ^ []), 630 ^ []]]))).
% 4.94/5.51 ncf('1.1.1.1.4.1.1.1',plain,[-(inclusion_relation(630 ^ []) = inclusion_relation(630 ^ []))],extension(2 ^ 17,bind([[_87452], [inclusion_relation(630 ^ [])]]))).
% 4.94/5.51 ncf('1.1.1.1.4.1.1.2',plain,[-(relation(inclusion_relation(630 ^ [])))],extension(407 ^ 15,bind([[_100507], [630 ^ []]]))).
% 4.94/5.51 ncf('1.1.1.1.5',plain,[-(relation(inclusion_relation(630 ^ [])))],extension(407 ^ 10,bind([[_100507], [630 ^ []]]))).
% 4.94/5.51 ncf('1.1.1.2',plain,[-(relation(inclusion_relation(630 ^ [])))],extension(407 ^ 5,bind([[_100507], [630 ^ []]]))).
% 4.94/5.51 ncf('1.1.2',plain,[-(relation(inclusion_relation(630 ^ [])))],extension(407 ^ 2,bind([[_100507], [630 ^ []]]))).
% 4.94/5.51 %-----------------------------------------------------
% 4.94/5.51 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------