%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET677+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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:16 EDT 2023
% Result : Theorem 0.31s 1.35s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.10 % Problem : SET677+3 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.10 % Command : nanocop.sh %s %d
% 0.10/0.31 % Computer : n029.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Thu May 18 19:08:43 EDT 2023
% 0.10/0.32 % CPUTime :
% 0.31/1.35
% 0.31/1.35 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.31/1.35 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.35 %-----------------------------------------------------
% 0.31/1.35 ncf(matrix, plain, [(736 ^ _100995) ^ [] : [-(ilf_type(734 ^ [], set_type))], (739 ^ _100995) ^ [] : [-(ilf_type(737 ^ [], identity_relation_of_type(734 ^ [])))], (741 ^ _100995) ^ [] : [-(subset(identity_relation_of(734 ^ []), 737 ^ []))], (743 ^ _100995) ^ [] : [734 ^ [] = domain(734 ^ [], 734 ^ [], 737 ^ []), 734 ^ [] = range(734 ^ [], 734 ^ [], 737 ^ [])], (2 ^ _100995) ^ [_101139] : [-(_101139 = _101139)], (4 ^ _100995) ^ [_101246, _101248] : [_101248 = _101246, -(_101246 = _101248)], (10 ^ _100995) ^ [_101450, _101452, _101454] : [-(_101454 = _101450), _101454 = _101452, _101452 = _101450], (20 ^ _100995) ^ [_101791, _101793, _101795, _101797] : [-(member(_101795, _101791)), member(_101797, _101793), _101797 = _101795, _101793 = _101791], (34 ^ _100995) ^ [_102207, _102209] : [-(empty(_102207)), _102209 = _102207, empty(_102209)], (44 ^ _100995) ^ [_102502, _102504] : [-(relation_like(_102502)), _102504 = _102502, relation_like(_102504)], (54 ^ _100995) ^ [_102825, _102827, _102829, _102831] : [-(ilf_type(_102829, _102825)), ilf_type(_102831, _102827), _102831 = _102829, _102827 = _102825], (68 ^ _100995) ^ [_103249, _103251, _103253, _103255] : [-(subset(_103253, _103249)), subset(_103255, _103251), _103255 = _103253, _103251 = _103249], (82 ^ _100995) ^ [_103679, _103681] : [_103681 = _103679, -(power_set(_103681) = power_set(_103679))], (88 ^ _100995) ^ [_103897, _103899] : [_103899 = _103897, -(member_type(_103899) = member_type(_103897))], (94 ^ _100995) ^ [_104143, _104145, _104147, _104149] : [-(ordered_pair(_104149, _104145) = ordered_pair(_104147, _104143)), _104149 = _104147, _104145 = _104143], (104 ^ _100995) ^ [_104502, _104504, _104506, _104508] : [-(cross_product(_104508, _104504) = cross_product(_104506, _104502)), _104508 = _104506, _104504 = _104502], (114 ^ _100995) ^ [_104833, _104835] : [_104835 = _104833, -(domain_of(_104835) = domain_of(_104833))], (120 ^ _100995) ^ [_105051, _105053] : [_105053 = _105051, -(range_of(_105053) = range_of(_105051))], (126 ^ _100995) ^ [_105297, _105299, _105301, _105303] : [-(relation_type(_105303, _105299) = relation_type(_105301, _105297)), _105303 = _105301, _105299 = _105297], (136 ^ _100995) ^ [_105628, _105630] : [_105630 = _105628, -(subset_type(_105630) = subset_type(_105628))], (142 ^ _100995) ^ [_105846, _105848] : [_105848 = _105846, -(identity_relation_of_type(_105848) = identity_relation_of_type(_105846))], (148 ^ _100995) ^ [_106064, _106066] : [_106066 = _106064, -(identity_relation_of(_106066) = identity_relation_of(_106064))], (154 ^ _100995) ^ [_106338, _106340, _106342, _106344, _106346, _106348] : [-(domain(_106348, _106344, _106340) = domain(_106346, _106342, _106338)), _106348 = _106346, _106344 = _106342, _106340 = _106338], (168 ^ _100995) ^ [_106834, _106836, _106838, _106840, _106842, _106844] : [-(range(_106844, _106840, _106836) = range(_106842, _106838, _106834)), _106844 = _106842, _106840 = _106838, _106836 = _106834], (182 ^ _100995) ^ [_107318] : [ilf_type(_107318, set_type), 185 ^ _100995 : [(186 ^ _100995) ^ [_107487] : [ilf_type(_107487, set_type), 189 ^ _100995 : [(190 ^ _100995) ^ [_107651] : [ilf_type(_107651, relation_type(_107487, _107318)), subset(identity_relation_of(_107487), _107651), 197 ^ _100995 : [(198 ^ _100995) ^ [] : [-(_107487 = domain(_107487, _107318, _107651))], (200 ^ _100995) ^ [] : [-(subset(_107487, range(_107487, _107318, _107651)))]]]]]]], (202 ^ _100995) ^ [_108063] : [ilf_type(_108063, set_type), 205 ^ _100995 : [(206 ^ _100995) ^ [_108232] : [ilf_type(_108232, set_type), 209 ^ _100995 : [(210 ^ _100995) ^ [_108396] : [ilf_type(_108396, relation_type(_108063, _108232)), subset(identity_relation_of(_108232), _108396), 217 ^ _100995 : [(218 ^ _100995) ^ [] : [-(subset(_108232, domain(_108063, _108232, _108396)))], (220 ^ _100995) ^ [] : [-(_108232 = range(_108063, _108232, _108396))]]]]]]], (222 ^ _100995) ^ [_108808] : [ilf_type(_108808, set_type), 225 ^ _100995 : [(226 ^ _100995) ^ [_108969] : [ilf_type(_108969, set_type), 229 ^ _100995 : [(230 ^ _100995) ^ [_109125] : [ilf_type(_109125, set_type), 233 ^ _100995 : [(234 ^ _100995) ^ [] : [member(ordered_pair(_108969, _109125), identity_relation_of(_108808)), 237 ^ _100995 : [(238 ^ _100995) ^ [] : [-(member(_108969, _108808))], (240 ^ _100995) ^ [] : [-(_108969 = _109125)]]], (242 ^ _100995) ^ [] : [-(member(ordered_pair(_108969, _109125), identity_relation_of(_108808))), member(_108969, _108808), _108969 = _109125]]]]]]], (252 ^ _100995) ^ [_109780] : [ilf_type(_109780, set_type), -(ilf_type(identity_relation_of(_109780), binary_relation_type))], (258 ^ _100995) ^ [_109974] : [ilf_type(_109974, set_type), 261 ^ _100995 : [(262 ^ _100995) ^ [_110118] : [ilf_type(_110118, set_type), 265 ^ _100995 : [(266 ^ _100995) ^ [] : [ilf_type(_110118, identity_relation_of_type(_109974)), -(ilf_type(_110118, relation_type(_109974, _109974)))], (272 ^ _100995) ^ [] : [ilf_type(_110118, relation_type(_109974, _109974)), -(ilf_type(_110118, identity_relation_of_type(_109974)))]]]]], (278 ^ _100995) ^ [_110586] : [ilf_type(_110586, set_type), -(ilf_type(281 ^ [_110586], identity_relation_of_type(_110586)))], (285 ^ _100995) ^ [_110833] : [ilf_type(_110833, binary_relation_type), 288 ^ _100995 : [(289 ^ _100995) ^ [_111006] : [ilf_type(_111006, binary_relation_type), 292 ^ _100995 : [(311 ^ _100995) ^ [] : [313 ^ _100995 : [(314 ^ _100995) ^ [] : [-(ilf_type(312 ^ [_110833, _111006], set_type))], (317 ^ _100995) ^ [] : [-(ilf_type(315 ^ [_110833, _111006], set_type))], (319 ^ _100995) ^ [] : [-(member(ordered_pair(312 ^ [_110833, _111006], 315 ^ [_110833, _111006]), _110833))], (321 ^ _100995) ^ [] : [member(ordered_pair(312 ^ [_110833, _111006], 315 ^ [_110833, _111006]), _111006)]], -(subset(_110833, _111006))], (293 ^ _100995) ^ [] : [subset(_110833, _111006), 296 ^ _100995 : [(297 ^ _100995) ^ [_111282] : [ilf_type(_111282, set_type), 300 ^ _100995 : [(301 ^ _100995) ^ [_111439] : [ilf_type(_111439, set_type), member(ordered_pair(_111282, _111439), _110833), -(member(ordered_pair(_111282, _111439), _111006))]]]]]]]]], (325 ^ _100995) ^ [_112317] : [ilf_type(_112317, set_type), 328 ^ _100995 : [(329 ^ _100995) ^ [_112462] : [ilf_type(_112462, set_type), 332 ^ _100995 : [(333 ^ _100995) ^ [] : [_112317 = _112462, 336 ^ _100995 : [(337 ^ _100995) ^ [] : [-(subset(_112317, _112462))], (339 ^ _100995) ^ [] : [-(subset(_112462, _112317))]]], (341 ^ _100995) ^ [] : [-(_112317 = _112462), subset(_112317, _112462), subset(_112462, _112317)]]]]], (351 ^ _100995) ^ [_113073] : [ilf_type(_113073, binary_relation_type), -(ilf_type(domain_of(_113073), set_type))], (357 ^ _100995) ^ [_113267] : [ilf_type(_113267, binary_relation_type), -(ilf_type(range_of(_113267), set_type))], (363 ^ _100995) ^ [_113461] : [ilf_type(_113461, set_type), 366 ^ _100995 : [(367 ^ _100995) ^ [_113597] : [ilf_type(_113597, set_type), -(ilf_type(ordered_pair(_113461, _113597), set_type))]]], (373 ^ _100995) ^ [_113806] : [ilf_type(_113806, set_type), 376 ^ _100995 : [(377 ^ _100995) ^ [] : [ilf_type(_113806, binary_relation_type), 380 ^ _100995 : [(381 ^ _100995) ^ [] : [-(relation_like(_113806))], (383 ^ _100995) ^ [] : [-(ilf_type(_113806, set_type))]]], (385 ^ _100995) ^ [] : [-(ilf_type(_113806, binary_relation_type)), relation_like(_113806), ilf_type(_113806, set_type)]]], (396 ^ _100995) ^ [] : [-(ilf_type(394 ^ [], binary_relation_type))], (398 ^ _100995) ^ [_114475] : [ilf_type(_114475, set_type), 401 ^ _100995 : [(402 ^ _100995) ^ [_114652] : [ilf_type(_114652, set_type), 405 ^ _100995 : [(406 ^ _100995) ^ [_114844] : [ilf_type(_114844, subset_type(cross_product(_114475, _114652))), -(ilf_type(_114844, relation_type(_114475, _114652)))], (412 ^ _100995) ^ [_115046] : [ilf_type(_115046, relation_type(_114475, _114652)), -(ilf_type(_115046, subset_type(cross_product(_114475, _114652))))]]]]], (418 ^ _100995) ^ [_115280] : [ilf_type(_115280, set_type), 421 ^ _100995 : [(422 ^ _100995) ^ [_115421] : [ilf_type(_115421, set_type), -(ilf_type(425 ^ [_115280, _115421], relation_type(_115421, _115280)))]]], (429 ^ _100995) ^ [_115690] : [ilf_type(_115690, set_type), 432 ^ _100995 : [(433 ^ _100995) ^ [_115835] : [ilf_type(_115835, set_type), 436 ^ _100995 : [(437 ^ _100995) ^ [] : [ilf_type(_115835, subset_type(_115690)), -(ilf_type(_115835, member_type(power_set(_115690))))], (443 ^ _100995) ^ [] : [ilf_type(_115835, member_type(power_set(_115690))), -(ilf_type(_115835, subset_type(_115690)))]]]]], (449 ^ _100995) ^ [_116306] : [ilf_type(_116306, set_type), -(ilf_type(452 ^ [_116306], subset_type(_116306)))], (456 ^ _100995) ^ [_116553] : [ilf_type(_116553, set_type), 459 ^ _100995 : [(460 ^ _100995) ^ [_116709] : [ilf_type(_116709, set_type), 463 ^ _100995 : [(478 ^ _100995) ^ [] : [480 ^ _100995 : [(481 ^ _100995) ^ [] : [-(ilf_type(479 ^ [_116553, _116709], set_type))], (483 ^ _100995) ^ [] : [-(member(479 ^ [_116553, _116709], _116553))], (485 ^ _100995) ^ [] : [member(479 ^ [_116553, _116709], _116709)]], -(subset(_116553, _116709))], (464 ^ _100995) ^ [] : [subset(_116553, _116709), 467 ^ _100995 : [(468 ^ _100995) ^ [_116968] : [ilf_type(_116968, set_type), member(_116968, _116553), -(member(_116968, _116709))]]]]]]], (489 ^ _100995) ^ [_117628] : [ilf_type(_117628, set_type), -(subset(_117628, _117628))], (495 ^ _100995) ^ [_117818] : [ilf_type(_117818, binary_relation_type), -(subset(_117818, _117818))], (501 ^ _100995) ^ [_118008] : [ilf_type(_118008, set_type), 504 ^ _100995 : [(505 ^ _100995) ^ [_118144] : [ilf_type(_118144, set_type), -(ilf_type(cross_product(_118008, _118144), set_type))]]], (511 ^ _100995) ^ [_118353] : [ilf_type(_118353, set_type), 514 ^ _100995 : [(515 ^ _100995) ^ [_118511] : [ilf_type(_118511, set_type), 518 ^ _100995 : [(533 ^ _100995) ^ [] : [535 ^ _100995 : [(536 ^ _100995) ^ [] : [-(ilf_type(534 ^ [_118353, _118511], set_type))], (538 ^ _100995) ^ [] : [-(member(534 ^ [_118353, _118511], _118353))], (540 ^ _100995) ^ [] : [member(534 ^ [_118353, _118511], _118511)]], -(member(_118353, power_set(_118511)))], (519 ^ _100995) ^ [] : [member(_118353, power_set(_118511)), 522 ^ _100995 : [(523 ^ _100995) ^ [_118774] : [ilf_type(_118774, set_type), member(_118774, _118353), -(member(_118774, _118511))]]]]]]], (544 ^ _100995) ^ [_119436] : [ilf_type(_119436, set_type), 547 ^ _100995 : [(548 ^ _100995) ^ [] : [empty(power_set(_119436))], (550 ^ _100995) ^ [] : [-(ilf_type(power_set(_119436), set_type))]]], (552 ^ _100995) ^ [_119706] : [ilf_type(_119706, set_type), 555 ^ _100995 : [(556 ^ _100995) ^ [_119854] : [-(empty(_119854)), ilf_type(_119854, set_type), 563 ^ _100995 : [(564 ^ _100995) ^ [] : [ilf_type(_119706, member_type(_119854)), -(member(_119706, _119854))], (570 ^ _100995) ^ [] : [member(_119706, _119854), -(ilf_type(_119706, member_type(_119854)))]]]]], (576 ^ _100995) ^ [_120405] : [-(ilf_type(583 ^ [_120405], member_type(_120405))), -(empty(_120405)), ilf_type(_120405, set_type)], (587 ^ _100995) ^ [_120738] : [ilf_type(_120738, set_type), 590 ^ _100995 : [(591 ^ _100995) ^ [] : [relation_like(_120738), 594 ^ _100995 : [(595 ^ _100995) ^ [_121010] : [ilf_type(_121010, set_type), member(_121010, _120738), 603 ^ _100995 : [(604 ^ _100995) ^ [] : [-(ilf_type(602 ^ [_120738, _121010], set_type))], (607 ^ _100995) ^ [] : [-(ilf_type(605 ^ [_120738, _121010], set_type))], (609 ^ _100995) ^ [] : [-(_121010 = ordered_pair(602 ^ [_120738, _121010], 605 ^ [_120738, _121010]))]]]]], (611 ^ _100995) ^ [] : [-(relation_like(_120738)), 613 ^ _100995 : [(614 ^ _100995) ^ [] : [-(ilf_type(612 ^ [_120738], set_type))], (616 ^ _100995) ^ [] : [-(member(612 ^ [_120738], _120738))], (618 ^ _100995) ^ [_121849] : [ilf_type(_121849, set_type), 621 ^ _100995 : [(622 ^ _100995) ^ [_121996] : [ilf_type(_121996, set_type), 612 ^ [_120738] = ordered_pair(_121849, _121996)]]]]]]], (630 ^ _100995) ^ [_122281] : [ilf_type(_122281, set_type), 633 ^ _100995 : [(634 ^ _100995) ^ [_122429] : [ilf_type(_122429, set_type), 637 ^ _100995 : [(638 ^ _100995) ^ [_122572] : [ilf_type(_122572, subset_type(cross_product(_122281, _122429))), -(relation_like(_122572))]]]]], (644 ^ _100995) ^ [_122796] : [ilf_type(_122796, set_type), 647 ^ _100995 : [(658 ^ _100995) ^ [] : [660 ^ _100995 : [(661 ^ _100995) ^ [] : [-(ilf_type(659 ^ [_122796], set_type))], (663 ^ _100995) ^ [] : [-(member(659 ^ [_122796], _122796))]], -(empty(_122796))], (648 ^ _100995) ^ [] : [empty(_122796), 651 ^ _100995 : [(652 ^ _100995) ^ [_123039] : [ilf_type(_123039, set_type), member(_123039, _122796)]]]]], (667 ^ _100995) ^ [_123499] : [-(relation_like(_123499)), empty(_123499), ilf_type(_123499, set_type)], (677 ^ _100995) ^ [_123770] : [ilf_type(_123770, set_type), 680 ^ _100995 : [(681 ^ _100995) ^ [_123923] : [ilf_type(_123923, set_type), 684 ^ _100995 : [(685 ^ _100995) ^ [_124071] : [ilf_type(_124071, relation_type(_123770, _123923)), -(domain(_123770, _123923, _124071) = domain_of(_124071))]]]]], (691 ^ _100995) ^ [_124305] : [ilf_type(_124305, set_type), 694 ^ _100995 : [(695 ^ _100995) ^ [_124458] : [ilf_type(_124458, set_type), 698 ^ _100995 : [(699 ^ _100995) ^ [_124606] : [ilf_type(_124606, relation_type(_124305, _124458)), -(ilf_type(domain(_124305, _124458, _124606), subset_type(_124305)))]]]]], (705 ^ _100995) ^ [_124840] : [ilf_type(_124840, set_type), 708 ^ _100995 : [(709 ^ _100995) ^ [_124993] : [ilf_type(_124993, set_type), 712 ^ _100995 : [(713 ^ _100995) ^ [_125141] : [ilf_type(_125141, relation_type(_124840, _124993)), -(range(_124840, _124993, _125141) = range_of(_125141))]]]]], (733 ^ _100995) ^ [_125875] : [-(ilf_type(_125875, set_type))], (719 ^ _100995) ^ [_125375] : [ilf_type(_125375, set_type), 722 ^ _100995 : [(723 ^ _100995) ^ [_125528] : [ilf_type(_125528, set_type), 726 ^ _100995 : [(727 ^ _100995) ^ [_125676] : [ilf_type(_125676, relation_type(_125375, _125528)), -(ilf_type(range(_125375, _125528, _125676), subset_type(_125528)))]]]]]], input).
% 0.31/1.35 ncf('1',plain,[734 ^ [] = domain(734 ^ [], 734 ^ [], 737 ^ []), 734 ^ [] = range(734 ^ [], 734 ^ [], 737 ^ [])],start(743 ^ 0)).
% 0.31/1.35 ncf('1.1',plain,[-(734 ^ [] = domain(734 ^ [], 734 ^ [], 737 ^ [])), 190 : ilf_type(737 ^ [], relation_type(734 ^ [], 734 ^ [])), 190 : subset(identity_relation_of(734 ^ []), 737 ^ []), 190 : ilf_type(734 ^ [], set_type), 186 : ilf_type(734 ^ [], set_type)],extension(182 ^ 1,bind([[_107318, _107487, _107651], [734 ^ [], 734 ^ [], 737 ^ []]]))).
% 0.31/1.35 ncf('1.1.1',plain,[-(ilf_type(737 ^ [], relation_type(734 ^ [], 734 ^ []))), 266 : ilf_type(737 ^ [], identity_relation_of_type(734 ^ [])), 266 : ilf_type(737 ^ [], set_type), 262 : ilf_type(734 ^ [], set_type)],extension(258 ^ 6,bind([[_109974, _110118], [734 ^ [], 737 ^ []]]))).
% 0.31/1.35 ncf('1.1.1.1',plain,[-(ilf_type(737 ^ [], identity_relation_of_type(734 ^ [])))],extension(739 ^ 11)).
% 0.31/1.35 ncf('1.1.1.2',plain,[-(ilf_type(737 ^ [], set_type))],extension(733 ^ 9,bind([[_125875], [737 ^ []]]))).
% 0.31/1.35 ncf('1.1.1.3',plain,[-(ilf_type(734 ^ [], set_type))],extension(736 ^ 7)).
% 0.31/1.35 ncf('1.1.2',plain,[-(subset(identity_relation_of(734 ^ []), 737 ^ []))],extension(741 ^ 6)).
% 0.31/1.35 ncf('1.1.3',plain,[-(ilf_type(734 ^ [], set_type))],extension(736 ^ 4)).
% 0.31/1.35 ncf('1.1.4',plain,[-(ilf_type(734 ^ [], set_type))],extension(736 ^ 2)).
% 0.31/1.35 ncf('1.2',plain,[-(734 ^ [] = range(734 ^ [], 734 ^ [], 737 ^ [])), 210 : ilf_type(737 ^ [], relation_type(734 ^ [], 734 ^ [])), 210 : subset(identity_relation_of(734 ^ []), 737 ^ []), 210 : ilf_type(734 ^ [], set_type), 206 : ilf_type(734 ^ [], set_type)],extension(202 ^ 1,bind([[_108063, _108232, _108396], [734 ^ [], 734 ^ [], 737 ^ []]]))).
% 0.31/1.35 ncf('1.2.1',plain,[-(ilf_type(737 ^ [], relation_type(734 ^ [], 734 ^ []))), 266 : ilf_type(737 ^ [], identity_relation_of_type(734 ^ [])), 266 : ilf_type(737 ^ [], set_type), 262 : ilf_type(734 ^ [], set_type)],extension(258 ^ 6,bind([[_109974, _110118], [734 ^ [], 737 ^ []]]))).
% 0.31/1.35 ncf('1.2.1.1',plain,[-(ilf_type(737 ^ [], identity_relation_of_type(734 ^ [])))],extension(739 ^ 11)).
% 0.31/1.35 ncf('1.2.1.2',plain,[-(ilf_type(737 ^ [], set_type))],extension(733 ^ 9,bind([[_125875], [737 ^ []]]))).
% 0.31/1.35 ncf('1.2.1.3',plain,[-(ilf_type(734 ^ [], set_type))],extension(736 ^ 7)).
% 0.31/1.35 ncf('1.2.2',plain,[-(subset(identity_relation_of(734 ^ []), 737 ^ []))],extension(741 ^ 6)).
% 0.31/1.35 ncf('1.2.3',plain,[-(ilf_type(734 ^ [], set_type))],extension(736 ^ 4)).
% 0.31/1.35 ncf('1.2.4',plain,[-(ilf_type(734 ^ [], set_type))],extension(736 ^ 2)).
% 0.31/1.35 %-----------------------------------------------------
% 0.31/1.35 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------