%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET792+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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 0.49s 1.37s
% Output : Proof 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SET792+4 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n031.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 19:21:25 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.49/1.37
% 0.49/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.49/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.49/1.37 %-----------------------------------------------------
% 0.49/1.37 ncf(matrix, plain, [(587 ^ _79680) ^ [] : [-(order(583 ^ [], 584 ^ []))], (589 ^ _79680) ^ [] : [-(least(585 ^ [], 583 ^ [], 584 ^ []))], (591 ^ _79680) ^ [] : [min(585 ^ [], 583 ^ [], 584 ^ [])], (2 ^ _79680) ^ [_79804] : [-(_79804 = _79804)], (4 ^ _79680) ^ [_79911, _79913] : [_79913 = _79911, -(_79911 = _79913)], (10 ^ _79680) ^ [_80115, _80117, _80119] : [-(_80119 = _80115), _80119 = _80117, _80117 = _80115], (20 ^ _79680) ^ [_80456, _80458, _80460, _80462] : [-(total_order(_80460, _80456)), total_order(_80462, _80458), _80462 = _80460, _80458 = _80456], (34 ^ _79680) ^ [_80928, _80930, _80932, _80934, _80936, _80938] : [-(greatest(_80936, _80932, _80928)), greatest(_80938, _80934, _80930), _80938 = _80936, _80934 = _80932, _80930 = _80928], (52 ^ _79680) ^ [_81537, _81539, _81541, _81543, _81545, _81547] : [-(max(_81545, _81541, _81537)), max(_81547, _81543, _81539), _81547 = _81545, _81543 = _81541, _81539 = _81537], (70 ^ _79680) ^ [_82174, _82176, _82178, _82180, _82182, _82184, _82186, _82188] : [-(least_upper_bound(_82186, _82182, _82178, _82174)), least_upper_bound(_82188, _82184, _82180, _82176), _82188 = _82186, _82184 = _82182, _82180 = _82178, _82176 = _82174], (92 ^ _79680) ^ [_82936, _82938, _82940, _82942, _82944, _82946] : [-(upper_bound(_82944, _82940, _82936)), upper_bound(_82946, _82942, _82938), _82946 = _82944, _82942 = _82940, _82938 = _82936], (110 ^ _79680) ^ [_83573, _83575, _83577, _83579, _83581, _83583, _83585, _83587] : [-(greatest_lower_bound(_83585, _83581, _83577, _83573)), greatest_lower_bound(_83587, _83583, _83579, _83575), _83587 = _83585, _83583 = _83581, _83579 = _83577, _83575 = _83573], (132 ^ _79680) ^ [_84307, _84309, _84311, _84313] : [-(member(_84311, _84307)), member(_84313, _84309), _84313 = _84311, _84309 = _84307], (146 ^ _79680) ^ [_84779, _84781, _84783, _84785, _84787, _84789] : [-(lower_bound(_84787, _84783, _84779)), lower_bound(_84789, _84785, _84781), _84789 = _84787, _84785 = _84783, _84781 = _84779], (164 ^ _79680) ^ [_85388, _85390, _85392, _85394, _85396, _85398] : [-(apply(_85396, _85392, _85388)), apply(_85398, _85394, _85390), _85398 = _85396, _85394 = _85392, _85390 = _85388], (182 ^ _79680) ^ [_85969, _85971, _85973, _85975] : [-(order(_85973, _85969)), order(_85975, _85971), _85975 = _85973, _85971 = _85969], (196 ^ _79680) ^ [_86441, _86443, _86445, _86447, _86449, _86451] : [-(least(_86449, _86445, _86441)), least(_86451, _86447, _86443), _86451 = _86449, _86447 = _86445, _86443 = _86441], (214 ^ _79680) ^ [_87030, _87032, _87034, _87036, _87038, _87040] : [-(min(_87038, _87034, _87030)), min(_87040, _87036, _87032), _87040 = _87038, _87036 = _87034, _87032 = _87030], (282 ^ _79680) ^ [_89240, _89242] : [-(order(_89242, _89240)), 286 ^ _79680 : [(287 ^ _79680) ^ [] : [-(member(285 ^ [_89240, _89242], _89240))], (289 ^ _79680) ^ [] : [apply(_89242, 285 ^ [_89240, _89242], 285 ^ [_89240, _89242])]], 294 ^ _79680 : [(295 ^ _79680) ^ [] : [-(member(292 ^ [_89240, _89242], _89240))], (297 ^ _79680) ^ [] : [-(member(293 ^ [_89240, _89242], _89240))], (299 ^ _79680) ^ [] : [-(apply(_89242, 292 ^ [_89240, _89242], 293 ^ [_89240, _89242]))], (301 ^ _79680) ^ [] : [-(apply(_89242, 293 ^ [_89240, _89242], 292 ^ [_89240, _89242]))], (303 ^ _79680) ^ [] : [292 ^ [_89240, _89242] = 293 ^ [_89240, _89242]]], 307 ^ _79680 : [(308 ^ _79680) ^ [] : [-(member(304 ^ [_89240, _89242], _89240))], (310 ^ _79680) ^ [] : [-(member(305 ^ [_89240, _89242], _89240))], (312 ^ _79680) ^ [] : [-(member(306 ^ [_89240, _89242], _89240))], (314 ^ _79680) ^ [] : [-(apply(_89242, 304 ^ [_89240, _89242], 305 ^ [_89240, _89242]))], (316 ^ _79680) ^ [] : [-(apply(_89242, 305 ^ [_89240, _89242], 306 ^ [_89240, _89242]))], (318 ^ _79680) ^ [] : [apply(_89242, 304 ^ [_89240, _89242], 306 ^ [_89240, _89242])]]], (232 ^ _79680) ^ [_87640, _87642] : [order(_87642, _87640), 235 ^ _79680 : [(236 ^ _79680) ^ [_87894] : [member(_87894, _87640), -(apply(_87642, _87894, _87894))], (242 ^ _79680) ^ [_88116, _88118] : [member(_88118, _87640), member(_88116, _87640), -(_88118 = _88116), apply(_87642, _88118, _88116), apply(_87642, _88116, _88118)], (260 ^ _79680) ^ [_88633, _88635, _88637] : [member(_88637, _87640), member(_88635, _87640), member(_88633, _87640), -(apply(_87642, _88637, _88633)), apply(_87642, _88637, _88635), apply(_87642, _88635, _88633)]]], (342 ^ _79680) ^ [_91761, _91763] : [-(total_order(_91763, _91761)), order(_91763, _91761), 349 ^ _79680 : [(350 ^ _79680) ^ [] : [-(member(347 ^ [_91761, _91763], _91761))], (352 ^ _79680) ^ [] : [-(member(348 ^ [_91761, _91763], _91761))], (354 ^ _79680) ^ [] : [apply(_91763, 347 ^ [_91761, _91763], 348 ^ [_91761, _91763])], (356 ^ _79680) ^ [] : [apply(_91763, 348 ^ [_91761, _91763], 347 ^ [_91761, _91763])]]], (322 ^ _79680) ^ [_91133, _91135] : [total_order(_91135, _91133), 325 ^ _79680 : [(326 ^ _79680) ^ [] : [-(order(_91135, _91133))], (328 ^ _79680) ^ [_91375, _91377] : [member(_91377, _91133), member(_91375, _91133), -(apply(_91135, _91377, _91375)), -(apply(_91135, _91375, _91377))]]], (370 ^ _79680) ^ [_92872, _92874, _92876] : [372 ^ _79680 : [(373 ^ _79680) ^ [] : [-(member(371 ^ [_92872, _92874, _92876], _92874))], (375 ^ _79680) ^ [] : [apply(_92876, 371 ^ [_92872, _92874, _92876], _92872)]], -(upper_bound(_92872, _92876, _92874))], (360 ^ _79680) ^ [_92541, _92543, _92545] : [upper_bound(_92541, _92545, _92543), 363 ^ _79680 : [(364 ^ _79680) ^ [_92685] : [member(_92685, _92543), -(apply(_92545, _92685, _92541))]]], (389 ^ _79680) ^ [_93624, _93626, _93628] : [391 ^ _79680 : [(392 ^ _79680) ^ [] : [-(member(390 ^ [_93624, _93626, _93628], _93626))], (394 ^ _79680) ^ [] : [apply(_93628, _93624, 390 ^ [_93624, _93626, _93628])]], -(lower_bound(_93624, _93628, _93626))], (379 ^ _79680) ^ [_93293, _93295, _93297] : [lower_bound(_93293, _93297, _93295), 382 ^ _79680 : [(383 ^ _79680) ^ [_93437] : [member(_93437, _93295), -(apply(_93297, _93293, _93437))]]], (398 ^ _79680) ^ [_94045, _94047, _94049] : [greatest(_94045, _94049, _94047), 401 ^ _79680 : [(402 ^ _79680) ^ [] : [-(member(_94045, _94047))], (404 ^ _79680) ^ [_94263] : [member(_94263, _94047), -(apply(_94049, _94263, _94045))]]], (410 ^ _79680) ^ [_94452, _94454, _94456] : [-(greatest(_94452, _94456, _94454)), member(_94452, _94454), 416 ^ _79680 : [(417 ^ _79680) ^ [] : [-(member(415 ^ [_94452, _94454, _94456], _94454))], (419 ^ _79680) ^ [] : [apply(_94456, 415 ^ [_94452, _94454, _94456], _94452)]]], (423 ^ _79680) ^ [_94966, _94968, _94970] : [least(_94966, _94970, _94968), 426 ^ _79680 : [(427 ^ _79680) ^ [] : [-(member(_94966, _94968))], (429 ^ _79680) ^ [_95184] : [member(_95184, _94968), -(apply(_94970, _94966, _95184))]]], (435 ^ _79680) ^ [_95373, _95375, _95377] : [-(least(_95373, _95377, _95375)), member(_95373, _95375), 441 ^ _79680 : [(442 ^ _79680) ^ [] : [-(member(440 ^ [_95373, _95375, _95377], _95375))], (444 ^ _79680) ^ [] : [apply(_95377, _95373, 440 ^ [_95373, _95375, _95377])]]], (464 ^ _79680) ^ [_96397, _96399, _96401] : [-(max(_96397, _96401, _96399)), member(_96397, _96399), 470 ^ _79680 : [(471 ^ _79680) ^ [] : [-(member(469 ^ [_96397, _96399, _96401], _96399))], (473 ^ _79680) ^ [] : [-(apply(_96401, _96397, 469 ^ [_96397, _96399, _96401]))], (475 ^ _79680) ^ [] : [_96397 = 469 ^ [_96397, _96399, _96401]]]], (448 ^ _79680) ^ [_95887, _95889, _95891] : [max(_95887, _95891, _95889), 451 ^ _79680 : [(452 ^ _79680) ^ [] : [-(member(_95887, _95889))], (454 ^ _79680) ^ [_96111] : [-(_95887 = _96111), member(_96111, _95889), apply(_95891, _95887, _96111)]]], (495 ^ _79680) ^ [_97514, _97516, _97518] : [-(min(_97514, _97518, _97516)), member(_97514, _97516), 501 ^ _79680 : [(502 ^ _79680) ^ [] : [-(member(500 ^ [_97514, _97516, _97518], _97516))], (504 ^ _79680) ^ [] : [-(apply(_97518, 500 ^ [_97514, _97516, _97518], _97514))], (506 ^ _79680) ^ [] : [_97514 = 500 ^ [_97514, _97516, _97518]]]], (479 ^ _79680) ^ [_97004, _97006, _97008] : [min(_97004, _97008, _97006), 482 ^ _79680 : [(483 ^ _79680) ^ [] : [-(member(_97004, _97006))], (485 ^ _79680) ^ [_97228] : [-(_97004 = _97228), member(_97228, _97006), apply(_97008, _97228, _97004)]]], (510 ^ _79680) ^ [_98135, _98137, _98139, _98141] : [least_upper_bound(_98141, _98139, _98137, _98135), 513 ^ _79680 : [(514 ^ _79680) ^ [] : [-(member(_98141, _98139))], (516 ^ _79680) ^ [] : [-(upper_bound(_98141, _98137, _98139))], (518 ^ _79680) ^ [_98446] : [-(apply(_98137, _98141, _98446)), member(_98446, _98135), upper_bound(_98446, _98137, _98139)]]], (528 ^ _79680) ^ [_98748, _98750, _98752, _98754] : [-(least_upper_bound(_98754, _98752, _98750, _98748)), member(_98754, _98752), upper_bound(_98754, _98750, _98752), 538 ^ _79680 : [(539 ^ _79680) ^ [] : [-(member(537 ^ [_98748, _98750, _98752, _98754], _98748))], (541 ^ _79680) ^ [] : [-(upper_bound(537 ^ [_98748, _98750, _98752, _98754], _98750, _98752))], (543 ^ _79680) ^ [] : [apply(_98750, _98754, 537 ^ [_98748, _98750, _98752, _98754])]]], (547 ^ _79680) ^ [_99477, _99479, _99481, _99483] : [greatest_lower_bound(_99483, _99481, _99479, _99477), 550 ^ _79680 : [(551 ^ _79680) ^ [] : [-(member(_99483, _99481))], (553 ^ _79680) ^ [] : [-(lower_bound(_99483, _99479, _99481))], (555 ^ _79680) ^ [_99788] : [-(apply(_99479, _99788, _99483)), member(_99788, _99477), lower_bound(_99788, _99479, _99481)]]], (565 ^ _79680) ^ [_100090, _100092, _100094, _100096] : [-(greatest_lower_bound(_100096, _100094, _100092, _100090)), member(_100096, _100094), lower_bound(_100096, _100092, _100094), 575 ^ _79680 : [(576 ^ _79680) ^ [] : [-(member(574 ^ [_100090, _100092, _100094, _100096], _100090))], (578 ^ _79680) ^ [] : [-(lower_bound(574 ^ [_100090, _100092, _100094, _100096], _100092, _100094))], (580 ^ _79680) ^ [] : [apply(_100092, 574 ^ [_100090, _100092, _100094, _100096], _100096)]]]], input).
% 0.49/1.37 ncf('1',plain,[min(585 ^ [], 583 ^ [], 584 ^ [])],start(591 ^ 0)).
% 0.49/1.37 ncf('1.1',plain,[-(min(585 ^ [], 583 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 504 : -(apply(583 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []], 585 ^ []))],extension(495 ^ 1,bind([[_97514, _97516, _97518], [585 ^ [], 584 ^ [], 583 ^ []]]))).
% 0.49/1.37 ncf('1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 585 ^ [] = 585 ^ [], 584 ^ [] = 584 ^ []],extension(132 ^ 2,bind([[_84307, _84309, _84311, _84313], [584 ^ [], 584 ^ [], 585 ^ [], 585 ^ []]]))).
% 0.49/1.37 ncf('1.1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), member(585 ^ [], 584 ^ []), 585 ^ [] = 585 ^ [], 584 ^ [] = 584 ^ []],extension(132 ^ 3,bind([[_84307, _84309, _84311, _84313], [584 ^ [], 584 ^ [], 585 ^ [], 585 ^ []]]))).
% 0.49/1.37 ncf('1.1.1.1.1',plain,[-(member(585 ^ [], 584 ^ [])), least(585 ^ [], 583 ^ [], 584 ^ [])],extension(423 ^ 4,bind([[_94966, _94968, _94970], [585 ^ [], 584 ^ [], 583 ^ []]]))).
% 0.49/1.37 ncf('1.1.1.1.1.1',plain,[-(least(585 ^ [], 583 ^ [], 584 ^ []))],extension(589 ^ 5)).
% 0.49/1.37 ncf('1.1.1.1.2',plain,[-(585 ^ [] = 585 ^ [])],extension(2 ^ 4,bind([[_79804], [585 ^ []]]))).
% 0.49/1.37 ncf('1.1.1.1.3',plain,[-(584 ^ [] = 584 ^ [])],extension(2 ^ 4,bind([[_79804], [584 ^ []]]))).
% 0.49/1.37 ncf('1.1.1.2',plain,[-(585 ^ [] = 585 ^ [])],extension(2 ^ 3,bind([[_79804], [585 ^ []]]))).
% 0.49/1.37 ncf('1.1.1.3',plain,[-(584 ^ [] = 584 ^ [])],extension(2 ^ 3,bind([[_79804], [584 ^ []]]))).
% 0.49/1.37 ncf('1.1.2',plain,[apply(583 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []], 585 ^ []), 242 : member(500 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []), 242 : member(585 ^ [], 584 ^ []), 242 : -(500 ^ [585 ^ [], 584 ^ [], 583 ^ []] = 585 ^ []), 242 : apply(583 ^ [], 585 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []]), 242 : order(583 ^ [], 584 ^ [])],extension(232 ^ 4,bind([[_87640, _87642, _88116, _88118], [584 ^ [], 583 ^ [], 585 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 0.49/1.37 ncf('1.1.2.1',plain,[-(member(500 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []))],extension(502 ^ 7)).
% 0.49/1.37 ncf('1.1.2.2',plain,[-(member(585 ^ [], 584 ^ []))],lemmata('[1].x')).
% 0.49/1.37 ncf('1.1.2.3',plain,[500 ^ [585 ^ [], 584 ^ [], 583 ^ []] = 585 ^ [], -(585 ^ [] = 500 ^ [585 ^ [], 584 ^ [], 583 ^ []])],extension(4 ^ 7,bind([[_79911, _79913], [585 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 0.49/1.37 ncf('1.1.2.3.1',plain,[585 ^ [] = 500 ^ [585 ^ [], 584 ^ [], 583 ^ []]],extension(506 ^ 8)).
% 0.49/1.37 ncf('1.1.2.4',plain,[-(apply(583 ^ [], 585 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []])), 429 : member(500 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []), 429 : least(585 ^ [], 583 ^ [], 584 ^ [])],extension(423 ^ 7,bind([[_94966, _94968, _94970, _95184], [585 ^ [], 584 ^ [], 583 ^ [], 500 ^ [585 ^ [], 584 ^ [], 583 ^ []]]]))).
% 0.49/1.37 ncf('1.1.2.4.1',plain,[-(member(500 ^ [585 ^ [], 584 ^ [], 583 ^ []], 584 ^ []))],extension(502 ^ 10)).
% 0.49/1.37 ncf('1.1.2.4.2',plain,[-(least(585 ^ [], 583 ^ [], 584 ^ []))],extension(589 ^ 8)).
% 0.49/1.37 ncf('1.1.2.5',plain,[-(order(583 ^ [], 584 ^ []))],extension(587 ^ 5)).
% 0.49/1.37 %-----------------------------------------------------
% 0.49/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------