%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO010+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:47:18 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO010+4 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 00:57:30 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(752 ^ _108140) ^ [] : [-(occurrence_of(750 ^ [], tptp0))], (754 ^ _108140) ^ [_133548, _133550] : [leaf_occ(_133548, 750 ^ []), 759 ^ _108140 : [(760 ^ _108140) ^ [] : [-(occurrence_of(_133548, tptp1))], (763 ^ _108140) ^ [] : [-(occurrence_of(761 ^ [_133548, _133550], tptp2))], (765 ^ _108140) ^ [] : [-(min_precedes(_133550, 761 ^ [_133548, _133550], tptp0))]], 766 ^ _108140 : [(767 ^ _108140) ^ [] : [-(occurrence_of(_133548, tptp2))], (770 ^ _108140) ^ [] : [-(occurrence_of(768 ^ [_133548, _133550], tptp1))], (772 ^ _108140) ^ [] : [-(min_precedes(_133550, 768 ^ [_133548, _133550], tptp0))]]], (2 ^ _108140) ^ [_108264] : [-(_108264 = _108264)], (4 ^ _108140) ^ [_108371, _108373] : [_108373 = _108371, -(_108371 = _108373)], (10 ^ _108140) ^ [_108575, _108577, _108579] : [-(_108579 = _108575), _108579 = _108577, _108577 = _108575], (20 ^ _108140) ^ [_108888, _108890] : [-(activity_occurrence(_108888)), _108890 = _108888, activity_occurrence(_108890)], (30 ^ _108140) ^ [_109211, _109213, _109215, _109217] : [-(atocc(_109215, _109211)), atocc(_109217, _109213), _109217 = _109215, _109213 = _109211], (44 ^ _108140) ^ [_109655, _109657, _109659, _109661] : [-(subactivity(_109659, _109655)), subactivity(_109661, _109657), _109661 = _109659, _109657 = _109655], (58 ^ _108140) ^ [_110099, _110101, _110103, _110105] : [-(leaf(_110103, _110099)), leaf(_110105, _110101), _110105 = _110103, _110101 = _110099], (72 ^ _108140) ^ [_110515, _110517] : [-(legal(_110515)), _110517 = _110515, legal(_110517)], (82 ^ _108140) ^ [_110838, _110840, _110842, _110844] : [-(root(_110842, _110838)), root(_110844, _110840), _110844 = _110842, _110840 = _110838], (96 ^ _108140) ^ [_111254, _111256] : [-(arboreal(_111254)), _111256 = _111254, arboreal(_111256)], (106 ^ _108140) ^ [_111577, _111579, _111581, _111583] : [-(subactivity_occurrence(_111581, _111577)), subactivity_occurrence(_111583, _111579), _111583 = _111581, _111579 = _111577], (120 ^ _108140) ^ [_112021, _112023, _112025, _112027] : [-(earlier(_112025, _112021)), earlier(_112027, _112023), _112027 = _112025, _112023 = _112021], (134 ^ _108140) ^ [_112465, _112467, _112469, _112471] : [-(precedes(_112469, _112465)), precedes(_112471, _112467), _112471 = _112469, _112467 = _112465], (148 ^ _108140) ^ [_112909, _112911, _112913, _112915] : [-(root_occ(_112913, _112909)), root_occ(_112915, _112911), _112915 = _112913, _112911 = _112909], (162 ^ _108140) ^ [_113381, _113383, _113385, _113387, _113389, _113391] : [-(next_subocc(_113389, _113385, _113381)), next_subocc(_113391, _113387, _113383), _113391 = _113389, _113387 = _113385, _113383 = _113381], (180 ^ _108140) ^ [_113934, _113936] : [-(activity(_113934)), _113936 = _113934, activity(_113936)], (190 ^ _108140) ^ [_114229, _114231] : [-(atomic(_114229)), _114231 = _114229, atomic(_114231)], (200 ^ _108140) ^ [_114552, _114554, _114556, _114558] : [-(leaf_occ(_114556, _114552)), leaf_occ(_114558, _114554), _114558 = _114556, _114554 = _114552], (214 ^ _108140) ^ [_114996, _114998, _115000, _115002] : [-(occurrence_of(_115000, _114996)), occurrence_of(_115002, _114998), _115002 = _115000, _114998 = _114996], (228 ^ _108140) ^ [_115448, _115450, _115452, _115454, _115456, _115458] : [-(min_precedes(_115456, _115452, _115448)), min_precedes(_115458, _115454, _115450), _115458 = _115456, _115454 = _115452, _115450 = _115448], (246 ^ _108140) ^ [_116075, _116077] : [254 ^ _108140 : [(255 ^ _108140) ^ [] : [-(root(253 ^ [_116075, _116077], _116077))], (257 ^ _108140) ^ [] : [-(subactivity_occurrence(253 ^ [_116075, _116077], _116075))]], occurrence_of(_116075, _116077), -(atomic(_116077))], (259 ^ _108140) ^ [_116562, _116564, _116566, _116568, _116570] : [-(min_precedes(_116566, _116562, _116570)), occurrence_of(_116568, _116570), root_occ(_116564, _116568), leaf_occ(_116562, _116568), subactivity_occurrence(_116566, _116568), min_precedes(_116564, _116566, _116570), -(_116566 = _116562)], (285 ^ _108140) ^ [_117330, _117332, _117334, _117336] : [-(_117330 = _117332), occurrence_of(_117334, _117336), subactivity_occurrence(_117332, _117334), leaf_occ(_117330, _117334), arboreal(_117332), -(min_precedes(_117332, _117330, _117336))], (307 ^ _108140) ^ [_117943, _117945] : [occurrence_of(_117943, _117945), 310 ^ _108140 : [(311 ^ _108140) ^ [] : [-(activity(_117945))], (313 ^ _108140) ^ [] : [-(activity_occurrence(_117943))]]], (315 ^ _108140) ^ [_118252, _118254, _118256, _118258] : [-(min_precedes(_118254, _118252, _118258)), -(min_precedes(_118252, _118254, _118258)), -(_118254 = _118252), occurrence_of(_118256, _118258), arboreal(_118254), arboreal(_118252), subactivity_occurrence(_118254, _118256), subactivity_occurrence(_118252, _118256)], (345 ^ _108140) ^ [_119062, _119064] : [root(_119062, _119064), 349 ^ _108140 : [(350 ^ _108140) ^ [] : [-(subactivity(348 ^ [_119062, _119064], _119064))], (352 ^ _108140) ^ [] : [-(atocc(_119062, 348 ^ [_119062, _119064]))]]], (354 ^ _108140) ^ [_119431, _119433, _119435] : [min_precedes(_119433, _119431, _119435), 358 ^ _108140 : [(359 ^ _108140) ^ [] : [-(occurrence_of(357 ^ [_119431, _119433, _119435], _119435))], (361 ^ _108140) ^ [] : [-(subactivity_occurrence(_119433, 357 ^ [_119431, _119433, _119435]))], (363 ^ _108140) ^ [] : [-(subactivity_occurrence(_119431, 357 ^ [_119431, _119433, _119435]))]]], (365 ^ _108140) ^ [_119895, _119897] : [373 ^ _108140 : [(374 ^ _108140) ^ [] : [-(occurrence_of(372 ^ [_119895, _119897], _119895))], (376 ^ _108140) ^ [] : [-(leaf_occ(_119897, 372 ^ [_119895, _119897]))]], leaf(_119897, _119895), -(atomic(_119895))], (378 ^ _108140) ^ [_120354, _120356, _120358] : [-(_120356 = _120354), occurrence_of(_120358, _120356), occurrence_of(_120358, _120354)], (388 ^ _108140) ^ [_120677, _120679, _120681] : [395 ^ _108140 : [(396 ^ _108140) ^ [_120892] : [min_precedes(_120679, _120892, _120677)]], occurrence_of(_120681, _120677), leaf_occ(_120679, _120681)], (398 ^ _108140) ^ [_121025, _121027, _121029] : [405 ^ _108140 : [(406 ^ _108140) ^ [_121240] : [min_precedes(_121240, _121027, _121025)]], occurrence_of(_121029, _121025), root_occ(_121027, _121029)], (408 ^ _108140) ^ [_121359, _121361] : [subactivity_occurrence(_121361, _121359), 411 ^ _108140 : [(412 ^ _108140) ^ [] : [-(activity_occurrence(_121361))], (414 ^ _108140) ^ [] : [-(activity_occurrence(_121359))]]], (416 ^ _108140) ^ [_121626] : [activity_occurrence(_121626), 420 ^ _108140 : [(421 ^ _108140) ^ [] : [-(activity(419 ^ [_121626]))], (423 ^ _108140) ^ [] : [-(occurrence_of(_121626, 419 ^ [_121626]))]]], (425 ^ _108140) ^ [_121946] : [legal(_121946), -(arboreal(_121946))], (431 ^ _108140) ^ [_122175, _122177] : [atocc(_122177, _122175), 435 ^ _108140 : [(436 ^ _108140) ^ [] : [-(subactivity(_122175, 434 ^ [_122175, _122177]))], (438 ^ _108140) ^ [] : [-(atomic(434 ^ [_122175, _122177]))], (440 ^ _108140) ^ [] : [-(occurrence_of(_122177, 434 ^ [_122175, _122177]))]]], (442 ^ _108140) ^ [_122566, _122568] : [-(atocc(_122568, _122566)), 443 ^ _108140 : [(444 ^ _108140) ^ [_122663] : [subactivity(_122566, _122663), atomic(_122663), occurrence_of(_122568, _122663)]]], (456 ^ _108140) ^ [_123055, _123057] : [leaf(_123057, _123055), 459 ^ _108140 : [(467 ^ _108140) ^ [_123395] : [min_precedes(_123057, _123395, _123055)], (460 ^ _108140) ^ [] : [-(root(_123057, _123055)), -(min_precedes(463 ^ [_123055, _123057], _123057, _123055))]]], (469 ^ _108140) ^ [_123466, _123468] : [-(leaf(_123468, _123466)), 472 ^ _108140 : [(473 ^ _108140) ^ [] : [root(_123468, _123466)], (475 ^ _108140) ^ [_123656] : [min_precedes(_123656, _123468, _123466)]], -(min_precedes(_123468, 476 ^ [_123466, _123468], _123466))], (482 ^ _108140) ^ [_123927, _123929] : [occurrence_of(_123929, _123927), 485 ^ _108140 : [(486 ^ _108140) ^ [] : [arboreal(_123929), -(atomic(_123927))], (492 ^ _108140) ^ [] : [atomic(_123927), -(arboreal(_123929))]]], (498 ^ _108140) ^ [_124381, _124383] : [root(_124383, _124381), -(legal(_124383))], (504 ^ _108140) ^ [_124618, _124620] : [leaf_occ(_124620, _124618), 508 ^ _108140 : [(509 ^ _108140) ^ [] : [-(occurrence_of(_124618, 507 ^ [_124618, _124620]))], (511 ^ _108140) ^ [] : [-(subactivity_occurrence(_124620, _124618))], (513 ^ _108140) ^ [] : [-(leaf(_124620, 507 ^ [_124618, _124620]))]]], (515 ^ _108140) ^ [_125005, _125007] : [-(leaf_occ(_125007, _125005)), 516 ^ _108140 : [(517 ^ _108140) ^ [_125103] : [occurrence_of(_125005, _125103), subactivity_occurrence(_125007, _125005), leaf(_125007, _125103)]]], (529 ^ _108140) ^ [_125497, _125499] : [root_occ(_125499, _125497), 533 ^ _108140 : [(534 ^ _108140) ^ [] : [-(occurrence_of(_125497, 532 ^ [_125497, _125499]))], (536 ^ _108140) ^ [] : [-(subactivity_occurrence(_125499, _125497))], (538 ^ _108140) ^ [] : [-(root(_125499, 532 ^ [_125497, _125499]))]]], (540 ^ _108140) ^ [_125884, _125886] : [-(root_occ(_125886, _125884)), 541 ^ _108140 : [(542 ^ _108140) ^ [_125982] : [occurrence_of(_125884, _125982), subactivity_occurrence(_125886, _125884), root(_125886, _125982)]]], (554 ^ _108140) ^ [_126347, _126349] : [earlier(_126349, _126347), earlier(_126347, _126349)], (560 ^ _108140) ^ [_126587, _126589] : [precedes(_126589, _126587), 563 ^ _108140 : [(564 ^ _108140) ^ [] : [-(earlier(_126589, _126587))], (566 ^ _108140) ^ [] : [-(legal(_126587))]]], (568 ^ _108140) ^ [_126822, _126824] : [-(precedes(_126824, _126822)), earlier(_126824, _126822), legal(_126822)], (578 ^ _108140) ^ [_127135, _127137, _127139] : [min_precedes(_127139, _127137, _127135), root(_127137, _127135)], (584 ^ _108140) ^ [_127368, _127370, _127372] : [min_precedes(_127372, _127370, _127368), 588 ^ _108140 : [(589 ^ _108140) ^ [] : [-(root(587 ^ [_127368, _127370, _127372], _127368))], (591 ^ _108140) ^ [] : [-(min_precedes(587 ^ [_127368, _127370, _127372], _127370, _127368))]]], (593 ^ _108140) ^ [_127758, _127760, _127762] : [min_precedes(_127762, _127760, _127758), -(precedes(_127762, _127760))], (599 ^ _108140) ^ [_127990, _127992, _127994] : [next_subocc(_127994, _127992, _127990), 602 ^ _108140 : [(603 ^ _108140) ^ [] : [-(arboreal(_127994))], (605 ^ _108140) ^ [] : [-(arboreal(_127992))]]], (607 ^ _108140) ^ [_128324, _128326, _128328] : [next_subocc(_128328, _128326, _128324), 610 ^ _108140 : [(611 ^ _108140) ^ [] : [-(min_precedes(_128328, _128326, _128324))], (613 ^ _108140) ^ [_128547] : [min_precedes(_128328, _128547, _128324), min_precedes(_128547, _128326, _128324)]]], (619 ^ _108140) ^ [_128737, _128739, _128741] : [-(next_subocc(_128741, _128739, _128737)), min_precedes(_128741, _128739, _128737), 625 ^ _108140 : [(626 ^ _108140) ^ [] : [-(min_precedes(_128741, 624 ^ [_128737, _128739, _128741], _128737))], (628 ^ _108140) ^ [] : [-(min_precedes(624 ^ [_128737, _128739, _128741], _128739, _128737))]]], (632 ^ _108140) ^ [_129244, _129246, _129248, _129250] : [-(subactivity_occurrence(_129250, _129244)), min_precedes(_129250, _129248, _129246), occurrence_of(_129244, _129246), subactivity_occurrence(_129248, _129244)], (646 ^ _108140) ^ [_129690, _129692, _129694, _129696] : [-(_129696 = _129694), occurrence_of(_129692, _129690), -(atomic(_129690)), leaf_occ(_129696, _129692), leaf_occ(_129694, _129692)], (664 ^ _108140) ^ [_130232, _130234, _130236, _130238] : [-(_130238 = _130236), occurrence_of(_130234, _130232), root_occ(_130238, _130234), root_occ(_130236, _130234)], (678 ^ _108140) ^ [_130662, _130664, _130666] : [-(earlier(_130666, _130662)), earlier(_130666, _130664), earlier(_130664, _130662)], (727 ^ _108140) ^ [] : [-(activity(tptp0))], (729 ^ _108140) ^ [] : [atomic(tptp0)], (731 ^ _108140) ^ [] : [-(atomic(tptp4))], (733 ^ _108140) ^ [] : [-(atomic(tptp1))], (735 ^ _108140) ^ [] : [-(atomic(tptp2))], (737 ^ _108140) ^ [] : [-(atomic(tptp3))], (739 ^ _108140) ^ [] : [tptp4 = tptp3], (741 ^ _108140) ^ [] : [tptp4 = tptp1], (743 ^ _108140) ^ [] : [tptp4 = tptp2], (745 ^ _108140) ^ [] : [tptp3 = tptp1], (747 ^ _108140) ^ [] : [tptp3 = tptp2], (749 ^ _108140) ^ [] : [tptp1 = tptp2], (702 ^ _108140) ^ [_131407] : [occurrence_of(_131407, tptp0), 708 ^ _108140 : [(709 ^ _108140) ^ [] : [-(occurrence_of(705 ^ [_131407], tptp3))], (711 ^ _108140) ^ [] : [-(root_occ(705 ^ [_131407], _131407))], (713 ^ _108140) ^ [] : [-(occurrence_of(706 ^ [_131407], tptp4))], (715 ^ _108140) ^ [] : [-(next_subocc(705 ^ [_131407], 706 ^ [_131407], tptp0))], (723 ^ _108140) ^ [] : [-(next_subocc(706 ^ [_131407], 707 ^ [_131407], tptp0))], (725 ^ _108140) ^ [] : [-(leaf_occ(707 ^ [_131407], _131407))], (717 ^ _108140) ^ [] : [-(occurrence_of(707 ^ [_131407], tptp1)), -(occurrence_of(707 ^ [_131407], tptp2))]]], (688 ^ _108140) ^ [_130999, _131001, _131003, _131005] : [-(min_precedes(_131003, _131001, _130999)), min_precedes(_131005, _131003, _130999), min_precedes(_131005, _131001, _130999), precedes(_131003, _131001)]], input).
% 0.36/1.37 ncf('1',plain,[396 : min_precedes(707 ^ [750 ^ []], 761 ^ [707 ^ [750 ^ []], 707 ^ [750 ^ []]], tptp0), 396 : occurrence_of(750 ^ [], tptp0), 396 : leaf_occ(707 ^ [750 ^ []], 750 ^ [])],start(388 ^ 0,bind([[_120677, _120679, _120681, _120892], [tptp0, 707 ^ [750 ^ []], 750 ^ [], 761 ^ [707 ^ [750 ^ []], 707 ^ [750 ^ []]]]]))).
% 0.36/1.37 ncf('1.1',plain,[-(min_precedes(707 ^ [750 ^ []], 761 ^ [707 ^ [750 ^ []], 707 ^ [750 ^ []]], tptp0)), leaf_occ(707 ^ [750 ^ []], 750 ^ []), 772 : -(min_precedes(707 ^ [750 ^ []], 768 ^ [707 ^ [750 ^ []], 707 ^ [750 ^ []]], tptp0))],extension(754 ^ 3,bind([[_133548, _133550], [707 ^ [750 ^ []], 707 ^ [750 ^ []]]]))).
% 0.36/1.37 ncf('1.1.1',plain,[-(leaf_occ(707 ^ [750 ^ []], 750 ^ [])), occurrence_of(750 ^ [], tptp0)],extension(702 ^ 4,bind([[_131407], [750 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.1',plain,[-(occurrence_of(750 ^ [], tptp0))],extension(752 ^ 5)).
% 0.36/1.37 ncf('1.1.2',plain,[min_precedes(707 ^ [750 ^ []], 768 ^ [707 ^ [750 ^ []], 707 ^ [750 ^ []]], tptp0)],extension(396 ^ 6,bind([[_120892], [768 ^ [707 ^ [750 ^ []], 707 ^ [750 ^ []]]]]))).
% 0.36/1.37 ncf('1.2',plain,[-(occurrence_of(750 ^ [], tptp0))],extension(752 ^ 1)).
% 0.36/1.37 ncf('1.3',plain,[-(leaf_occ(707 ^ [750 ^ []], 750 ^ [])), leaf_occ(707 ^ [750 ^ []], 750 ^ []), 707 ^ [750 ^ []] = 707 ^ [750 ^ []], 750 ^ [] = 750 ^ []],extension(200 ^ 1,bind([[_114552, _114554, _114556, _114558], [750 ^ [], 750 ^ [], 707 ^ [750 ^ []], 707 ^ [750 ^ []]]]))).
% 0.36/1.37 ncf('1.3.1',plain,[-(leaf_occ(707 ^ [750 ^ []], 750 ^ [])), occurrence_of(750 ^ [], tptp0)],extension(702 ^ 2,bind([[_131407], [750 ^ []]]))).
% 0.36/1.37 ncf('1.3.1.1',plain,[-(occurrence_of(750 ^ [], tptp0))],extension(752 ^ 3)).
% 0.36/1.37 ncf('1.3.2',plain,[-(707 ^ [750 ^ []] = 707 ^ [750 ^ []])],extension(2 ^ 2,bind([[_108264], [707 ^ [750 ^ []]]]))).
% 0.36/1.37 ncf('1.3.3',plain,[-(750 ^ [] = 750 ^ [])],extension(2 ^ 2,bind([[_108264], [750 ^ []]]))).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------