%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO011+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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.37s 1.37s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO011+2 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n019.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 01:33:42 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.37/1.37
% 0.37/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 ncf(matrix, plain, [(720 ^ _104517) ^ [] : [-(occurrence_of(718 ^ [], tptp0))], (722 ^ _104517) ^ [_129139, _129141] : [leaf_occ(_129139, 718 ^ []), 727 ^ _104517 : [(728 ^ _104517) ^ [] : [-(occurrence_of(_129139, tptp1))], (731 ^ _104517) ^ [] : [-(occurrence_of(729 ^ [_129139, _129141], tptp2))], (733 ^ _104517) ^ [] : [-(subactivity_occurrence(729 ^ [_129139, _129141], 718 ^ []))], (735 ^ _104517) ^ [] : [-(min_precedes(_129141, 729 ^ [_129139, _129141], tptp0))]], 736 ^ _104517 : [(737 ^ _104517) ^ [] : [-(occurrence_of(_129139, tptp2))], (740 ^ _104517) ^ [] : [-(occurrence_of(738 ^ [_129139, _129141], tptp1))], (742 ^ _104517) ^ [] : [-(subactivity_occurrence(738 ^ [_129139, _129141], 718 ^ []))], (744 ^ _104517) ^ [] : [-(min_precedes(_129141, 738 ^ [_129139, _129141], tptp0))]]], (2 ^ _104517) ^ [_104641] : [-(_104641 = _104641)], (4 ^ _104517) ^ [_104748, _104750] : [_104750 = _104748, -(_104748 = _104750)], (10 ^ _104517) ^ [_104952, _104954, _104956] : [-(_104956 = _104952), _104956 = _104954, _104954 = _104952], (20 ^ _104517) ^ [_105293, _105295, _105297, _105299] : [-(precedes(_105297, _105293)), precedes(_105299, _105295), _105299 = _105297, _105295 = _105293], (34 ^ _104517) ^ [_105737, _105739, _105741, _105743] : [-(earlier(_105741, _105737)), earlier(_105743, _105739), _105743 = _105741, _105739 = _105737], (48 ^ _104517) ^ [_106153, _106155] : [-(legal(_106153)), _106155 = _106153, legal(_106155)], (58 ^ _104517) ^ [_106476, _106478, _106480, _106482] : [-(leaf(_106480, _106476)), leaf(_106482, _106478), _106482 = _106480, _106478 = _106476], (72 ^ _104517) ^ [_106920, _106922, _106924, _106926] : [-(atocc(_106924, _106920)), atocc(_106926, _106922), _106926 = _106924, _106922 = _106920], (86 ^ _104517) ^ [_107336, _107338] : [-(arboreal(_107336)), _107338 = _107336, arboreal(_107338)], (96 ^ _104517) ^ [_107631, _107633] : [-(activity_occurrence(_107631)), _107633 = _107631, activity_occurrence(_107633)], (106 ^ _104517) ^ [_107954, _107956, _107958, _107960] : [-(root(_107958, _107954)), root(_107960, _107956), _107960 = _107958, _107956 = _107954], (120 ^ _104517) ^ [_108398, _108400, _108402, _108404] : [-(subactivity(_108402, _108398)), subactivity(_108404, _108400), _108404 = _108402, _108400 = _108398], (134 ^ _104517) ^ [_108842, _108844, _108846, _108848] : [-(root_occ(_108846, _108842)), root_occ(_108848, _108844), _108848 = _108846, _108844 = _108842], (148 ^ _104517) ^ [_109314, _109316, _109318, _109320, _109322, _109324] : [-(next_subocc(_109322, _109318, _109314)), next_subocc(_109324, _109320, _109316), _109324 = _109322, _109320 = _109318, _109316 = _109314], (166 ^ _104517) ^ [_109867, _109869] : [-(activity(_109867)), _109869 = _109867, activity(_109869)], (176 ^ _104517) ^ [_110162, _110164] : [-(atomic(_110162)), _110164 = _110162, atomic(_110164)], (186 ^ _104517) ^ [_110485, _110487, _110489, _110491] : [-(leaf_occ(_110489, _110485)), leaf_occ(_110491, _110487), _110491 = _110489, _110487 = _110485], (200 ^ _104517) ^ [_110929, _110931, _110933, _110935] : [-(occurrence_of(_110933, _110929)), occurrence_of(_110935, _110931), _110935 = _110933, _110931 = _110929], (214 ^ _104517) ^ [_111373, _111375, _111377, _111379] : [-(subactivity_occurrence(_111377, _111373)), subactivity_occurrence(_111379, _111375), _111379 = _111377, _111375 = _111373], (228 ^ _104517) ^ [_111825, _111827, _111829, _111831, _111833, _111835] : [-(min_precedes(_111833, _111829, _111825)), min_precedes(_111835, _111831, _111827), _111835 = _111833, _111831 = _111829, _111827 = _111825], (246 ^ _104517) ^ [_112480, _112482, _112484, _112486] : [-(min_precedes(_112486, _112482, _112480)), min_precedes(_112486, _112484, _112480), min_precedes(_112484, _112482, _112480)], (256 ^ _104517) ^ [_112819, _112821, _112823] : [-(earlier(_112823, _112819)), earlier(_112823, _112821), earlier(_112821, _112819)], (266 ^ _104517) ^ [_113156, _113158, _113160, _113162] : [-(_113162 = _113160), occurrence_of(_113158, _113156), root_occ(_113162, _113158), root_occ(_113160, _113158)], (280 ^ _104517) ^ [_113600, _113602, _113604, _113606] : [-(_113606 = _113604), occurrence_of(_113602, _113600), -(atomic(_113600)), leaf_occ(_113606, _113602), leaf_occ(_113604, _113602)], (298 ^ _104517) ^ [_114157, _114159, _114161] : [next_subocc(_114161, _114159, _114157), 301 ^ _104517 : [(302 ^ _104517) ^ [] : [-(min_precedes(_114161, _114159, _114157))], (304 ^ _104517) ^ [_114380] : [min_precedes(_114161, _114380, _114157), min_precedes(_114380, _114159, _114157)]]], (310 ^ _104517) ^ [_114570, _114572, _114574] : [-(next_subocc(_114574, _114572, _114570)), min_precedes(_114574, _114572, _114570), 316 ^ _104517 : [(317 ^ _104517) ^ [] : [-(min_precedes(_114574, 315 ^ [_114570, _114572, _114574], _114570))], (319 ^ _104517) ^ [] : [-(min_precedes(315 ^ [_114570, _114572, _114574], _114572, _114570))]]], (323 ^ _104517) ^ [_115063, _115065, _115067] : [next_subocc(_115067, _115065, _115063), 326 ^ _104517 : [(327 ^ _104517) ^ [] : [-(arboreal(_115067))], (329 ^ _104517) ^ [] : [-(arboreal(_115065))]]], (331 ^ _104517) ^ [_115368, _115370, _115372] : [min_precedes(_115372, _115370, _115368), -(precedes(_115372, _115370))], (337 ^ _104517) ^ [_115600, _115602, _115604] : [min_precedes(_115604, _115602, _115600), root(_115602, _115600)], (343 ^ _104517) ^ [_115848, _115850] : [precedes(_115850, _115848), 346 ^ _104517 : [(347 ^ _104517) ^ [] : [-(earlier(_115850, _115848))], (349 ^ _104517) ^ [] : [-(legal(_115848))]]], (351 ^ _104517) ^ [_116083, _116085] : [-(precedes(_116085, _116083)), earlier(_116085, _116083), legal(_116083)], (361 ^ _104517) ^ [_116382, _116384] : [earlier(_116384, _116382), earlier(_116382, _116384)], (367 ^ _104517) ^ [_116622, _116624] : [root_occ(_116624, _116622), 371 ^ _104517 : [(372 ^ _104517) ^ [] : [-(occurrence_of(_116622, 370 ^ [_116622, _116624]))], (374 ^ _104517) ^ [] : [-(subactivity_occurrence(_116624, _116622))], (376 ^ _104517) ^ [] : [-(root(_116624, 370 ^ [_116622, _116624]))]]], (378 ^ _104517) ^ [_117009, _117011] : [-(root_occ(_117011, _117009)), 379 ^ _104517 : [(380 ^ _104517) ^ [_117107] : [occurrence_of(_117009, _117107), subactivity_occurrence(_117011, _117009), root(_117011, _117107)]]], (392 ^ _104517) ^ [_117501, _117503] : [leaf_occ(_117503, _117501), 396 ^ _104517 : [(397 ^ _104517) ^ [] : [-(occurrence_of(_117501, 395 ^ [_117501, _117503]))], (399 ^ _104517) ^ [] : [-(subactivity_occurrence(_117503, _117501))], (401 ^ _104517) ^ [] : [-(leaf(_117503, 395 ^ [_117501, _117503]))]]], (403 ^ _104517) ^ [_117888, _117890] : [-(leaf_occ(_117890, _117888)), 404 ^ _104517 : [(405 ^ _104517) ^ [_117986] : [occurrence_of(_117888, _117986), subactivity_occurrence(_117890, _117888), leaf(_117890, _117986)]]], (417 ^ _104517) ^ [_118351, _118353] : [root(_118353, _118351), -(legal(_118353))], (423 ^ _104517) ^ [_118559, _118561] : [occurrence_of(_118561, _118559), 426 ^ _104517 : [(427 ^ _104517) ^ [] : [arboreal(_118561), -(atomic(_118559))], (433 ^ _104517) ^ [] : [atomic(_118559), -(arboreal(_118561))]]], (439 ^ _104517) ^ [_119042, _119044] : [leaf(_119044, _119042), 442 ^ _104517 : [(450 ^ _104517) ^ [_119382] : [min_precedes(_119044, _119382, _119042)], (443 ^ _104517) ^ [] : [-(root(_119044, _119042)), -(min_precedes(446 ^ [_119042, _119044], _119044, _119042))]]], (452 ^ _104517) ^ [_119453, _119455] : [-(leaf(_119455, _119453)), 455 ^ _104517 : [(456 ^ _104517) ^ [] : [root(_119455, _119453)], (458 ^ _104517) ^ [_119643] : [min_precedes(_119643, _119455, _119453)]], -(min_precedes(_119455, 459 ^ [_119453, _119455], _119453))], (465 ^ _104517) ^ [_119943, _119945] : [atocc(_119945, _119943), 469 ^ _104517 : [(470 ^ _104517) ^ [] : [-(subactivity(_119943, 468 ^ [_119943, _119945]))], (472 ^ _104517) ^ [] : [-(atomic(468 ^ [_119943, _119945]))], (474 ^ _104517) ^ [] : [-(occurrence_of(_119945, 468 ^ [_119943, _119945]))]]], (476 ^ _104517) ^ [_120334, _120336] : [-(atocc(_120336, _120334)), 477 ^ _104517 : [(478 ^ _104517) ^ [_120431] : [subactivity(_120334, _120431), atomic(_120431), occurrence_of(_120336, _120431)]]], (490 ^ _104517) ^ [_120794, _120796] : [-(root(_120796, _120794)), atocc(_120796, _120794), legal(_120796)], (500 ^ _104517) ^ [_121077] : [legal(_121077), -(arboreal(_121077))], (506 ^ _104517) ^ [_121263] : [activity_occurrence(_121263), 510 ^ _104517 : [(511 ^ _104517) ^ [] : [-(activity(509 ^ [_121263]))], (513 ^ _104517) ^ [] : [-(occurrence_of(_121263, 509 ^ [_121263]))]]], (515 ^ _104517) ^ [_121597, _121599] : [subactivity_occurrence(_121599, _121597), 518 ^ _104517 : [(519 ^ _104517) ^ [] : [-(activity_occurrence(_121599))], (521 ^ _104517) ^ [] : [-(activity_occurrence(_121597))]]], (523 ^ _104517) ^ [_121892, _121894, _121896] : [530 ^ _104517 : [(531 ^ _104517) ^ [_122107] : [min_precedes(_122107, _121894, _121892)]], occurrence_of(_121896, _121892), root_occ(_121894, _121896)], (533 ^ _104517) ^ [_122240, _122242, _122244] : [540 ^ _104517 : [(541 ^ _104517) ^ [_122455] : [min_precedes(_122242, _122455, _122240)]], occurrence_of(_122244, _122240), leaf_occ(_122242, _122244)], (543 ^ _104517) ^ [_122588, _122590, _122592] : [-(_122590 = _122588), occurrence_of(_122592, _122590), occurrence_of(_122592, _122588)], (553 ^ _104517) ^ [_122897, _122899] : [561 ^ _104517 : [(562 ^ _104517) ^ [] : [-(occurrence_of(560 ^ [_122897, _122899], _122897))], (564 ^ _104517) ^ [] : [-(leaf_occ(_122899, 560 ^ [_122897, _122899]))]], leaf(_122899, _122897), -(atomic(_122897))], (566 ^ _104517) ^ [_123356, _123358, _123360] : [min_precedes(_123358, _123356, _123360), 570 ^ _104517 : [(571 ^ _104517) ^ [] : [-(occurrence_of(569 ^ [_123356, _123358, _123360], _123360))], (573 ^ _104517) ^ [] : [-(subactivity_occurrence(_123358, 569 ^ [_123356, _123358, _123360]))], (575 ^ _104517) ^ [] : [-(subactivity_occurrence(_123356, 569 ^ [_123356, _123358, _123360]))]]], (577 ^ _104517) ^ [_123820, _123822] : [585 ^ _104517 : [(586 ^ _104517) ^ [] : [-(occurrence_of(584 ^ [_123820, _123822], _123820))], (588 ^ _104517) ^ [] : [-(leaf_occ(_123822, 584 ^ [_123820, _123822]))]], leaf(_123822, _123820), -(atomic(_123820))], (590 ^ _104517) ^ [_124279, _124281, _124283] : [min_precedes(_124281, _124279, _124283), 595 ^ _104517 : [(596 ^ _104517) ^ [] : [-(subactivity(593 ^ [_124279, _124281, _124283], _124283))], (598 ^ _104517) ^ [] : [-(subactivity(594 ^ [_124279, _124281, _124283], _124283))], (600 ^ _104517) ^ [] : [-(atocc(_124281, 593 ^ [_124279, _124281, _124283]))], (602 ^ _104517) ^ [] : [-(atocc(_124279, 594 ^ [_124279, _124281, _124283]))]]], (604 ^ _104517) ^ [_124929, _124931] : [root(_124929, _124931), 608 ^ _104517 : [(609 ^ _104517) ^ [] : [-(subactivity(607 ^ [_124929, _124931], _124931))], (611 ^ _104517) ^ [] : [-(atocc(_124929, 607 ^ [_124929, _124931]))]]], (613 ^ _104517) ^ [_125312, _125314, _125316, _125318] : [-(min_precedes(_125314, _125312, _125318)), -(min_precedes(_125312, _125314, _125318)), -(_125314 = _125312), occurrence_of(_125316, _125318), arboreal(_125314), arboreal(_125312), subactivity_occurrence(_125314, _125316), subactivity_occurrence(_125312, _125316)], (643 ^ _104517) ^ [_126122, _126124] : [occurrence_of(_126122, _126124), 646 ^ _104517 : [(647 ^ _104517) ^ [] : [-(activity(_126124))], (649 ^ _104517) ^ [] : [-(activity_occurrence(_126122))]]], (651 ^ _104517) ^ [_126403, _126405] : [659 ^ _104517 : [(660 ^ _104517) ^ [] : [-(root(658 ^ [_126403, _126405], _126405))], (662 ^ _104517) ^ [] : [-(subactivity_occurrence(658 ^ [_126403, _126405], _126403))]], occurrence_of(_126403, _126405), -(atomic(_126405))], (664 ^ _104517) ^ [_126834] : [activity(_126834), -(subactivity(_126834, _126834))], (695 ^ _104517) ^ [] : [-(activity(tptp0))], (697 ^ _104517) ^ [] : [atomic(tptp0)], (699 ^ _104517) ^ [] : [-(atomic(tptp4))], (701 ^ _104517) ^ [] : [-(atomic(tptp1))], (703 ^ _104517) ^ [] : [-(atomic(tptp2))], (705 ^ _104517) ^ [] : [-(atomic(tptp3))], (707 ^ _104517) ^ [] : [tptp4 = tptp3], (709 ^ _104517) ^ [] : [tptp4 = tptp1], (711 ^ _104517) ^ [] : [tptp4 = tptp2], (713 ^ _104517) ^ [] : [tptp3 = tptp1], (715 ^ _104517) ^ [] : [tptp3 = tptp2], (717 ^ _104517) ^ [] : [tptp1 = tptp2], (670 ^ _104517) ^ [_127022] : [occurrence_of(_127022, tptp0), 676 ^ _104517 : [(677 ^ _104517) ^ [] : [-(occurrence_of(673 ^ [_127022], tptp3))], (679 ^ _104517) ^ [] : [-(root_occ(673 ^ [_127022], _127022))], (681 ^ _104517) ^ [] : [-(occurrence_of(674 ^ [_127022], tptp4))], (683 ^ _104517) ^ [] : [-(next_subocc(673 ^ [_127022], 674 ^ [_127022], tptp0))], (691 ^ _104517) ^ [] : [-(next_subocc(674 ^ [_127022], 675 ^ [_127022], tptp0))], (693 ^ _104517) ^ [] : [-(leaf_occ(675 ^ [_127022], _127022))], (685 ^ _104517) ^ [] : [-(occurrence_of(675 ^ [_127022], tptp1)), -(occurrence_of(675 ^ [_127022], tptp2))]]]], input).
% 0.37/1.37 ncf('1',plain,[541 : min_precedes(675 ^ [718 ^ []], 729 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0), 541 : occurrence_of(718 ^ [], tptp0), 541 : leaf_occ(675 ^ [718 ^ []], 718 ^ [])],start(533 ^ 0,bind([[_122240, _122242, _122244, _122455], [tptp0, 675 ^ [718 ^ []], 718 ^ [], 729 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]]]]))).
% 0.37/1.37 ncf('1.1',plain,[-(min_precedes(675 ^ [718 ^ []], 729 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0)), leaf_occ(675 ^ [718 ^ []], 718 ^ []), 744 : -(min_precedes(675 ^ [718 ^ []], 738 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0))],extension(722 ^ 3,bind([[_129139, _129141], [675 ^ [718 ^ []], 675 ^ [718 ^ []]]]))).
% 0.37/1.37 ncf('1.1.1',plain,[-(leaf_occ(675 ^ [718 ^ []], 718 ^ [])), occurrence_of(718 ^ [], tptp0)],extension(670 ^ 4,bind([[_127022], [718 ^ []]]))).
% 0.37/1.37 ncf('1.1.1.1',plain,[-(occurrence_of(718 ^ [], tptp0))],extension(720 ^ 5)).
% 0.37/1.37 ncf('1.1.2',plain,[min_precedes(675 ^ [718 ^ []], 738 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0)],extension(541 ^ 6,bind([[_122455], [738 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]]]]))).
% 0.37/1.37 ncf('1.2',plain,[-(occurrence_of(718 ^ [], tptp0))],extension(720 ^ 1)).
% 0.37/1.37 ncf('1.3',plain,[-(leaf_occ(675 ^ [718 ^ []], 718 ^ [])), leaf_occ(675 ^ [718 ^ []], 718 ^ []), 675 ^ [718 ^ []] = 675 ^ [718 ^ []], 718 ^ [] = 718 ^ []],extension(186 ^ 1,bind([[_110485, _110487, _110489, _110491], [718 ^ [], 718 ^ [], 675 ^ [718 ^ []], 675 ^ [718 ^ []]]]))).
% 0.37/1.37 ncf('1.3.1',plain,[-(leaf_occ(675 ^ [718 ^ []], 718 ^ [])), occurrence_of(718 ^ [], tptp0)],extension(670 ^ 2,bind([[_127022], [718 ^ []]]))).
% 0.37/1.37 ncf('1.3.1.1',plain,[-(occurrence_of(718 ^ [], tptp0))],extension(720 ^ 3)).
% 0.37/1.37 ncf('1.3.2',plain,[-(675 ^ [718 ^ []] = 675 ^ [718 ^ []])],extension(2 ^ 2,bind([[_104641], [675 ^ [718 ^ []]]]))).
% 0.37/1.37 ncf('1.3.3',plain,[-(718 ^ [] = 718 ^ [])],extension(2 ^ 2,bind([[_104641], [718 ^ []]]))).
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------