%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET794+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:26 EDT 2023
% Result : Theorem 1.30s 2.42s
% Output : Proof 1.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SET794+4 : TPTP v8.1.2. Released v3.2.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n022.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 19:21:17 EDT 2023
% 0.14/0.35 % CPUTime :
% 1.30/2.42
% 1.30/2.42 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 1.30/2.42 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.30/2.42 %-----------------------------------------------------
% 1.30/2.42 ncf(matrix, plain, [(587 ^ _80350) ^ [] : [-(total_order(583 ^ [], 584 ^ []))], (589 ^ _80350) ^ [] : [-(min(585 ^ [], 583 ^ [], 584 ^ []))], (591 ^ _80350) ^ [] : [least(585 ^ [], 583 ^ [], 584 ^ [])], (2 ^ _80350) ^ [_80474] : [-(_80474 = _80474)], (4 ^ _80350) ^ [_80581, _80583] : [_80583 = _80581, -(_80581 = _80583)], (10 ^ _80350) ^ [_80785, _80787, _80789] : [-(_80789 = _80785), _80789 = _80787, _80787 = _80785], (20 ^ _80350) ^ [_81126, _81128, _81130, _81132] : [-(order(_81130, _81126)), order(_81132, _81128), _81132 = _81130, _81128 = _81126], (34 ^ _80350) ^ [_81598, _81600, _81602, _81604, _81606, _81608] : [-(greatest(_81606, _81602, _81598)), greatest(_81608, _81604, _81600), _81608 = _81606, _81604 = _81602, _81600 = _81598], (52 ^ _80350) ^ [_82207, _82209, _82211, _82213, _82215, _82217] : [-(max(_82215, _82211, _82207)), max(_82217, _82213, _82209), _82217 = _82215, _82213 = _82211, _82209 = _82207], (70 ^ _80350) ^ [_82844, _82846, _82848, _82850, _82852, _82854, _82856, _82858] : [-(least_upper_bound(_82856, _82852, _82848, _82844)), least_upper_bound(_82858, _82854, _82850, _82846), _82858 = _82856, _82854 = _82852, _82850 = _82848, _82846 = _82844], (92 ^ _80350) ^ [_83606, _83608, _83610, _83612, _83614, _83616] : [-(upper_bound(_83614, _83610, _83606)), upper_bound(_83616, _83612, _83608), _83616 = _83614, _83612 = _83610, _83608 = _83606], (110 ^ _80350) ^ [_84243, _84245, _84247, _84249, _84251, _84253, _84255, _84257] : [-(greatest_lower_bound(_84255, _84251, _84247, _84243)), greatest_lower_bound(_84257, _84253, _84249, _84245), _84257 = _84255, _84253 = _84251, _84249 = _84247, _84245 = _84243], (132 ^ _80350) ^ [_84977, _84979, _84981, _84983] : [-(member(_84981, _84977)), member(_84983, _84979), _84983 = _84981, _84979 = _84977], (146 ^ _80350) ^ [_85449, _85451, _85453, _85455, _85457, _85459] : [-(lower_bound(_85457, _85453, _85449)), lower_bound(_85459, _85455, _85451), _85459 = _85457, _85455 = _85453, _85451 = _85449], (164 ^ _80350) ^ [_86058, _86060, _86062, _86064, _86066, _86068] : [-(apply(_86066, _86062, _86058)), apply(_86068, _86064, _86060), _86068 = _86066, _86064 = _86062, _86060 = _86058], (182 ^ _80350) ^ [_86639, _86641, _86643, _86645] : [-(total_order(_86643, _86639)), total_order(_86645, _86641), _86645 = _86643, _86641 = _86639], (196 ^ _80350) ^ [_87111, _87113, _87115, _87117, _87119, _87121] : [-(min(_87119, _87115, _87111)), min(_87121, _87117, _87113), _87121 = _87119, _87117 = _87115, _87113 = _87111], (214 ^ _80350) ^ [_87700, _87702, _87704, _87706, _87708, _87710] : [-(least(_87708, _87704, _87700)), least(_87710, _87706, _87702), _87710 = _87708, _87706 = _87704, _87702 = _87700], (282 ^ _80350) ^ [_89910, _89912] : [-(order(_89912, _89910)), 286 ^ _80350 : [(287 ^ _80350) ^ [] : [-(member(285 ^ [_89910, _89912], _89910))], (289 ^ _80350) ^ [] : [apply(_89912, 285 ^ [_89910, _89912], 285 ^ [_89910, _89912])]], 294 ^ _80350 : [(295 ^ _80350) ^ [] : [-(member(292 ^ [_89910, _89912], _89910))], (297 ^ _80350) ^ [] : [-(member(293 ^ [_89910, _89912], _89910))], (299 ^ _80350) ^ [] : [-(apply(_89912, 292 ^ [_89910, _89912], 293 ^ [_89910, _89912]))], (301 ^ _80350) ^ [] : [-(apply(_89912, 293 ^ [_89910, _89912], 292 ^ [_89910, _89912]))], (303 ^ _80350) ^ [] : [292 ^ [_89910, _89912] = 293 ^ [_89910, _89912]]], 307 ^ _80350 : [(308 ^ _80350) ^ [] : [-(member(304 ^ [_89910, _89912], _89910))], (310 ^ _80350) ^ [] : [-(member(305 ^ [_89910, _89912], _89910))], (312 ^ _80350) ^ [] : [-(member(306 ^ [_89910, _89912], _89910))], (314 ^ _80350) ^ [] : [-(apply(_89912, 304 ^ [_89910, _89912], 305 ^ [_89910, _89912]))], (316 ^ _80350) ^ [] : [-(apply(_89912, 305 ^ [_89910, _89912], 306 ^ [_89910, _89912]))], (318 ^ _80350) ^ [] : [apply(_89912, 304 ^ [_89910, _89912], 306 ^ [_89910, _89912])]]], (232 ^ _80350) ^ [_88310, _88312] : [order(_88312, _88310), 235 ^ _80350 : [(236 ^ _80350) ^ [_88564] : [member(_88564, _88310), -(apply(_88312, _88564, _88564))], (242 ^ _80350) ^ [_88786, _88788] : [member(_88788, _88310), member(_88786, _88310), -(_88788 = _88786), apply(_88312, _88788, _88786), apply(_88312, _88786, _88788)], (260 ^ _80350) ^ [_89303, _89305, _89307] : [member(_89307, _88310), member(_89305, _88310), member(_89303, _88310), -(apply(_88312, _89307, _89303)), apply(_88312, _89307, _89305), apply(_88312, _89305, _89303)]]], (342 ^ _80350) ^ [_92431, _92433] : [-(total_order(_92433, _92431)), order(_92433, _92431), 349 ^ _80350 : [(350 ^ _80350) ^ [] : [-(member(347 ^ [_92431, _92433], _92431))], (352 ^ _80350) ^ [] : [-(member(348 ^ [_92431, _92433], _92431))], (354 ^ _80350) ^ [] : [apply(_92433, 347 ^ [_92431, _92433], 348 ^ [_92431, _92433])], (356 ^ _80350) ^ [] : [apply(_92433, 348 ^ [_92431, _92433], 347 ^ [_92431, _92433])]]], (322 ^ _80350) ^ [_91803, _91805] : [total_order(_91805, _91803), 325 ^ _80350 : [(326 ^ _80350) ^ [] : [-(order(_91805, _91803))], (328 ^ _80350) ^ [_92045, _92047] : [member(_92047, _91803), member(_92045, _91803), -(apply(_91805, _92047, _92045)), -(apply(_91805, _92045, _92047))]]], (370 ^ _80350) ^ [_93542, _93544, _93546] : [372 ^ _80350 : [(373 ^ _80350) ^ [] : [-(member(371 ^ [_93542, _93544, _93546], _93544))], (375 ^ _80350) ^ [] : [apply(_93546, 371 ^ [_93542, _93544, _93546], _93542)]], -(upper_bound(_93542, _93546, _93544))], (360 ^ _80350) ^ [_93211, _93213, _93215] : [upper_bound(_93211, _93215, _93213), 363 ^ _80350 : [(364 ^ _80350) ^ [_93355] : [member(_93355, _93213), -(apply(_93215, _93355, _93211))]]], (389 ^ _80350) ^ [_94294, _94296, _94298] : [391 ^ _80350 : [(392 ^ _80350) ^ [] : [-(member(390 ^ [_94294, _94296, _94298], _94296))], (394 ^ _80350) ^ [] : [apply(_94298, _94294, 390 ^ [_94294, _94296, _94298])]], -(lower_bound(_94294, _94298, _94296))], (379 ^ _80350) ^ [_93963, _93965, _93967] : [lower_bound(_93963, _93967, _93965), 382 ^ _80350 : [(383 ^ _80350) ^ [_94107] : [member(_94107, _93965), -(apply(_93967, _93963, _94107))]]], (398 ^ _80350) ^ [_94715, _94717, _94719] : [greatest(_94715, _94719, _94717), 401 ^ _80350 : [(402 ^ _80350) ^ [] : [-(member(_94715, _94717))], (404 ^ _80350) ^ [_94933] : [member(_94933, _94717), -(apply(_94719, _94933, _94715))]]], (410 ^ _80350) ^ [_95122, _95124, _95126] : [-(greatest(_95122, _95126, _95124)), member(_95122, _95124), 416 ^ _80350 : [(417 ^ _80350) ^ [] : [-(member(415 ^ [_95122, _95124, _95126], _95124))], (419 ^ _80350) ^ [] : [apply(_95126, 415 ^ [_95122, _95124, _95126], _95122)]]], (423 ^ _80350) ^ [_95636, _95638, _95640] : [least(_95636, _95640, _95638), 426 ^ _80350 : [(427 ^ _80350) ^ [] : [-(member(_95636, _95638))], (429 ^ _80350) ^ [_95854] : [member(_95854, _95638), -(apply(_95640, _95636, _95854))]]], (435 ^ _80350) ^ [_96043, _96045, _96047] : [-(least(_96043, _96047, _96045)), member(_96043, _96045), 441 ^ _80350 : [(442 ^ _80350) ^ [] : [-(member(440 ^ [_96043, _96045, _96047], _96045))], (444 ^ _80350) ^ [] : [apply(_96047, _96043, 440 ^ [_96043, _96045, _96047])]]], (464 ^ _80350) ^ [_97067, _97069, _97071] : [-(max(_97067, _97071, _97069)), member(_97067, _97069), 470 ^ _80350 : [(471 ^ _80350) ^ [] : [-(member(469 ^ [_97067, _97069, _97071], _97069))], (473 ^ _80350) ^ [] : [-(apply(_97071, _97067, 469 ^ [_97067, _97069, _97071]))], (475 ^ _80350) ^ [] : [_97067 = 469 ^ [_97067, _97069, _97071]]]], (448 ^ _80350) ^ [_96557, _96559, _96561] : [max(_96557, _96561, _96559), 451 ^ _80350 : [(452 ^ _80350) ^ [] : [-(member(_96557, _96559))], (454 ^ _80350) ^ [_96781] : [-(_96557 = _96781), member(_96781, _96559), apply(_96561, _96557, _96781)]]], (495 ^ _80350) ^ [_98184, _98186, _98188] : [-(min(_98184, _98188, _98186)), member(_98184, _98186), 501 ^ _80350 : [(502 ^ _80350) ^ [] : [-(member(500 ^ [_98184, _98186, _98188], _98186))], (504 ^ _80350) ^ [] : [-(apply(_98188, 500 ^ [_98184, _98186, _98188], _98184))], (506 ^ _80350) ^ [] : [_98184 = 500 ^ [_98184, _98186, _98188]]]], (479 ^ _80350) ^ [_97674, _97676, _97678] : [min(_97674, _97678, _97676), 482 ^ _80350 : [(483 ^ _80350) ^ [] : [-(member(_97674, _97676))], (485 ^ _80350) ^ [_97898] : [-(_97674 = _97898), member(_97898, _97676), apply(_97678, _97898, _97674)]]], (510 ^ _80350) ^ [_98805, _98807, _98809, _98811] : [least_upper_bound(_98811, _98809, _98807, _98805), 513 ^ _80350 : [(514 ^ _80350) ^ [] : [-(member(_98811, _98809))], (516 ^ _80350) ^ [] : [-(upper_bound(_98811, _98807, _98809))], (518 ^ _80350) ^ [_99116] : [-(apply(_98807, _98811, _99116)), member(_99116, _98805), upper_bound(_99116, _98807, _98809)]]], (528 ^ _80350) ^ [_99418, _99420, _99422, _99424] : [-(least_upper_bound(_99424, _99422, _99420, _99418)), member(_99424, _99422), upper_bound(_99424, _99420, _99422), 538 ^ _80350 : [(539 ^ _80350) ^ [] : [-(member(537 ^ [_99418, _99420, _99422, _99424], _99418))], (541 ^ _80350) ^ [] : [-(upper_bound(537 ^ [_99418, _99420, _99422, _99424], _99420, _99422))], (543 ^ _80350) ^ [] : [apply(_99420, _99424, 537 ^ [_99418, _99420, _99422, _99424])]]], (547 ^ _80350) ^ [_100147, _100149, _100151, _100153] : [greatest_lower_bound(_100153, _100151, _100149, _100147), 550 ^ _80350 : [(551 ^ _80350) ^ [] : [-(member(_100153, _100151))], (553 ^ _80350) ^ [] : [-(lower_bound(_100153, _100149, _100151))], (555 ^ _80350) ^ [_100458] : [-(apply(_100149, _100458, _100153)), member(_100458, _100147), lower_bound(_100458, _100149, _100151)]]], (565 ^ _80350) ^ [_100760, _100762, _100764, _100766] : [-(greatest_lower_bound(_100766, _100764, _100762, _100760)), member(_100766, _100764), lower_bound(_100766, _100762, _100764), 575 ^ _80350 : [(576 ^ _80350) ^ [] : [-(member(574 ^ [_100760, _100762, _100764, _100766], _100760))], (578 ^ _80350) ^ [] : [-(lower_bound(574 ^ [_100760, _100762, _100764, _100766], _100762, _100764))], (580 ^ _80350) ^ [] : [apply(_100762, 574 ^ [_100760, _100762, _100764, _100766], _100766)]]]], input).
% 1.30/2.42 ncf('1',plain,[least(585 ^ [], 583 ^ [], 584 ^ [])],start(591 ^ 0)).
% 1.30/2.42 ncf('1.1',plain,[-(least(585 ^ [], 583 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 442 : -(member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []))],extension(435 ^ 1,bind([[_96043, _96045, _96047], [585 ^ [], 584 ^ [], 583 ^ []]]))).
% 1.30/2.42 ncf('1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 585 ^ [] = 585 ^ [], 584 ^ [] = 584 ^ []],extension(132 ^ 2,bind([[_84977, _84979, _84981, _84983], [584 ^ [], 584 ^ [], 585 ^ [], 585 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 585 ^ [] = 585 ^ [], 584 ^ [] = 584 ^ []],extension(132 ^ 3,bind([[_84977, _84979, _84981, _84983], [584 ^ [], 584 ^ [], 585 ^ [], 585 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 585 ^ [] = 585 ^ [], 584 ^ [] = 584 ^ []],extension(132 ^ 4,bind([[_84977, _84979, _84981, _84983], [584 ^ [], 584 ^ [], 585 ^ [], 585 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), min(585 ^ [], 583 ^ [], 584 ^ [])],extension(479 ^ 5,bind([[_97674, _97676, _97678], [585 ^ [], 584 ^ [], 583 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1.1.1.1',plain,[-(min(585 ^ [], 583 ^ [], 584 ^ []))],extension(589 ^ 6)).
% 1.30/2.42 ncf('1.1.1.1.1.2',plain,[-(585 ^ [] = 585 ^ [])],extension(2 ^ 5,bind([[_80474], [585 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1.1.3',plain,[-(584 ^ [] = 584 ^ [])],extension(2 ^ 5,bind([[_80474], [584 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1.2',plain,[-(585 ^ [] = 585 ^ [])],extension(2 ^ 4,bind([[_80474], [585 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.1.3',plain,[-(584 ^ [] = 584 ^ [])],extension(2 ^ 4,bind([[_80474], [584 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.2',plain,[-(585 ^ [] = 585 ^ [])],extension(2 ^ 3,bind([[_80474], [585 ^ []]]))).
% 1.30/2.42 ncf('1.1.1.3',plain,[-(584 ^ [] = 584 ^ [])],extension(2 ^ 3,bind([[_80474], [584 ^ []]]))).
% 1.30/2.42 ncf('1.1.2',plain,[member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []), 485 : -(585 ^ [] = 440 ^ [585 ^ [], 584 ^ [], 583 ^ []]), 485 : apply(583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 585 ^ []), 485 : min(585 ^ [], 583 ^ [], 584 ^ [])],extension(479 ^ 4,bind([[_97674, _97676, _97678, _97898], [585 ^ [], 584 ^ [], 583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 1.30/2.42 ncf('1.1.2.1',plain,[585 ^ [] = 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], -(440 ^ [585 ^ [], 584 ^ [], 583 ^ []] = 585 ^ [])],extension(4 ^ 7,bind([[_80581, _80583], [440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 585 ^ []]]))).
% 1.30/2.42 ncf('1.1.2.1.1',plain,[440 ^ [585 ^ [], 584 ^ [], 583 ^ []] = 585 ^ [], -(apply(583 ^ [], 585 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])), apply(583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []]), 583 ^ [] = 583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []] = 440 ^ [585 ^ [], 584 ^ [], 583 ^ []]],extension(164 ^ 8,bind([[_86058, _86060, _86062, _86064, _86066, _86068], [440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 585 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 583 ^ [], 583 ^ []]]))).
% 1.30/2.42 ncf('1.1.2.1.1.1',plain,[apply(583 ^ [], 585 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])],extension(444 ^ 9)).
% 1.30/2.42 ncf('1.1.2.1.1.2',plain,[-(apply(583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])), 328 : member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []), 328 : member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []), 328 : -(apply(583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])), 328 : total_order(583 ^ [], 584 ^ [])],extension(322 ^ 9,bind([[_91803, _91805, _92045, _92047], [584 ^ [], 583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 1.30/2.42 ncf('1.1.2.1.1.2.1',plain,[-(member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []))],reduction('1.1')).
% 1.30/2.42 ncf('1.1.2.1.1.2.2',plain,[-(member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []))],reduction('1.1')).
% 1.30/2.42 ncf('1.1.2.1.1.2.3',plain,[apply(583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])],reduction('1.1.2.1.1')).
% 1.30/2.42 ncf('1.1.2.1.1.2.4',plain,[-(total_order(583 ^ [], 584 ^ []))],extension(587 ^ 10)).
% 1.30/2.42 ncf('1.1.2.1.1.3',plain,[-(583 ^ [] = 583 ^ [])],extension(2 ^ 9,bind([[_80474], [583 ^ []]]))).
% 1.30/2.42 ncf('1.1.2.1.1.4',plain,[-(440 ^ [585 ^ [], 584 ^ [], 583 ^ []] = 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])],extension(2 ^ 9,bind([[_80474], [440 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 1.30/2.42 ncf('1.1.2.2',plain,[-(apply(583 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 585 ^ [])), 328 : member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []), 328 : member(585 ^ [], 584 ^ []), 328 : -(apply(583 ^ [], 585 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])), 328 : total_order(583 ^ [], 584 ^ [])],extension(322 ^ 7,bind([[_91803, _91805, _92045, _92047], [584 ^ [], 583 ^ [], 585 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 1.30/2.42 ncf('1.1.2.2.1',plain,[-(member(440 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []))],reduction('1.1')).
% 1.30/2.42 ncf('1.1.2.2.2',plain,[-(member(585 ^ [], 584 ^ []))],lemmata('[1].x')).
% 1.30/2.42 ncf('1.1.2.2.3',plain,[apply(583 ^ [], 585 ^ [], 440 ^ [585 ^ [], 584 ^ [], 583 ^ []])],extension(444 ^ 10)).
% 1.30/2.42 ncf('1.1.2.2.4',plain,[-(total_order(583 ^ [], 584 ^ []))],extension(587 ^ 8)).
% 1.30/2.42 ncf('1.1.2.3',plain,[-(min(585 ^ [], 583 ^ [], 584 ^ []))],extension(589 ^ 5)).
% 1.30/2.42 %-----------------------------------------------------
% 1.30/2.42 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------