%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR021+1 : TPTP v8.1.2. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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 102.17s 98.89s
% Output : Proof 102.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR021+1 : TPTP v8.1.2. Bugfixed v3.1.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n015.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 : Fri May 19 00:16:52 EDT 2023
% 0.13/0.34 % CPUTime :
% 102.17/98.89
% 102.17/98.89 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 102.17/98.89 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 102.17/98.89 %-----------------------------------------------------
% 102.17/98.89 ncf(matrix, plain, [(862 ^ _112771) ^ [] : [-(holdsAt(backwards, n3))], (224 ^ _112771) ^ [_120400, _120402, _120404, _120406] : [-(plus(_120406, _120402) = plus(_120404, _120400)), _120406 = _120404, _120402 = _120400], (2 ^ _112771) ^ [_112915] : [-(_112915 = _112915)], (4 ^ _112771) ^ [_113022, _113024] : [_113024 = _113022, -(_113022 = _113024)], (10 ^ _112771) ^ [_113226, _113228, _113230] : [-(_113230 = _113226), _113230 = _113228, _113228 = _113226], (20 ^ _112771) ^ [_113623, _113625, _113627, _113629, _113631, _113633, _113635, _113637] : [-(trajectory(_113635, _113631, _113627, _113623)), trajectory(_113637, _113633, _113629, _113625), _113637 = _113635, _113633 = _113631, _113629 = _113627, _113625 = _113623], (42 ^ _112771) ^ [_114385, _114387, _114389, _114391, _114393, _114395] : [-(stoppedIn(_114393, _114389, _114385)), stoppedIn(_114395, _114391, _114387), _114395 = _114393, _114391 = _114389, _114387 = _114385], (60 ^ _112771) ^ [_115022, _115024, _115026, _115028, _115030, _115032, _115034, _115036] : [-(antitrajectory(_115034, _115030, _115026, _115022)), antitrajectory(_115036, _115032, _115028, _115024), _115036 = _115034, _115032 = _115030, _115028 = _115026, _115024 = _115022], (82 ^ _112771) ^ [_115784, _115786, _115788, _115790, _115792, _115794] : [-(startedIn(_115792, _115788, _115784)), startedIn(_115794, _115790, _115786), _115794 = _115792, _115790 = _115788, _115786 = _115784], (100 ^ _112771) ^ [_116393, _116395, _116397, _116399, _116401, _116403] : [-(initiates(_116401, _116397, _116393)), initiates(_116403, _116399, _116395), _116403 = _116401, _116399 = _116397, _116395 = _116393], (118 ^ _112771) ^ [_117002, _117004, _117006, _117008, _117010, _117012] : [-(terminates(_117010, _117006, _117002)), terminates(_117012, _117008, _117004), _117012 = _117010, _117008 = _117006, _117004 = _117002], (136 ^ _112771) ^ [_117611, _117613, _117615, _117617, _117619, _117621] : [-(releases(_117619, _117615, _117611)), releases(_117621, _117617, _117613), _117621 = _117619, _117617 = _117615, _117613 = _117611], (154 ^ _112771) ^ [_118192, _118194, _118196, _118198] : [-(happens(_118196, _118192)), happens(_118198, _118194), _118198 = _118196, _118194 = _118192], (168 ^ _112771) ^ [_118636, _118638, _118640, _118642] : [-(less_or_equal(_118640, _118636)), less_or_equal(_118642, _118638), _118642 = _118640, _118638 = _118636], (182 ^ _112771) ^ [_119080, _119082, _119084, _119086] : [-(less(_119084, _119080)), less(_119086, _119082), _119086 = _119084, _119082 = _119080], (196 ^ _112771) ^ [_119524, _119526, _119528, _119530] : [-(releasedAt(_119528, _119524)), releasedAt(_119530, _119526), _119530 = _119528, _119526 = _119524], (210 ^ _112771) ^ [_119948, _119950, _119952, _119954] : [-(holdsAt(_119952, _119948)), holdsAt(_119954, _119950), _119954 = _119952, _119950 = _119948], (234 ^ _112771) ^ [_120796, _120798, _120800] : [stoppedIn(_120800, _120798, _120796), 239 ^ _112771 : [(240 ^ _112771) ^ [] : [-(happens(237 ^ [_120796, _120798, _120800], 238 ^ [_120796, _120798, _120800]))], (242 ^ _112771) ^ [] : [-(less(_120800, 238 ^ [_120796, _120798, _120800]))], (244 ^ _112771) ^ [] : [-(less(238 ^ [_120796, _120798, _120800], _120796))], (246 ^ _112771) ^ [] : [-(terminates(237 ^ [_120796, _120798, _120800], _120798, 238 ^ [_120796, _120798, _120800]))]]], (248 ^ _112771) ^ [_121420, _121422, _121424] : [-(stoppedIn(_121424, _121422, _121420)), 249 ^ _112771 : [(250 ^ _112771) ^ [_121547, _121549] : [happens(_121549, _121547), less(_121424, _121547), less(_121547, _121420), terminates(_121549, _121422, _121547)]]], (266 ^ _112771) ^ [_122083, _122085, _122087] : [startedIn(_122087, _122083, _122085), 271 ^ _112771 : [(272 ^ _112771) ^ [] : [-(happens(269 ^ [_122083, _122085, _122087], 270 ^ [_122083, _122085, _122087]))], (274 ^ _112771) ^ [] : [-(less(_122087, 270 ^ [_122083, _122085, _122087]))], (276 ^ _112771) ^ [] : [-(less(270 ^ [_122083, _122085, _122087], _122085))], (278 ^ _112771) ^ [] : [-(initiates(269 ^ [_122083, _122085, _122087], _122083, 270 ^ [_122083, _122085, _122087]))]]], (280 ^ _112771) ^ [_122707, _122709, _122711] : [-(startedIn(_122711, _122707, _122709)), 281 ^ _112771 : [(282 ^ _112771) ^ [_122834, _122836] : [happens(_122836, _122834), less(_122711, _122834), less(_122834, _122709), initiates(_122836, _122707, _122834)]]], (298 ^ _112771) ^ [_123369, _123371, _123373, _123375, _123377] : [-(holdsAt(_123371, plus(_123375, _123369))), happens(_123377, _123375), initiates(_123377, _123373, _123375), less(n0, _123369), trajectory(_123373, _123375, _123371, _123369), -(stoppedIn(_123375, _123373, plus(_123375, _123369)))], (320 ^ _112771) ^ [_124066, _124068, _124070, _124072, _124074] : [-(holdsAt(_124066, plus(_124072, _124068))), happens(_124074, _124072), terminates(_124074, _124070, _124072), less(n0, _124068), antitrajectory(_124070, _124072, _124066, _124068), -(startedIn(_124072, _124070, plus(_124072, _124068)))], (342 ^ _112771) ^ [_124721, _124723] : [-(holdsAt(_124723, plus(_124721, n1))), holdsAt(_124723, _124721), -(releasedAt(_124723, plus(_124721, n1))), 352 ^ _112771 : [(353 ^ _112771) ^ [] : [-(happens(351 ^ [_124721, _124723], _124721))], (355 ^ _112771) ^ [] : [-(terminates(351 ^ [_124721, _124723], _124723, _124721))]]], (359 ^ _112771) ^ [_125275, _125277] : [holdsAt(_125277, plus(_125275, n1)), -(holdsAt(_125277, _125275)), -(releasedAt(_125277, plus(_125275, n1))), 369 ^ _112771 : [(370 ^ _112771) ^ [] : [-(happens(368 ^ [_125275, _125277], _125275))], (372 ^ _112771) ^ [] : [-(initiates(368 ^ [_125275, _125277], _125277, _125275))]]], (376 ^ _112771) ^ [_125833, _125835] : [-(releasedAt(_125835, plus(_125833, n1))), releasedAt(_125835, _125833), 382 ^ _112771 : [(383 ^ _112771) ^ [] : [-(happens(381 ^ [_125833, _125835], _125833))], (385 ^ _112771) ^ [] : [-(initiates(381 ^ [_125833, _125835], _125835, _125833)), -(terminates(381 ^ [_125833, _125835], _125835, _125833))]]], (393 ^ _112771) ^ [_126395, _126397] : [releasedAt(_126397, plus(_126395, n1)), -(releasedAt(_126397, _126395)), 399 ^ _112771 : [(400 ^ _112771) ^ [] : [-(happens(398 ^ [_126395, _126397], _126395))], (402 ^ _112771) ^ [] : [-(releases(398 ^ [_126395, _126397], _126397, _126395))]]], (406 ^ _112771) ^ [_126869, _126871, _126873] : [-(holdsAt(_126869, plus(_126871, n1))), happens(_126873, _126871), initiates(_126873, _126869, _126871)], (416 ^ _112771) ^ [_127200, _127202, _127204] : [holdsAt(_127200, plus(_127202, n1)), happens(_127204, _127202), terminates(_127204, _127200, _127202)], (426 ^ _112771) ^ [_127532, _127534, _127536] : [-(releasedAt(_127532, plus(_127534, n1))), happens(_127536, _127534), releases(_127536, _127532, _127534)], (436 ^ _112771) ^ [_127843, _127845, _127847] : [releasedAt(_127843, plus(_127845, n1)), happens(_127847, _127845), 441 ^ _112771 : [(442 ^ _112771) ^ [] : [initiates(_127847, _127843, _127845)], (444 ^ _112771) ^ [] : [terminates(_127847, _127843, _127845)]]], (686 ^ _112771) ^ [] : [-(plus(n0, n0) = n0)], (688 ^ _112771) ^ [] : [-(plus(n0, n1) = n1)], (690 ^ _112771) ^ [] : [-(plus(n0, n2) = n2)], (692 ^ _112771) ^ [] : [-(plus(n0, n3) = n3)], (694 ^ _112771) ^ [] : [-(plus(n1, n1) = n2)], (696 ^ _112771) ^ [] : [-(plus(n1, n2) = n3)], (698 ^ _112771) ^ [] : [-(plus(n1, n3) = n4)], (700 ^ _112771) ^ [] : [-(plus(n2, n2) = n4)], (702 ^ _112771) ^ [] : [-(plus(n2, n3) = n5)], (704 ^ _112771) ^ [] : [-(plus(n3, n3) = n6)], (706 ^ _112771) ^ [_135807, _135809] : [-(plus(_135809, _135807) = plus(_135807, _135809))], (718 ^ _112771) ^ [_136203, _136205] : [719 ^ _112771 : [(720 ^ _112771) ^ [] : [less(_136205, _136203)], (722 ^ _112771) ^ [] : [_136205 = _136203]], -(less_or_equal(_136205, _136203))], (708 ^ _112771) ^ [_135951, _135953] : [less_or_equal(_135953, _135951), -(less(_135953, _135951)), -(_135953 = _135951)], (726 ^ _112771) ^ [_136459] : [less(_136459, n0)], (728 ^ _112771) ^ [_136581] : [less(_136581, n1), -(less_or_equal(_136581, n0))], (734 ^ _112771) ^ [_136737] : [less_or_equal(_136737, n0), -(less(_136737, n1))], (740 ^ _112771) ^ [_136958] : [less(_136958, n2), -(less_or_equal(_136958, n1))], (746 ^ _112771) ^ [_137114] : [less_or_equal(_137114, n1), -(less(_137114, n2))], (752 ^ _112771) ^ [_137335] : [less(_137335, n3), -(less_or_equal(_137335, n2))], (758 ^ _112771) ^ [_137491] : [less_or_equal(_137491, n2), -(less(_137491, n3))], (764 ^ _112771) ^ [_137712] : [less(_137712, n4), -(less_or_equal(_137712, n3))], (770 ^ _112771) ^ [_137868] : [less_or_equal(_137868, n3), -(less(_137868, n4))], (776 ^ _112771) ^ [_138089] : [less(_138089, n5), -(less_or_equal(_138089, n4))], (782 ^ _112771) ^ [_138245] : [less_or_equal(_138245, n4), -(less(_138245, n5))], (788 ^ _112771) ^ [_138466] : [less(_138466, n6), -(less_or_equal(_138466, n5))], (794 ^ _112771) ^ [_138622] : [less_or_equal(_138622, n5), -(less(_138622, n6))], (800 ^ _112771) ^ [_138843] : [less(_138843, n7), -(less_or_equal(_138843, n6))], (806 ^ _112771) ^ [_138999] : [less_or_equal(_138999, n6), -(less(_138999, n7))], (812 ^ _112771) ^ [_139220] : [less(_139220, n8), -(less_or_equal(_139220, n7))], (818 ^ _112771) ^ [_139376] : [less_or_equal(_139376, n7), -(less(_139376, n8))], (824 ^ _112771) ^ [_139597] : [less(_139597, n9), -(less_or_equal(_139597, n8))], (830 ^ _112771) ^ [_139753] : [less_or_equal(_139753, n8), -(less(_139753, n9))], (854 ^ _112771) ^ [] : [holdsAt(forwards, n0)], (856 ^ _112771) ^ [] : [holdsAt(backwards, n0)], (858 ^ _112771) ^ [] : [holdsAt(spinning, n0)], (860 ^ _112771) ^ [_140654, _140656] : [releasedAt(_140656, _140654)], (836 ^ _112771) ^ [_139988, _139990] : [less(_139990, _139988), 839 ^ _112771 : [(840 ^ _112771) ^ [] : [less(_139988, _139990)], (842 ^ _112771) ^ [] : [_139988 = _139990]]], (844 ^ _112771) ^ [_140227, _140229] : [-(less(_140229, _140227)), -(less(_140227, _140229)), -(_140227 = _140229)], (448 ^ _112771) ^ [_128328, _128330, _128332] : [initiates(_128332, _128330, _128328), 453 ^ _112771 : [(454 ^ _112771) ^ [] : [-(_128332 = push)], (456 ^ _112771) ^ [] : [-(_128330 = forwards)], (458 ^ _112771) ^ [] : [happens(pull, _128328)]], 461 ^ _112771 : [(462 ^ _112771) ^ [] : [-(_128332 = pull)], (464 ^ _112771) ^ [] : [-(_128330 = backwards)], (466 ^ _112771) ^ [] : [happens(push, _128328)]], 467 ^ _112771 : [(468 ^ _112771) ^ [] : [-(_128332 = pull)], (470 ^ _112771) ^ [] : [-(_128330 = spinning)], (472 ^ _112771) ^ [] : [-(happens(push, _128328))]]], (474 ^ _112771) ^ [_129147, _129149, _129151] : [-(initiates(_129151, _129149, _129147)), 475 ^ _112771 : [(476 ^ _112771) ^ [] : [_129151 = push, _129149 = forwards, -(happens(pull, _129147))], (486 ^ _112771) ^ [] : [_129151 = pull, _129149 = backwards, -(happens(push, _129147))], (496 ^ _112771) ^ [] : [_129151 = pull, _129149 = spinning, happens(push, _129147)]]], (622 ^ _112771) ^ [_133409, _133411, _133413] : [releases(_133413, _133411, _133409)], (678 ^ _112771) ^ [] : [push = pull], (680 ^ _112771) ^ [] : [forwards = backwards], (682 ^ _112771) ^ [] : [forwards = spinning], (684 ^ _112771) ^ [] : [spinning = backwards], (624 ^ _112771) ^ [_133550, _133552] : [happens(_133552, _133550), 629 ^ _112771 : [(630 ^ _112771) ^ [] : [-(_133552 = push)], (632 ^ _112771) ^ [] : [-(_133550 = n0)]], 635 ^ _112771 : [(636 ^ _112771) ^ [] : [-(_133552 = pull)], (638 ^ _112771) ^ [] : [-(_133550 = n1)]], 641 ^ _112771 : [(642 ^ _112771) ^ [] : [-(_133552 = pull)], (644 ^ _112771) ^ [] : [-(_133550 = n2)]], 645 ^ _112771 : [(646 ^ _112771) ^ [] : [-(_133552 = push)], (648 ^ _112771) ^ [] : [-(_133550 = n2)]]], (650 ^ _112771) ^ [_134282, _134284] : [-(happens(_134284, _134282)), 651 ^ _112771 : [(652 ^ _112771) ^ [] : [_134284 = push, _134282 = n0], (658 ^ _112771) ^ [] : [_134284 = pull, _134282 = n1], (664 ^ _112771) ^ [] : [_134284 = pull, _134282 = n2], (670 ^ _112771) ^ [] : [_134284 = push, _134282 = n2]]], (508 ^ _112771) ^ [_130125, _130127, _130129] : [terminates(_130129, _130127, _130125), 513 ^ _112771 : [(514 ^ _112771) ^ [] : [-(_130129 = push)], (516 ^ _112771) ^ [] : [-(_130127 = backwards)], (518 ^ _112771) ^ [] : [happens(pull, _130125)]], 521 ^ _112771 : [(522 ^ _112771) ^ [] : [-(_130129 = pull)], (524 ^ _112771) ^ [] : [-(_130127 = forwards)], (526 ^ _112771) ^ [] : [happens(push, _130125)]], 529 ^ _112771 : [(530 ^ _112771) ^ [] : [-(_130129 = pull)], (532 ^ _112771) ^ [] : [-(_130127 = forwards)], (534 ^ _112771) ^ [] : [-(happens(push, _130125))]], 537 ^ _112771 : [(538 ^ _112771) ^ [] : [-(_130129 = pull)], (540 ^ _112771) ^ [] : [-(_130127 = backwards)], (542 ^ _112771) ^ [] : [-(happens(push, _130125))]], 545 ^ _112771 : [(546 ^ _112771) ^ [] : [-(_130129 = push)], (548 ^ _112771) ^ [] : [-(_130127 = spinning)], (550 ^ _112771) ^ [] : [happens(pull, _130125)]], 551 ^ _112771 : [(552 ^ _112771) ^ [] : [-(_130129 = pull)], (554 ^ _112771) ^ [] : [-(_130127 = spinning)], (556 ^ _112771) ^ [] : [happens(push, _130125)]]], (558 ^ _112771) ^ [_131687, _131689, _131691] : [-(terminates(_131691, _131689, _131687)), 559 ^ _112771 : [(560 ^ _112771) ^ [] : [_131691 = push, _131689 = backwards, -(happens(pull, _131687))], (570 ^ _112771) ^ [] : [_131691 = pull, _131689 = forwards, -(happens(push, _131687))], (580 ^ _112771) ^ [] : [_131691 = pull, _131689 = forwards, happens(push, _131687)], (590 ^ _112771) ^ [] : [_131691 = pull, _131689 = backwards, happens(push, _131687)], (600 ^ _112771) ^ [] : [_131691 = push, _131689 = spinning, -(happens(pull, _131687))], (610 ^ _112771) ^ [] : [_131691 = pull, _131689 = spinning, -(happens(push, _131687))]]]], input).
% 102.17/98.89 ncf('1',plain,[holdsAt(backwards, plus(n2, n1)), happens(pull, n2), terminates(pull, backwards, n2)],start(416 ^ 0,bind([[_127200, _127202, _127204], [backwards, n2, pull]]))).
% 102.17/98.89 ncf('1.1',plain,[-(holdsAt(backwards, plus(n2, n1))), holdsAt(backwards, n3), backwards = backwards, n3 = plus(n2, n1)],extension(210 ^ 1,bind([[_119948, _119950, _119952, _119954], [plus(n2, n1), n3, backwards, backwards]]))).
% 102.17/98.89 ncf('1.1.1',plain,[-(holdsAt(backwards, n3))],extension(862 ^ 2)).
% 102.17/98.89 ncf('1.1.2',plain,[-(backwards = backwards)],extension(2 ^ 2,bind([[_112915], [backwards]]))).
% 102.17/98.89 ncf('1.1.3',plain,[-(n3 = plus(n2, n1)), n3 = plus(n1, n2), plus(n1, n2) = plus(n2, n1)],extension(10 ^ 2,bind([[_113226, _113228, _113230], [plus(n2, n1), plus(n1, n2), n3]]))).
% 102.17/98.89 ncf('1.1.3.1',plain,[-(n3 = plus(n1, n2)), plus(n1, n2) = n3],extension(4 ^ 3,bind([[_113022, _113024], [n3, plus(n1, n2)]]))).
% 102.17/98.89 ncf('1.1.3.1.1',plain,[-(plus(n1, n2) = n3)],extension(696 ^ 4)).
% 102.17/98.89 ncf('1.1.3.2',plain,[-(plus(n1, n2) = plus(n2, n1))],extension(706 ^ 3,bind([[_135807, _135809], [n2, n1]]))).
% 102.17/98.89 ncf('1.2',plain,[-(happens(pull, n2)), happens(pull, n2), pull = pull, n2 = n2],extension(154 ^ 1,bind([[_118192, _118194, _118196, _118198], [n2, n2, pull, pull]]))).
% 102.17/98.89 ncf('1.2.1',plain,[-(happens(pull, n2)), 664 : pull = pull, 664 : n2 = n2],extension(650 ^ 2,bind([[_134282, _134284], [n2, pull]]))).
% 102.17/98.89 ncf('1.2.1.1',plain,[-(pull = pull)],extension(2 ^ 5,bind([[_112915], [pull]]))).
% 102.17/98.89 ncf('1.2.1.2',plain,[-(n2 = n2)],extension(2 ^ 5,bind([[_112915], [n2]]))).
% 102.17/98.89 ncf('1.2.2',plain,[-(pull = pull)],extension(2 ^ 2,bind([[_112915], [pull]]))).
% 102.17/98.89 ncf('1.2.3',plain,[-(n2 = n2)],extension(2 ^ 2,bind([[_112915], [n2]]))).
% 102.17/98.89 ncf('1.3',plain,[-(terminates(pull, backwards, n2)), 590 : pull = pull, 590 : backwards = backwards, 590 : happens(push, n2)],extension(558 ^ 1,bind([[_131687, _131689, _131691], [n2, backwards, pull]]))).
% 102.17/98.89 ncf('1.3.1',plain,[-(pull = pull)],extension(2 ^ 4,bind([[_112915], [pull]]))).
% 102.17/98.89 ncf('1.3.2',plain,[-(backwards = backwards)],extension(2 ^ 4,bind([[_112915], [backwards]]))).
% 102.17/98.89 ncf('1.3.3',plain,[-(happens(push, n2)), 670 : push = push, 670 : n2 = n2],extension(650 ^ 4,bind([[_134282, _134284], [n2, push]]))).
% 102.17/98.89 ncf('1.3.3.1',plain,[-(push = push)],extension(2 ^ 7,bind([[_112915], [push]]))).
% 102.17/98.89 ncf('1.3.3.2',plain,[-(n2 = n2)],extension(2 ^ 7,bind([[_112915], [n2]]))).
% 102.17/98.89 %-----------------------------------------------------
% 102.17/98.89 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------