%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR022+1 : TPTP v8.1.2. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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 10:23:52 EDT 2023
% Result : Theorem 101.55s 98.67s
% Output : Proof 101.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : CSR022+1 : TPTP v8.1.2. Bugfixed v3.1.0.
% 0.04/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.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 : Fri May 19 00:13:50 EDT 2023
% 0.12/0.33 % CPUTime :
% 101.55/98.67
% 101.55/98.67 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 101.55/98.67 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.55/98.67 %-----------------------------------------------------
% 101.55/98.67 ncf(matrix, plain, [(862 ^ _113182) ^ [] : [-(holdsAt(forwards, n3))], (224 ^ _113182) ^ [_120811, _120813, _120815, _120817] : [-(plus(_120817, _120813) = plus(_120815, _120811)), _120817 = _120815, _120813 = _120811], (2 ^ _113182) ^ [_113326] : [-(_113326 = _113326)], (4 ^ _113182) ^ [_113433, _113435] : [_113435 = _113433, -(_113433 = _113435)], (10 ^ _113182) ^ [_113637, _113639, _113641] : [-(_113641 = _113637), _113641 = _113639, _113639 = _113637], (20 ^ _113182) ^ [_114034, _114036, _114038, _114040, _114042, _114044, _114046, _114048] : [-(trajectory(_114046, _114042, _114038, _114034)), trajectory(_114048, _114044, _114040, _114036), _114048 = _114046, _114044 = _114042, _114040 = _114038, _114036 = _114034], (42 ^ _113182) ^ [_114796, _114798, _114800, _114802, _114804, _114806] : [-(stoppedIn(_114804, _114800, _114796)), stoppedIn(_114806, _114802, _114798), _114806 = _114804, _114802 = _114800, _114798 = _114796], (60 ^ _113182) ^ [_115433, _115435, _115437, _115439, _115441, _115443, _115445, _115447] : [-(antitrajectory(_115445, _115441, _115437, _115433)), antitrajectory(_115447, _115443, _115439, _115435), _115447 = _115445, _115443 = _115441, _115439 = _115437, _115435 = _115433], (82 ^ _113182) ^ [_116195, _116197, _116199, _116201, _116203, _116205] : [-(startedIn(_116203, _116199, _116195)), startedIn(_116205, _116201, _116197), _116205 = _116203, _116201 = _116199, _116197 = _116195], (100 ^ _113182) ^ [_116804, _116806, _116808, _116810, _116812, _116814] : [-(initiates(_116812, _116808, _116804)), initiates(_116814, _116810, _116806), _116814 = _116812, _116810 = _116808, _116806 = _116804], (118 ^ _113182) ^ [_117413, _117415, _117417, _117419, _117421, _117423] : [-(terminates(_117421, _117417, _117413)), terminates(_117423, _117419, _117415), _117423 = _117421, _117419 = _117417, _117415 = _117413], (136 ^ _113182) ^ [_118022, _118024, _118026, _118028, _118030, _118032] : [-(releases(_118030, _118026, _118022)), releases(_118032, _118028, _118024), _118032 = _118030, _118028 = _118026, _118024 = _118022], (154 ^ _113182) ^ [_118603, _118605, _118607, _118609] : [-(happens(_118607, _118603)), happens(_118609, _118605), _118609 = _118607, _118605 = _118603], (168 ^ _113182) ^ [_119047, _119049, _119051, _119053] : [-(less_or_equal(_119051, _119047)), less_or_equal(_119053, _119049), _119053 = _119051, _119049 = _119047], (182 ^ _113182) ^ [_119491, _119493, _119495, _119497] : [-(less(_119495, _119491)), less(_119497, _119493), _119497 = _119495, _119493 = _119491], (196 ^ _113182) ^ [_119935, _119937, _119939, _119941] : [-(releasedAt(_119939, _119935)), releasedAt(_119941, _119937), _119941 = _119939, _119937 = _119935], (210 ^ _113182) ^ [_120359, _120361, _120363, _120365] : [-(holdsAt(_120363, _120359)), holdsAt(_120365, _120361), _120365 = _120363, _120361 = _120359], (234 ^ _113182) ^ [_121207, _121209, _121211] : [stoppedIn(_121211, _121209, _121207), 239 ^ _113182 : [(240 ^ _113182) ^ [] : [-(happens(237 ^ [_121207, _121209, _121211], 238 ^ [_121207, _121209, _121211]))], (242 ^ _113182) ^ [] : [-(less(_121211, 238 ^ [_121207, _121209, _121211]))], (244 ^ _113182) ^ [] : [-(less(238 ^ [_121207, _121209, _121211], _121207))], (246 ^ _113182) ^ [] : [-(terminates(237 ^ [_121207, _121209, _121211], _121209, 238 ^ [_121207, _121209, _121211]))]]], (248 ^ _113182) ^ [_121831, _121833, _121835] : [-(stoppedIn(_121835, _121833, _121831)), 249 ^ _113182 : [(250 ^ _113182) ^ [_121958, _121960] : [happens(_121960, _121958), less(_121835, _121958), less(_121958, _121831), terminates(_121960, _121833, _121958)]]], (266 ^ _113182) ^ [_122494, _122496, _122498] : [startedIn(_122498, _122494, _122496), 271 ^ _113182 : [(272 ^ _113182) ^ [] : [-(happens(269 ^ [_122494, _122496, _122498], 270 ^ [_122494, _122496, _122498]))], (274 ^ _113182) ^ [] : [-(less(_122498, 270 ^ [_122494, _122496, _122498]))], (276 ^ _113182) ^ [] : [-(less(270 ^ [_122494, _122496, _122498], _122496))], (278 ^ _113182) ^ [] : [-(initiates(269 ^ [_122494, _122496, _122498], _122494, 270 ^ [_122494, _122496, _122498]))]]], (280 ^ _113182) ^ [_123118, _123120, _123122] : [-(startedIn(_123122, _123118, _123120)), 281 ^ _113182 : [(282 ^ _113182) ^ [_123245, _123247] : [happens(_123247, _123245), less(_123122, _123245), less(_123245, _123120), initiates(_123247, _123118, _123245)]]], (298 ^ _113182) ^ [_123780, _123782, _123784, _123786, _123788] : [-(holdsAt(_123782, plus(_123786, _123780))), happens(_123788, _123786), initiates(_123788, _123784, _123786), less(n0, _123780), trajectory(_123784, _123786, _123782, _123780), -(stoppedIn(_123786, _123784, plus(_123786, _123780)))], (320 ^ _113182) ^ [_124477, _124479, _124481, _124483, _124485] : [-(holdsAt(_124477, plus(_124483, _124479))), happens(_124485, _124483), terminates(_124485, _124481, _124483), less(n0, _124479), antitrajectory(_124481, _124483, _124477, _124479), -(startedIn(_124483, _124481, plus(_124483, _124479)))], (342 ^ _113182) ^ [_125132, _125134] : [-(holdsAt(_125134, plus(_125132, n1))), holdsAt(_125134, _125132), -(releasedAt(_125134, plus(_125132, n1))), 352 ^ _113182 : [(353 ^ _113182) ^ [] : [-(happens(351 ^ [_125132, _125134], _125132))], (355 ^ _113182) ^ [] : [-(terminates(351 ^ [_125132, _125134], _125134, _125132))]]], (359 ^ _113182) ^ [_125686, _125688] : [holdsAt(_125688, plus(_125686, n1)), -(holdsAt(_125688, _125686)), -(releasedAt(_125688, plus(_125686, n1))), 369 ^ _113182 : [(370 ^ _113182) ^ [] : [-(happens(368 ^ [_125686, _125688], _125686))], (372 ^ _113182) ^ [] : [-(initiates(368 ^ [_125686, _125688], _125688, _125686))]]], (376 ^ _113182) ^ [_126244, _126246] : [-(releasedAt(_126246, plus(_126244, n1))), releasedAt(_126246, _126244), 382 ^ _113182 : [(383 ^ _113182) ^ [] : [-(happens(381 ^ [_126244, _126246], _126244))], (385 ^ _113182) ^ [] : [-(initiates(381 ^ [_126244, _126246], _126246, _126244)), -(terminates(381 ^ [_126244, _126246], _126246, _126244))]]], (393 ^ _113182) ^ [_126806, _126808] : [releasedAt(_126808, plus(_126806, n1)), -(releasedAt(_126808, _126806)), 399 ^ _113182 : [(400 ^ _113182) ^ [] : [-(happens(398 ^ [_126806, _126808], _126806))], (402 ^ _113182) ^ [] : [-(releases(398 ^ [_126806, _126808], _126808, _126806))]]], (406 ^ _113182) ^ [_127280, _127282, _127284] : [-(holdsAt(_127280, plus(_127282, n1))), happens(_127284, _127282), initiates(_127284, _127280, _127282)], (416 ^ _113182) ^ [_127611, _127613, _127615] : [holdsAt(_127611, plus(_127613, n1)), happens(_127615, _127613), terminates(_127615, _127611, _127613)], (426 ^ _113182) ^ [_127943, _127945, _127947] : [-(releasedAt(_127943, plus(_127945, n1))), happens(_127947, _127945), releases(_127947, _127943, _127945)], (436 ^ _113182) ^ [_128254, _128256, _128258] : [releasedAt(_128254, plus(_128256, n1)), happens(_128258, _128256), 441 ^ _113182 : [(442 ^ _113182) ^ [] : [initiates(_128258, _128254, _128256)], (444 ^ _113182) ^ [] : [terminates(_128258, _128254, _128256)]]], (686 ^ _113182) ^ [] : [-(plus(n0, n0) = n0)], (688 ^ _113182) ^ [] : [-(plus(n0, n1) = n1)], (690 ^ _113182) ^ [] : [-(plus(n0, n2) = n2)], (692 ^ _113182) ^ [] : [-(plus(n0, n3) = n3)], (694 ^ _113182) ^ [] : [-(plus(n1, n1) = n2)], (696 ^ _113182) ^ [] : [-(plus(n1, n2) = n3)], (698 ^ _113182) ^ [] : [-(plus(n1, n3) = n4)], (700 ^ _113182) ^ [] : [-(plus(n2, n2) = n4)], (702 ^ _113182) ^ [] : [-(plus(n2, n3) = n5)], (704 ^ _113182) ^ [] : [-(plus(n3, n3) = n6)], (706 ^ _113182) ^ [_136218, _136220] : [-(plus(_136220, _136218) = plus(_136218, _136220))], (718 ^ _113182) ^ [_136614, _136616] : [719 ^ _113182 : [(720 ^ _113182) ^ [] : [less(_136616, _136614)], (722 ^ _113182) ^ [] : [_136616 = _136614]], -(less_or_equal(_136616, _136614))], (708 ^ _113182) ^ [_136362, _136364] : [less_or_equal(_136364, _136362), -(less(_136364, _136362)), -(_136364 = _136362)], (726 ^ _113182) ^ [_136870] : [less(_136870, n0)], (728 ^ _113182) ^ [_136992] : [less(_136992, n1), -(less_or_equal(_136992, n0))], (734 ^ _113182) ^ [_137148] : [less_or_equal(_137148, n0), -(less(_137148, n1))], (740 ^ _113182) ^ [_137369] : [less(_137369, n2), -(less_or_equal(_137369, n1))], (746 ^ _113182) ^ [_137525] : [less_or_equal(_137525, n1), -(less(_137525, n2))], (752 ^ _113182) ^ [_137746] : [less(_137746, n3), -(less_or_equal(_137746, n2))], (758 ^ _113182) ^ [_137902] : [less_or_equal(_137902, n2), -(less(_137902, n3))], (764 ^ _113182) ^ [_138123] : [less(_138123, n4), -(less_or_equal(_138123, n3))], (770 ^ _113182) ^ [_138279] : [less_or_equal(_138279, n3), -(less(_138279, n4))], (776 ^ _113182) ^ [_138500] : [less(_138500, n5), -(less_or_equal(_138500, n4))], (782 ^ _113182) ^ [_138656] : [less_or_equal(_138656, n4), -(less(_138656, n5))], (788 ^ _113182) ^ [_138877] : [less(_138877, n6), -(less_or_equal(_138877, n5))], (794 ^ _113182) ^ [_139033] : [less_or_equal(_139033, n5), -(less(_139033, n6))], (800 ^ _113182) ^ [_139254] : [less(_139254, n7), -(less_or_equal(_139254, n6))], (806 ^ _113182) ^ [_139410] : [less_or_equal(_139410, n6), -(less(_139410, n7))], (812 ^ _113182) ^ [_139631] : [less(_139631, n8), -(less_or_equal(_139631, n7))], (818 ^ _113182) ^ [_139787] : [less_or_equal(_139787, n7), -(less(_139787, n8))], (824 ^ _113182) ^ [_140008] : [less(_140008, n9), -(less_or_equal(_140008, n8))], (830 ^ _113182) ^ [_140164] : [less_or_equal(_140164, n8), -(less(_140164, n9))], (854 ^ _113182) ^ [] : [holdsAt(forwards, n0)], (856 ^ _113182) ^ [] : [holdsAt(backwards, n0)], (858 ^ _113182) ^ [] : [holdsAt(spinning, n0)], (860 ^ _113182) ^ [_141065, _141067] : [releasedAt(_141067, _141065)], (836 ^ _113182) ^ [_140399, _140401] : [less(_140401, _140399), 839 ^ _113182 : [(840 ^ _113182) ^ [] : [less(_140399, _140401)], (842 ^ _113182) ^ [] : [_140399 = _140401]]], (844 ^ _113182) ^ [_140638, _140640] : [-(less(_140640, _140638)), -(less(_140638, _140640)), -(_140638 = _140640)], (448 ^ _113182) ^ [_128739, _128741, _128743] : [initiates(_128743, _128741, _128739), 453 ^ _113182 : [(454 ^ _113182) ^ [] : [-(_128743 = push)], (456 ^ _113182) ^ [] : [-(_128741 = forwards)], (458 ^ _113182) ^ [] : [happens(pull, _128739)]], 461 ^ _113182 : [(462 ^ _113182) ^ [] : [-(_128743 = pull)], (464 ^ _113182) ^ [] : [-(_128741 = backwards)], (466 ^ _113182) ^ [] : [happens(push, _128739)]], 467 ^ _113182 : [(468 ^ _113182) ^ [] : [-(_128743 = pull)], (470 ^ _113182) ^ [] : [-(_128741 = spinning)], (472 ^ _113182) ^ [] : [-(happens(push, _128739))]]], (474 ^ _113182) ^ [_129558, _129560, _129562] : [-(initiates(_129562, _129560, _129558)), 475 ^ _113182 : [(476 ^ _113182) ^ [] : [_129562 = push, _129560 = forwards, -(happens(pull, _129558))], (486 ^ _113182) ^ [] : [_129562 = pull, _129560 = backwards, -(happens(push, _129558))], (496 ^ _113182) ^ [] : [_129562 = pull, _129560 = spinning, happens(push, _129558)]]], (622 ^ _113182) ^ [_133820, _133822, _133824] : [releases(_133824, _133822, _133820)], (678 ^ _113182) ^ [] : [push = pull], (680 ^ _113182) ^ [] : [forwards = backwards], (682 ^ _113182) ^ [] : [forwards = spinning], (684 ^ _113182) ^ [] : [spinning = backwards], (624 ^ _113182) ^ [_133961, _133963] : [happens(_133963, _133961), 629 ^ _113182 : [(630 ^ _113182) ^ [] : [-(_133963 = push)], (632 ^ _113182) ^ [] : [-(_133961 = n0)]], 635 ^ _113182 : [(636 ^ _113182) ^ [] : [-(_133963 = pull)], (638 ^ _113182) ^ [] : [-(_133961 = n1)]], 641 ^ _113182 : [(642 ^ _113182) ^ [] : [-(_133963 = pull)], (644 ^ _113182) ^ [] : [-(_133961 = n2)]], 645 ^ _113182 : [(646 ^ _113182) ^ [] : [-(_133963 = push)], (648 ^ _113182) ^ [] : [-(_133961 = n2)]]], (650 ^ _113182) ^ [_134693, _134695] : [-(happens(_134695, _134693)), 651 ^ _113182 : [(652 ^ _113182) ^ [] : [_134695 = push, _134693 = n0], (658 ^ _113182) ^ [] : [_134695 = pull, _134693 = n1], (664 ^ _113182) ^ [] : [_134695 = pull, _134693 = n2], (670 ^ _113182) ^ [] : [_134695 = push, _134693 = n2]]], (508 ^ _113182) ^ [_130536, _130538, _130540] : [terminates(_130540, _130538, _130536), 513 ^ _113182 : [(514 ^ _113182) ^ [] : [-(_130540 = push)], (516 ^ _113182) ^ [] : [-(_130538 = backwards)], (518 ^ _113182) ^ [] : [happens(pull, _130536)]], 521 ^ _113182 : [(522 ^ _113182) ^ [] : [-(_130540 = pull)], (524 ^ _113182) ^ [] : [-(_130538 = forwards)], (526 ^ _113182) ^ [] : [happens(push, _130536)]], 529 ^ _113182 : [(530 ^ _113182) ^ [] : [-(_130540 = pull)], (532 ^ _113182) ^ [] : [-(_130538 = forwards)], (534 ^ _113182) ^ [] : [-(happens(push, _130536))]], 537 ^ _113182 : [(538 ^ _113182) ^ [] : [-(_130540 = pull)], (540 ^ _113182) ^ [] : [-(_130538 = backwards)], (542 ^ _113182) ^ [] : [-(happens(push, _130536))]], 545 ^ _113182 : [(546 ^ _113182) ^ [] : [-(_130540 = push)], (548 ^ _113182) ^ [] : [-(_130538 = spinning)], (550 ^ _113182) ^ [] : [happens(pull, _130536)]], 551 ^ _113182 : [(552 ^ _113182) ^ [] : [-(_130540 = pull)], (554 ^ _113182) ^ [] : [-(_130538 = spinning)], (556 ^ _113182) ^ [] : [happens(push, _130536)]]], (558 ^ _113182) ^ [_132098, _132100, _132102] : [-(terminates(_132102, _132100, _132098)), 559 ^ _113182 : [(560 ^ _113182) ^ [] : [_132102 = push, _132100 = backwards, -(happens(pull, _132098))], (570 ^ _113182) ^ [] : [_132102 = pull, _132100 = forwards, -(happens(push, _132098))], (580 ^ _113182) ^ [] : [_132102 = pull, _132100 = forwards, happens(push, _132098)], (590 ^ _113182) ^ [] : [_132102 = pull, _132100 = backwards, happens(push, _132098)], (600 ^ _113182) ^ [] : [_132102 = push, _132100 = spinning, -(happens(pull, _132098))], (610 ^ _113182) ^ [] : [_132102 = pull, _132100 = spinning, -(happens(push, _132098))]]]], input).
% 101.55/98.67 ncf('1',plain,[holdsAt(forwards, plus(n2, n1)), happens(pull, n2), terminates(pull, forwards, n2)],start(416 ^ 0,bind([[_127611, _127613, _127615], [forwards, n2, pull]]))).
% 101.55/98.67 ncf('1.1',plain,[-(holdsAt(forwards, plus(n2, n1))), holdsAt(forwards, n3), forwards = forwards, n3 = plus(n2, n1)],extension(210 ^ 1,bind([[_120359, _120361, _120363, _120365], [plus(n2, n1), n3, forwards, forwards]]))).
% 101.55/98.67 ncf('1.1.1',plain,[-(holdsAt(forwards, n3))],extension(862 ^ 2)).
% 101.55/98.67 ncf('1.1.2',plain,[-(forwards = forwards)],extension(2 ^ 2,bind([[_113326], [forwards]]))).
% 101.55/98.67 ncf('1.1.3',plain,[-(n3 = plus(n2, n1)), n3 = plus(n1, n2), plus(n1, n2) = plus(n2, n1)],extension(10 ^ 2,bind([[_113637, _113639, _113641], [plus(n2, n1), plus(n1, n2), n3]]))).
% 101.55/98.67 ncf('1.1.3.1',plain,[-(n3 = plus(n1, n2)), plus(n1, n2) = n3],extension(4 ^ 3,bind([[_113433, _113435], [n3, plus(n1, n2)]]))).
% 101.55/98.67 ncf('1.1.3.1.1',plain,[-(plus(n1, n2) = n3)],extension(696 ^ 4)).
% 101.55/98.67 ncf('1.1.3.2',plain,[-(plus(n1, n2) = plus(n2, n1))],extension(706 ^ 3,bind([[_136218, _136220], [n2, n1]]))).
% 101.55/98.67 ncf('1.2',plain,[-(happens(pull, n2)), happens(pull, n2), pull = pull, n2 = n2],extension(154 ^ 1,bind([[_118603, _118605, _118607, _118609], [n2, n2, pull, pull]]))).
% 101.55/98.67 ncf('1.2.1',plain,[-(happens(pull, n2)), 664 : pull = pull, 664 : n2 = n2],extension(650 ^ 2,bind([[_134693, _134695], [n2, pull]]))).
% 101.55/98.67 ncf('1.2.1.1',plain,[-(pull = pull)],extension(2 ^ 5,bind([[_113326], [pull]]))).
% 101.55/98.67 ncf('1.2.1.2',plain,[-(n2 = n2)],extension(2 ^ 5,bind([[_113326], [n2]]))).
% 101.55/98.67 ncf('1.2.2',plain,[-(pull = pull)],extension(2 ^ 2,bind([[_113326], [pull]]))).
% 101.55/98.67 ncf('1.2.3',plain,[-(n2 = n2)],extension(2 ^ 2,bind([[_113326], [n2]]))).
% 101.55/98.67 ncf('1.3',plain,[-(terminates(pull, forwards, n2)), terminates(pull, forwards, n2), pull = pull, forwards = forwards, n2 = n2],extension(118 ^ 1,bind([[_117413, _117415, _117417, _117419, _117421, _117423], [n2, n2, forwards, forwards, pull, pull]]))).
% 101.55/98.67 ncf('1.3.1',plain,[-(terminates(pull, forwards, n2)), 570 : pull = pull, 570 : forwards = forwards, 570 : -(happens(push, n2))],extension(558 ^ 2,bind([[_132098, _132100, _132102], [n2, forwards, pull]]))).
% 101.55/98.67 ncf('1.3.1.1',plain,[-(pull = pull)],extension(2 ^ 5,bind([[_113326], [pull]]))).
% 101.55/98.67 ncf('1.3.1.2',plain,[-(forwards = forwards)],extension(2 ^ 5,bind([[_113326], [forwards]]))).
% 101.55/98.67 ncf('1.3.1.3',plain,[happens(push, n2), pull = pull, forwards = forwards],extension(580 ^ 5)).
% 101.55/98.67 ncf('1.3.1.3.1',plain,[-(pull = pull)],lemmata('[3, 1].x')).
% 101.55/98.67 ncf('1.3.1.3.2',plain,[-(forwards = forwards)],lemmata('[3, 1].x')).
% 101.55/98.67 ncf('1.3.2',plain,[-(pull = pull)],extension(2 ^ 2,bind([[_113326], [pull]]))).
% 101.55/98.67 ncf('1.3.3',plain,[-(forwards = forwards)],extension(2 ^ 2,bind([[_113326], [forwards]]))).
% 101.55/98.67 ncf('1.3.4',plain,[-(n2 = n2)],extension(2 ^ 2,bind([[_113326], [n2]]))).
% 101.55/98.67 %-----------------------------------------------------
% 101.55/98.67 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------