%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET801+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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:27 EDT 2023
% Result : Theorem 1.57s 2.41s
% Output : Proof 1.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET801+4 : TPTP v8.1.2. Released v3.2.0.
% 0.13/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n018.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 19:24:12 EDT 2023
% 0.13/0.34 % CPUTime :
% 1.57/2.41
% 1.57/2.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 1.57/2.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.57/2.41 %-----------------------------------------------------
% 1.57/2.41 ncf(matrix, plain, [(851 ^ _118591) ^ [] : [-(order(848 ^ [], 849 ^ []))], (854 ^ _118591) ^ [] : [-(subset(852 ^ [], 849 ^ []))], (857 ^ _118591) ^ [] : [866 ^ _118591 : [(867 ^ _118591) ^ [] : [-(member(855 ^ [], 852 ^ []))], (869 ^ _118591) ^ [] : [-(least_upper_bound(855 ^ [], 852 ^ [], 848 ^ [], 849 ^ []))], (871 ^ _118591) ^ [] : [greatest(855 ^ [], 848 ^ [], 852 ^ [])]], 858 ^ _118591 : [(859 ^ _118591) ^ [] : [-(greatest(855 ^ [], 848 ^ [], 852 ^ []))], (861 ^ _118591) ^ [] : [member(855 ^ [], 852 ^ []), least_upper_bound(855 ^ [], 852 ^ [], 848 ^ [], 849 ^ [])]]], (260 ^ _118591) ^ [_127470, _127472] : [_127472 = _127470, -(power_set(_127472) = power_set(_127470))], (266 ^ _118591) ^ [_127716, _127718, _127720, _127722] : [-(intersection(_127722, _127718) = intersection(_127720, _127716)), _127722 = _127720, _127718 = _127716], (276 ^ _118591) ^ [_128075, _128077, _128079, _128081] : [-(union(_128081, _128077) = union(_128079, _128075)), _128081 = _128079, _128077 = _128075], (286 ^ _118591) ^ [_128434, _128436, _128438, _128440] : [-(difference(_128440, _128436) = difference(_128438, _128434)), _128440 = _128438, _128436 = _128434], (296 ^ _118591) ^ [_128765, _128767] : [_128767 = _128765, -(singleton(_128767) = singleton(_128765))], (302 ^ _118591) ^ [_129011, _129013, _129015, _129017] : [-(unordered_pair(_129017, _129013) = unordered_pair(_129015, _129011)), _129017 = _129015, _129013 = _129011], (312 ^ _118591) ^ [_129342, _129344] : [_129344 = _129342, -(sum(_129344) = sum(_129342))], (318 ^ _118591) ^ [_129540, _129542] : [_129542 = _129540, -(product(_129542) = product(_129540))], (2 ^ _118591) ^ [_118735] : [-(_118735 = _118735)], (4 ^ _118591) ^ [_118842, _118844] : [_118844 = _118842, -(_118842 = _118844)], (10 ^ _118591) ^ [_119046, _119048, _119050] : [-(_119050 = _119046), _119050 = _119048, _119048 = _119046], (20 ^ _118591) ^ [_119387, _119389, _119391, _119393] : [-(equal_set(_119391, _119387)), equal_set(_119393, _119389), _119393 = _119391, _119389 = _119387], (34 ^ _118591) ^ [_119831, _119833, _119835, _119837] : [-(total_order(_119835, _119831)), total_order(_119837, _119833), _119837 = _119835, _119833 = _119831], (48 ^ _118591) ^ [_120303, _120305, _120307, _120309, _120311, _120313] : [-(least(_120311, _120307, _120303)), least(_120313, _120309, _120305), _120313 = _120311, _120309 = _120307, _120305 = _120303], (66 ^ _118591) ^ [_120912, _120914, _120916, _120918, _120920, _120922] : [-(max(_120920, _120916, _120912)), max(_120922, _120918, _120914), _120922 = _120920, _120918 = _120916, _120914 = _120912], (84 ^ _118591) ^ [_121521, _121523, _121525, _121527, _121529, _121531] : [-(min(_121529, _121525, _121521)), min(_121531, _121527, _121523), _121531 = _121529, _121527 = _121525, _121523 = _121521], (102 ^ _118591) ^ [_122130, _122132, _122134, _122136, _122138, _122140] : [-(upper_bound(_122138, _122134, _122130)), upper_bound(_122140, _122136, _122132), _122140 = _122138, _122136 = _122134, _122132 = _122130], (120 ^ _118591) ^ [_122767, _122769, _122771, _122773, _122775, _122777, _122779, _122781] : [-(greatest_lower_bound(_122779, _122775, _122771, _122767)), greatest_lower_bound(_122781, _122777, _122773, _122769), _122781 = _122779, _122777 = _122775, _122773 = _122771, _122769 = _122767], (142 ^ _118591) ^ [_123529, _123531, _123533, _123535, _123537, _123539] : [-(lower_bound(_123537, _123533, _123529)), lower_bound(_123539, _123535, _123531), _123539 = _123537, _123535 = _123533, _123531 = _123529], (160 ^ _118591) ^ [_124138, _124140, _124142, _124144, _124146, _124148] : [-(apply(_124146, _124142, _124138)), apply(_124148, _124144, _124140), _124148 = _124146, _124144 = _124142, _124140 = _124138], (178 ^ _118591) ^ [_124719, _124721, _124723, _124725] : [-(order(_124723, _124719)), order(_124725, _124721), _124725 = _124723, _124721 = _124719], (192 ^ _118591) ^ [_125163, _125165, _125167, _125169] : [-(subset(_125167, _125163)), subset(_125169, _125165), _125169 = _125167, _125165 = _125163], (206 ^ _118591) ^ [_125635, _125637, _125639, _125641, _125643, _125645] : [-(greatest(_125643, _125639, _125635)), greatest(_125645, _125641, _125637), _125645 = _125643, _125641 = _125639, _125637 = _125635], (224 ^ _118591) ^ [_126216, _126218, _126220, _126222] : [-(member(_126220, _126216)), member(_126222, _126218), _126222 = _126220, _126218 = _126216], (238 ^ _118591) ^ [_126696, _126698, _126700, _126702, _126704, _126706, _126708, _126710] : [-(least_upper_bound(_126708, _126704, _126700, _126696)), least_upper_bound(_126710, _126706, _126702, _126698), _126710 = _126708, _126706 = _126704, _126702 = _126700, _126698 = _126696], (334 ^ _118591) ^ [_130155, _130157] : [336 ^ _118591 : [(337 ^ _118591) ^ [] : [-(member(335 ^ [_130155, _130157], _130157))], (339 ^ _118591) ^ [] : [member(335 ^ [_130155, _130157], _130155)]], -(subset(_130157, _130155))], (324 ^ _118591) ^ [_129841, _129843] : [subset(_129843, _129841), 327 ^ _118591 : [(328 ^ _118591) ^ [_129978] : [member(_129978, _129843), -(member(_129978, _129841))]]], (343 ^ _118591) ^ [_130541, _130543] : [equal_set(_130543, _130541), 346 ^ _118591 : [(347 ^ _118591) ^ [] : [-(subset(_130543, _130541))], (349 ^ _118591) ^ [] : [-(subset(_130541, _130543))]]], (351 ^ _118591) ^ [_130778, _130780] : [-(equal_set(_130780, _130778)), subset(_130780, _130778), subset(_130778, _130780)], (361 ^ _118591) ^ [_131108, _131110] : [member(_131110, power_set(_131108)), -(subset(_131110, _131108))], (367 ^ _118591) ^ [_131274, _131276] : [subset(_131276, _131274), -(member(_131276, power_set(_131274)))], (373 ^ _118591) ^ [_131533, _131535, _131537] : [member(_131537, intersection(_131535, _131533)), 376 ^ _118591 : [(377 ^ _118591) ^ [] : [-(member(_131537, _131535))], (379 ^ _118591) ^ [] : [-(member(_131537, _131533))]]], (381 ^ _118591) ^ [_131784, _131786, _131788] : [-(member(_131788, intersection(_131786, _131784))), member(_131788, _131786), member(_131788, _131784)], (401 ^ _118591) ^ [_132412, _132414, _132416] : [402 ^ _118591 : [(403 ^ _118591) ^ [] : [member(_132416, _132414)], (405 ^ _118591) ^ [] : [member(_132416, _132412)]], -(member(_132416, union(_132414, _132412)))], (391 ^ _118591) ^ [_132144, _132146, _132148] : [member(_132148, union(_132146, _132144)), -(member(_132148, _132146)), -(member(_132148, _132144))], (409 ^ _118591) ^ [_132682] : [member(_132682, empty_set)], (411 ^ _118591) ^ [_132832, _132834, _132836] : [member(_132836, difference(_132832, _132834)), 414 ^ _118591 : [(415 ^ _118591) ^ [] : [-(member(_132836, _132832))], (417 ^ _118591) ^ [] : [member(_132836, _132834)]]], (419 ^ _118591) ^ [_133084, _133086, _133088] : [-(member(_133088, difference(_133084, _133086))), member(_133088, _133084), -(member(_133088, _133086))], (429 ^ _118591) ^ [_133433, _133435] : [member(_133435, singleton(_133433)), -(_133435 = _133433)], (435 ^ _118591) ^ [_133599, _133601] : [_133601 = _133599, -(member(_133601, singleton(_133599)))], (451 ^ _118591) ^ [_134126, _134128, _134130] : [452 ^ _118591 : [(453 ^ _118591) ^ [] : [_134130 = _134128], (455 ^ _118591) ^ [] : [_134130 = _134126]], -(member(_134130, unordered_pair(_134128, _134126)))], (441 ^ _118591) ^ [_133858, _133860, _133862] : [member(_133862, unordered_pair(_133860, _133858)), -(_133862 = _133860), -(_133862 = _133858)], (459 ^ _118591) ^ [_134455, _134457] : [member(_134457, sum(_134455)), 463 ^ _118591 : [(464 ^ _118591) ^ [] : [-(member(462 ^ [_134455, _134457], _134455))], (466 ^ _118591) ^ [] : [-(member(_134457, 462 ^ [_134455, _134457]))]]], (468 ^ _118591) ^ [_134766, _134768] : [-(member(_134768, sum(_134766))), 469 ^ _118591 : [(470 ^ _118591) ^ [_134860] : [member(_134860, _134766), member(_134768, _134860)]]], (488 ^ _118591) ^ [_135461, _135463] : [490 ^ _118591 : [(491 ^ _118591) ^ [] : [-(member(489 ^ [_135461, _135463], _135461))], (493 ^ _118591) ^ [] : [member(_135463, 489 ^ [_135461, _135463])]], -(member(_135463, product(_135461)))], (478 ^ _118591) ^ [_135143, _135145] : [member(_135145, product(_135143)), 481 ^ _118591 : [(482 ^ _118591) ^ [_135284] : [member(_135284, _135143), -(member(_135145, _135284))]]], (547 ^ _118591) ^ [_137489, _137491] : [-(order(_137491, _137489)), 551 ^ _118591 : [(552 ^ _118591) ^ [] : [-(member(550 ^ [_137489, _137491], _137489))], (554 ^ _118591) ^ [] : [apply(_137491, 550 ^ [_137489, _137491], 550 ^ [_137489, _137491])]], 559 ^ _118591 : [(560 ^ _118591) ^ [] : [-(member(557 ^ [_137489, _137491], _137489))], (562 ^ _118591) ^ [] : [-(member(558 ^ [_137489, _137491], _137489))], (564 ^ _118591) ^ [] : [-(apply(_137491, 557 ^ [_137489, _137491], 558 ^ [_137489, _137491]))], (566 ^ _118591) ^ [] : [-(apply(_137491, 558 ^ [_137489, _137491], 557 ^ [_137489, _137491]))], (568 ^ _118591) ^ [] : [557 ^ [_137489, _137491] = 558 ^ [_137489, _137491]]], 572 ^ _118591 : [(573 ^ _118591) ^ [] : [-(member(569 ^ [_137489, _137491], _137489))], (575 ^ _118591) ^ [] : [-(member(570 ^ [_137489, _137491], _137489))], (577 ^ _118591) ^ [] : [-(member(571 ^ [_137489, _137491], _137489))], (579 ^ _118591) ^ [] : [-(apply(_137491, 569 ^ [_137489, _137491], 570 ^ [_137489, _137491]))], (581 ^ _118591) ^ [] : [-(apply(_137491, 570 ^ [_137489, _137491], 571 ^ [_137489, _137491]))], (583 ^ _118591) ^ [] : [apply(_137491, 569 ^ [_137489, _137491], 571 ^ [_137489, _137491])]]], (497 ^ _118591) ^ [_135889, _135891] : [order(_135891, _135889), 500 ^ _118591 : [(501 ^ _118591) ^ [_136143] : [member(_136143, _135889), -(apply(_135891, _136143, _136143))], (507 ^ _118591) ^ [_136365, _136367] : [member(_136367, _135889), member(_136365, _135889), -(_136367 = _136365), apply(_135891, _136367, _136365), apply(_135891, _136365, _136367)], (525 ^ _118591) ^ [_136882, _136884, _136886] : [member(_136886, _135889), member(_136884, _135889), member(_136882, _135889), -(apply(_135891, _136886, _136882)), apply(_135891, _136886, _136884), apply(_135891, _136884, _136882)]]], (607 ^ _118591) ^ [_140010, _140012] : [-(total_order(_140012, _140010)), order(_140012, _140010), 614 ^ _118591 : [(615 ^ _118591) ^ [] : [-(member(612 ^ [_140010, _140012], _140010))], (617 ^ _118591) ^ [] : [-(member(613 ^ [_140010, _140012], _140010))], (619 ^ _118591) ^ [] : [apply(_140012, 612 ^ [_140010, _140012], 613 ^ [_140010, _140012])], (621 ^ _118591) ^ [] : [apply(_140012, 613 ^ [_140010, _140012], 612 ^ [_140010, _140012])]]], (587 ^ _118591) ^ [_139382, _139384] : [total_order(_139384, _139382), 590 ^ _118591 : [(591 ^ _118591) ^ [] : [-(order(_139384, _139382))], (593 ^ _118591) ^ [_139624, _139626] : [member(_139626, _139382), member(_139624, _139382), -(apply(_139384, _139626, _139624)), -(apply(_139384, _139624, _139626))]]], (635 ^ _118591) ^ [_141121, _141123, _141125] : [637 ^ _118591 : [(638 ^ _118591) ^ [] : [-(member(636 ^ [_141121, _141123, _141125], _141123))], (640 ^ _118591) ^ [] : [apply(_141125, 636 ^ [_141121, _141123, _141125], _141121)]], -(upper_bound(_141121, _141125, _141123))], (625 ^ _118591) ^ [_140790, _140792, _140794] : [upper_bound(_140790, _140794, _140792), 628 ^ _118591 : [(629 ^ _118591) ^ [_140934] : [member(_140934, _140792), -(apply(_140794, _140934, _140790))]]], (654 ^ _118591) ^ [_141873, _141875, _141877] : [656 ^ _118591 : [(657 ^ _118591) ^ [] : [-(member(655 ^ [_141873, _141875, _141877], _141875))], (659 ^ _118591) ^ [] : [apply(_141877, _141873, 655 ^ [_141873, _141875, _141877])]], -(lower_bound(_141873, _141877, _141875))], (644 ^ _118591) ^ [_141542, _141544, _141546] : [lower_bound(_141542, _141546, _141544), 647 ^ _118591 : [(648 ^ _118591) ^ [_141686] : [member(_141686, _141544), -(apply(_141546, _141542, _141686))]]], (663 ^ _118591) ^ [_142294, _142296, _142298] : [greatest(_142294, _142298, _142296), 666 ^ _118591 : [(667 ^ _118591) ^ [] : [-(member(_142294, _142296))], (669 ^ _118591) ^ [_142512] : [member(_142512, _142296), -(apply(_142298, _142512, _142294))]]], (675 ^ _118591) ^ [_142701, _142703, _142705] : [-(greatest(_142701, _142705, _142703)), member(_142701, _142703), 681 ^ _118591 : [(682 ^ _118591) ^ [] : [-(member(680 ^ [_142701, _142703, _142705], _142703))], (684 ^ _118591) ^ [] : [apply(_142705, 680 ^ [_142701, _142703, _142705], _142701)]]], (688 ^ _118591) ^ [_143215, _143217, _143219] : [least(_143215, _143219, _143217), 691 ^ _118591 : [(692 ^ _118591) ^ [] : [-(member(_143215, _143217))], (694 ^ _118591) ^ [_143433] : [member(_143433, _143217), -(apply(_143219, _143215, _143433))]]], (700 ^ _118591) ^ [_143622, _143624, _143626] : [-(least(_143622, _143626, _143624)), member(_143622, _143624), 706 ^ _118591 : [(707 ^ _118591) ^ [] : [-(member(705 ^ [_143622, _143624, _143626], _143624))], (709 ^ _118591) ^ [] : [apply(_143626, _143622, 705 ^ [_143622, _143624, _143626])]]], (729 ^ _118591) ^ [_144646, _144648, _144650] : [-(max(_144646, _144650, _144648)), member(_144646, _144648), 735 ^ _118591 : [(736 ^ _118591) ^ [] : [-(member(734 ^ [_144646, _144648, _144650], _144648))], (738 ^ _118591) ^ [] : [-(apply(_144650, _144646, 734 ^ [_144646, _144648, _144650]))], (740 ^ _118591) ^ [] : [_144646 = 734 ^ [_144646, _144648, _144650]]]], (713 ^ _118591) ^ [_144136, _144138, _144140] : [max(_144136, _144140, _144138), 716 ^ _118591 : [(717 ^ _118591) ^ [] : [-(member(_144136, _144138))], (719 ^ _118591) ^ [_144360] : [-(_144136 = _144360), member(_144360, _144138), apply(_144140, _144136, _144360)]]], (760 ^ _118591) ^ [_145763, _145765, _145767] : [-(min(_145763, _145767, _145765)), member(_145763, _145765), 766 ^ _118591 : [(767 ^ _118591) ^ [] : [-(member(765 ^ [_145763, _145765, _145767], _145765))], (769 ^ _118591) ^ [] : [-(apply(_145767, 765 ^ [_145763, _145765, _145767], _145763))], (771 ^ _118591) ^ [] : [_145763 = 765 ^ [_145763, _145765, _145767]]]], (744 ^ _118591) ^ [_145253, _145255, _145257] : [min(_145253, _145257, _145255), 747 ^ _118591 : [(748 ^ _118591) ^ [] : [-(member(_145253, _145255))], (750 ^ _118591) ^ [_145477] : [-(_145253 = _145477), member(_145477, _145255), apply(_145257, _145477, _145253)]]], (775 ^ _118591) ^ [_146384, _146386, _146388, _146390] : [least_upper_bound(_146390, _146388, _146386, _146384), 778 ^ _118591 : [(779 ^ _118591) ^ [] : [-(member(_146390, _146388))], (781 ^ _118591) ^ [] : [-(upper_bound(_146390, _146386, _146388))], (783 ^ _118591) ^ [_146695] : [-(apply(_146386, _146390, _146695)), member(_146695, _146384), upper_bound(_146695, _146386, _146388)]]], (793 ^ _118591) ^ [_146997, _146999, _147001, _147003] : [-(least_upper_bound(_147003, _147001, _146999, _146997)), member(_147003, _147001), upper_bound(_147003, _146999, _147001), 803 ^ _118591 : [(804 ^ _118591) ^ [] : [-(member(802 ^ [_146997, _146999, _147001, _147003], _146997))], (806 ^ _118591) ^ [] : [-(upper_bound(802 ^ [_146997, _146999, _147001, _147003], _146999, _147001))], (808 ^ _118591) ^ [] : [apply(_146999, _147003, 802 ^ [_146997, _146999, _147001, _147003])]]], (812 ^ _118591) ^ [_147726, _147728, _147730, _147732] : [greatest_lower_bound(_147732, _147730, _147728, _147726), 815 ^ _118591 : [(816 ^ _118591) ^ [] : [-(member(_147732, _147730))], (818 ^ _118591) ^ [] : [-(lower_bound(_147732, _147728, _147730))], (820 ^ _118591) ^ [_148037] : [-(apply(_147728, _148037, _147732)), member(_148037, _147726), lower_bound(_148037, _147728, _147730)]]], (830 ^ _118591) ^ [_148339, _148341, _148343, _148345] : [-(greatest_lower_bound(_148345, _148343, _148341, _148339)), member(_148345, _148343), lower_bound(_148345, _148341, _148343), 840 ^ _118591 : [(841 ^ _118591) ^ [] : [-(member(839 ^ [_148339, _148341, _148343, _148345], _148339))], (843 ^ _118591) ^ [] : [-(lower_bound(839 ^ [_148339, _148341, _148343, _148345], _148341, _148343))], (845 ^ _118591) ^ [] : [apply(_148341, 839 ^ [_148339, _148341, _148343, _148345], _148345)]]]], input).
% 1.57/2.41 ncf('1',plain,[871 : greatest(855 ^ [], 848 ^ [], 852 ^ []), 861 : member(855 ^ [], 852 ^ []), 861 : least_upper_bound(855 ^ [], 852 ^ [], 848 ^ [], 849 ^ [])],start(857 ^ 0)).
% 1.57/2.41 ncf('1.1',plain,[-(greatest(855 ^ [], 848 ^ [], 852 ^ [])), greatest(855 ^ [], 848 ^ [], 852 ^ []), 855 ^ [] = 855 ^ [], 848 ^ [] = 848 ^ [], 852 ^ [] = 852 ^ []],extension(206 ^ 3,bind([[_125635, _125637, _125639, _125641, _125643, _125645], [852 ^ [], 852 ^ [], 848 ^ [], 848 ^ [], 855 ^ [], 855 ^ []]]))).
% 1.57/2.41 ncf('1.1.1',plain,[-(greatest(855 ^ [], 848 ^ [], 852 ^ [])), member(855 ^ [], 852 ^ []), 682 : -(member(680 ^ [855 ^ [], 852 ^ [], 848 ^ []], 852 ^ []))],extension(675 ^ 4,bind([[_142701, _142703, _142705], [855 ^ [], 852 ^ [], 848 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1',plain,[-(member(855 ^ [], 852 ^ []))],extension(867 ^ 5)).
% 1.57/2.41 ncf('1.1.1.2',plain,[member(680 ^ [855 ^ [], 852 ^ [], 848 ^ []], 852 ^ []), 629 : -(apply(848 ^ [], 680 ^ [855 ^ [], 852 ^ [], 848 ^ []], 855 ^ [])), 629 : upper_bound(855 ^ [], 848 ^ [], 852 ^ [])],extension(625 ^ 7,bind([[_140790, _140792, _140794, _140934], [855 ^ [], 852 ^ [], 848 ^ [], 680 ^ [855 ^ [], 852 ^ [], 848 ^ []]]]))).
% 1.57/2.41 ncf('1.1.1.2.1',plain,[apply(848 ^ [], 680 ^ [855 ^ [], 852 ^ [], 848 ^ []], 855 ^ [])],extension(684 ^ 10)).
% 1.57/2.41 ncf('1.1.1.2.2',plain,[-(upper_bound(855 ^ [], 848 ^ [], 852 ^ [])), least_upper_bound(855 ^ [], 852 ^ [], 848 ^ [], 849 ^ [])],extension(775 ^ 8,bind([[_146384, _146386, _146388, _146390], [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.2.1',plain,[-(least_upper_bound(855 ^ [], 852 ^ [], 848 ^ [], 849 ^ []))],extension(869 ^ 9)).
% 1.57/2.41 ncf('1.1.2',plain,[-(855 ^ [] = 855 ^ [])],extension(2 ^ 4,bind([[_118735], [855 ^ []]]))).
% 1.57/2.41 ncf('1.1.3',plain,[-(848 ^ [] = 848 ^ [])],extension(2 ^ 4,bind([[_118735], [848 ^ []]]))).
% 1.57/2.41 ncf('1.1.4',plain,[-(852 ^ [] = 852 ^ [])],extension(2 ^ 4,bind([[_118735], [852 ^ []]]))).
% 1.57/2.41 ncf('1.2',plain,[-(member(855 ^ [], 852 ^ [])), member(855 ^ [], intersection(852 ^ [], _81126))],extension(373 ^ 3,bind([[_131533, _131535, _131537], [_81126, 852 ^ [], 855 ^ []]]))).
% 1.57/2.41 ncf('1.2.1',plain,[-(member(855 ^ [], intersection(852 ^ [], _81126))), member(855 ^ [], union(intersection(852 ^ [], _81126), 852 ^ [])), -(member(855 ^ [], 852 ^ []))],extension(391 ^ 4,bind([[_132144, _132146, _132148], [852 ^ [], intersection(852 ^ [], _81126), 855 ^ []]]))).
% 1.57/2.41 ncf('1.2.1.1',plain,[-(member(855 ^ [], union(intersection(852 ^ [], _81126), 852 ^ []))), 405 : member(855 ^ [], 852 ^ [])],extension(401 ^ 5,bind([[_132412, _132414, _132416], [852 ^ [], intersection(852 ^ [], _81126), 855 ^ []]]))).
% 1.57/2.41 ncf('1.2.1.1.1',plain,[-(member(855 ^ [], 852 ^ [])), greatest(855 ^ [], 848 ^ [], 852 ^ [])],extension(663 ^ 8,bind([[_142294, _142296, _142298], [855 ^ [], 852 ^ [], 848 ^ []]]))).
% 1.57/2.41 ncf('1.2.1.1.1.1',plain,[-(greatest(855 ^ [], 848 ^ [], 852 ^ []))],extension(859 ^ 9)).
% 1.57/2.41 ncf('1.2.1.2',plain,[member(855 ^ [], 852 ^ [])],reduction('1')).
% 1.57/2.41 ncf('1.3',plain,[-(least_upper_bound(855 ^ [], 852 ^ [], 848 ^ [], 849 ^ [])), member(855 ^ [], 852 ^ []), upper_bound(855 ^ [], 848 ^ [], 852 ^ []), 806 : -(upper_bound(802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []], 848 ^ [], 852 ^ []))],extension(793 ^ 3,bind([[_146997, _146999, _147001, _147003], [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []]]))).
% 1.57/2.41 ncf('1.3.1',plain,[-(member(855 ^ [], 852 ^ []))],lemmata('x')).
% 1.57/2.41 ncf('1.3.2',plain,[-(upper_bound(855 ^ [], 848 ^ [], 852 ^ [])), 638 : -(member(636 ^ [855 ^ [], 852 ^ [], 848 ^ []], 852 ^ []))],extension(635 ^ 4,bind([[_141121, _141123, _141125], [855 ^ [], 852 ^ [], 848 ^ []]]))).
% 1.57/2.41 ncf('1.3.2.1',plain,[member(636 ^ [855 ^ [], 852 ^ [], 848 ^ []], 852 ^ []), 669 : -(apply(848 ^ [], 636 ^ [855 ^ [], 852 ^ [], 848 ^ []], 855 ^ [])), 669 : greatest(855 ^ [], 848 ^ [], 852 ^ [])],extension(663 ^ 7,bind([[_142294, _142296, _142298, _142512], [855 ^ [], 852 ^ [], 848 ^ [], 636 ^ [855 ^ [], 852 ^ [], 848 ^ []]]]))).
% 1.57/2.41 ncf('1.3.2.1.1',plain,[apply(848 ^ [], 636 ^ [855 ^ [], 852 ^ [], 848 ^ []], 855 ^ [])],extension(640 ^ 10)).
% 1.57/2.41 ncf('1.3.2.1.2',plain,[-(greatest(855 ^ [], 848 ^ [], 852 ^ []))],extension(859 ^ 8)).
% 1.57/2.41 ncf('1.3.3',plain,[upper_bound(802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []], 848 ^ [], 852 ^ []), 629 : member(855 ^ [], 852 ^ []), 629 : -(apply(848 ^ [], 855 ^ [], 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []]))],extension(625 ^ 6,bind([[_140790, _140792, _140794, _140934], [802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []], 852 ^ [], 848 ^ [], 855 ^ []]]))).
% 1.57/2.41 ncf('1.3.3.1',plain,[-(member(855 ^ [], 852 ^ [])), greatest(855 ^ [], 848 ^ [], 852 ^ [])],extension(663 ^ 9,bind([[_142294, _142296, _142298], [855 ^ [], 852 ^ [], 848 ^ []]]))).
% 1.57/2.41 ncf('1.3.3.1.1',plain,[-(greatest(855 ^ [], 848 ^ [], 852 ^ []))],extension(859 ^ 10)).
% 1.57/2.41 ncf('1.3.3.2',plain,[apply(848 ^ [], 855 ^ [], 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []]), -(apply(848 ^ [], 855 ^ [], 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []])), 848 ^ [] = 848 ^ [], 855 ^ [] = 855 ^ [], 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []] = 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []]],extension(160 ^ 9,bind([[_124138, _124140, _124142, _124144, _124146, _124148], [802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []], 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []], 855 ^ [], 855 ^ [], 848 ^ [], 848 ^ []]]))).
% 1.57/2.41 ncf('1.3.3.2.1',plain,[apply(848 ^ [], 855 ^ [], 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []])],extension(808 ^ 10)).
% 1.57/2.41 ncf('1.3.3.2.2',plain,[-(848 ^ [] = 848 ^ [])],extension(2 ^ 10,bind([[_118735], [848 ^ []]]))).
% 1.57/2.41 ncf('1.3.3.2.3',plain,[-(855 ^ [] = 855 ^ [])],extension(2 ^ 10,bind([[_118735], [855 ^ []]]))).
% 1.57/2.41 ncf('1.3.3.2.4',plain,[-(802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []] = 802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []])],extension(2 ^ 10,bind([[_118735], [802 ^ [849 ^ [], 848 ^ [], 852 ^ [], 855 ^ []]]]))).
% 1.57/2.41 %-----------------------------------------------------
% 1.57/2.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------