%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO010+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.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : PRO010+2 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.11 % Command : nanocop.sh %s %d
% 0.11/0.31 % Computer : n019.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Fri May 19 01:34:12 EDT 2023
% 0.16/0.31 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(720 ^ _103667) ^ [] : [-(occurrence_of(718 ^ [], tptp0))], (722 ^ _103667) ^ [_128277, _128279] : [leaf_occ(_128277, 718 ^ []), 727 ^ _103667 : [(728 ^ _103667) ^ [] : [-(occurrence_of(_128277, tptp1))], (731 ^ _103667) ^ [] : [-(occurrence_of(729 ^ [_128277, _128279], tptp2))], (733 ^ _103667) ^ [] : [-(min_precedes(_128279, 729 ^ [_128277, _128279], tptp0))]], 734 ^ _103667 : [(735 ^ _103667) ^ [] : [-(occurrence_of(_128277, tptp2))], (738 ^ _103667) ^ [] : [-(occurrence_of(736 ^ [_128277, _128279], tptp1))], (740 ^ _103667) ^ [] : [-(min_precedes(_128279, 736 ^ [_128277, _128279], tptp0))]]], (2 ^ _103667) ^ [_103791] : [-(_103791 = _103791)], (4 ^ _103667) ^ [_103898, _103900] : [_103900 = _103898, -(_103898 = _103900)], (10 ^ _103667) ^ [_104102, _104104, _104106] : [-(_104106 = _104102), _104106 = _104104, _104104 = _104102], (20 ^ _103667) ^ [_104443, _104445, _104447, _104449] : [-(precedes(_104447, _104443)), precedes(_104449, _104445), _104449 = _104447, _104445 = _104443], (34 ^ _103667) ^ [_104887, _104889, _104891, _104893] : [-(earlier(_104891, _104887)), earlier(_104893, _104889), _104893 = _104891, _104889 = _104887], (48 ^ _103667) ^ [_105303, _105305] : [-(legal(_105303)), _105305 = _105303, legal(_105305)], (58 ^ _103667) ^ [_105626, _105628, _105630, _105632] : [-(leaf(_105630, _105626)), leaf(_105632, _105628), _105632 = _105630, _105628 = _105626], (72 ^ _103667) ^ [_106070, _106072, _106074, _106076] : [-(atocc(_106074, _106070)), atocc(_106076, _106072), _106076 = _106074, _106072 = _106070], (86 ^ _103667) ^ [_106486, _106488] : [-(arboreal(_106486)), _106488 = _106486, arboreal(_106488)], (96 ^ _103667) ^ [_106781, _106783] : [-(activity_occurrence(_106781)), _106783 = _106781, activity_occurrence(_106783)], (106 ^ _103667) ^ [_107104, _107106, _107108, _107110] : [-(root(_107108, _107104)), root(_107110, _107106), _107110 = _107108, _107106 = _107104], (120 ^ _103667) ^ [_107548, _107550, _107552, _107554] : [-(subactivity_occurrence(_107552, _107548)), subactivity_occurrence(_107554, _107550), _107554 = _107552, _107550 = _107548], (134 ^ _103667) ^ [_107992, _107994, _107996, _107998] : [-(subactivity(_107996, _107992)), subactivity(_107998, _107994), _107998 = _107996, _107994 = _107992], (148 ^ _103667) ^ [_108436, _108438, _108440, _108442] : [-(root_occ(_108440, _108436)), root_occ(_108442, _108438), _108442 = _108440, _108438 = _108436], (162 ^ _103667) ^ [_108908, _108910, _108912, _108914, _108916, _108918] : [-(next_subocc(_108916, _108912, _108908)), next_subocc(_108918, _108914, _108910), _108918 = _108916, _108914 = _108912, _108910 = _108908], (180 ^ _103667) ^ [_109461, _109463] : [-(activity(_109461)), _109463 = _109461, activity(_109463)], (190 ^ _103667) ^ [_109756, _109758] : [-(atomic(_109756)), _109758 = _109756, atomic(_109758)], (200 ^ _103667) ^ [_110079, _110081, _110083, _110085] : [-(leaf_occ(_110083, _110079)), leaf_occ(_110085, _110081), _110085 = _110083, _110081 = _110079], (214 ^ _103667) ^ [_110523, _110525, _110527, _110529] : [-(occurrence_of(_110527, _110523)), occurrence_of(_110529, _110525), _110529 = _110527, _110525 = _110523], (228 ^ _103667) ^ [_110975, _110977, _110979, _110981, _110983, _110985] : [-(min_precedes(_110983, _110979, _110975)), min_precedes(_110985, _110981, _110977), _110985 = _110983, _110981 = _110979, _110977 = _110975], (246 ^ _103667) ^ [_111630, _111632, _111634, _111636] : [-(min_precedes(_111636, _111632, _111630)), min_precedes(_111636, _111634, _111630), min_precedes(_111634, _111632, _111630)], (256 ^ _103667) ^ [_111969, _111971, _111973] : [-(earlier(_111973, _111969)), earlier(_111973, _111971), earlier(_111971, _111969)], (266 ^ _103667) ^ [_112306, _112308, _112310, _112312] : [-(_112312 = _112310), occurrence_of(_112308, _112306), root_occ(_112312, _112308), root_occ(_112310, _112308)], (280 ^ _103667) ^ [_112750, _112752, _112754, _112756] : [-(_112756 = _112754), occurrence_of(_112752, _112750), -(atomic(_112750)), leaf_occ(_112756, _112752), leaf_occ(_112754, _112752)], (298 ^ _103667) ^ [_113307, _113309, _113311] : [next_subocc(_113311, _113309, _113307), 301 ^ _103667 : [(302 ^ _103667) ^ [] : [-(min_precedes(_113311, _113309, _113307))], (304 ^ _103667) ^ [_113530] : [min_precedes(_113311, _113530, _113307), min_precedes(_113530, _113309, _113307)]]], (310 ^ _103667) ^ [_113720, _113722, _113724] : [-(next_subocc(_113724, _113722, _113720)), min_precedes(_113724, _113722, _113720), 316 ^ _103667 : [(317 ^ _103667) ^ [] : [-(min_precedes(_113724, 315 ^ [_113720, _113722, _113724], _113720))], (319 ^ _103667) ^ [] : [-(min_precedes(315 ^ [_113720, _113722, _113724], _113722, _113720))]]], (323 ^ _103667) ^ [_114213, _114215, _114217] : [next_subocc(_114217, _114215, _114213), 326 ^ _103667 : [(327 ^ _103667) ^ [] : [-(arboreal(_114217))], (329 ^ _103667) ^ [] : [-(arboreal(_114215))]]], (331 ^ _103667) ^ [_114518, _114520, _114522] : [min_precedes(_114522, _114520, _114518), -(precedes(_114522, _114520))], (337 ^ _103667) ^ [_114750, _114752, _114754] : [min_precedes(_114754, _114752, _114750), root(_114752, _114750)], (343 ^ _103667) ^ [_114998, _115000] : [precedes(_115000, _114998), 346 ^ _103667 : [(347 ^ _103667) ^ [] : [-(earlier(_115000, _114998))], (349 ^ _103667) ^ [] : [-(legal(_114998))]]], (351 ^ _103667) ^ [_115233, _115235] : [-(precedes(_115235, _115233)), earlier(_115235, _115233), legal(_115233)], (361 ^ _103667) ^ [_115532, _115534] : [earlier(_115534, _115532), earlier(_115532, _115534)], (367 ^ _103667) ^ [_115772, _115774] : [root_occ(_115774, _115772), 371 ^ _103667 : [(372 ^ _103667) ^ [] : [-(occurrence_of(_115772, 370 ^ [_115772, _115774]))], (374 ^ _103667) ^ [] : [-(subactivity_occurrence(_115774, _115772))], (376 ^ _103667) ^ [] : [-(root(_115774, 370 ^ [_115772, _115774]))]]], (378 ^ _103667) ^ [_116159, _116161] : [-(root_occ(_116161, _116159)), 379 ^ _103667 : [(380 ^ _103667) ^ [_116257] : [occurrence_of(_116159, _116257), subactivity_occurrence(_116161, _116159), root(_116161, _116257)]]], (392 ^ _103667) ^ [_116651, _116653] : [leaf_occ(_116653, _116651), 396 ^ _103667 : [(397 ^ _103667) ^ [] : [-(occurrence_of(_116651, 395 ^ [_116651, _116653]))], (399 ^ _103667) ^ [] : [-(subactivity_occurrence(_116653, _116651))], (401 ^ _103667) ^ [] : [-(leaf(_116653, 395 ^ [_116651, _116653]))]]], (403 ^ _103667) ^ [_117038, _117040] : [-(leaf_occ(_117040, _117038)), 404 ^ _103667 : [(405 ^ _103667) ^ [_117136] : [occurrence_of(_117038, _117136), subactivity_occurrence(_117040, _117038), leaf(_117040, _117136)]]], (417 ^ _103667) ^ [_117501, _117503] : [root(_117503, _117501), -(legal(_117503))], (423 ^ _103667) ^ [_117709, _117711] : [occurrence_of(_117711, _117709), 426 ^ _103667 : [(427 ^ _103667) ^ [] : [arboreal(_117711), -(atomic(_117709))], (433 ^ _103667) ^ [] : [atomic(_117709), -(arboreal(_117711))]]], (439 ^ _103667) ^ [_118192, _118194] : [leaf(_118194, _118192), 442 ^ _103667 : [(450 ^ _103667) ^ [_118532] : [min_precedes(_118194, _118532, _118192)], (443 ^ _103667) ^ [] : [-(root(_118194, _118192)), -(min_precedes(446 ^ [_118192, _118194], _118194, _118192))]]], (452 ^ _103667) ^ [_118603, _118605] : [-(leaf(_118605, _118603)), 455 ^ _103667 : [(456 ^ _103667) ^ [] : [root(_118605, _118603)], (458 ^ _103667) ^ [_118793] : [min_precedes(_118793, _118605, _118603)]], -(min_precedes(_118605, 459 ^ [_118603, _118605], _118603))], (465 ^ _103667) ^ [_119093, _119095] : [atocc(_119095, _119093), 469 ^ _103667 : [(470 ^ _103667) ^ [] : [-(subactivity(_119093, 468 ^ [_119093, _119095]))], (472 ^ _103667) ^ [] : [-(atomic(468 ^ [_119093, _119095]))], (474 ^ _103667) ^ [] : [-(occurrence_of(_119095, 468 ^ [_119093, _119095]))]]], (476 ^ _103667) ^ [_119484, _119486] : [-(atocc(_119486, _119484)), 477 ^ _103667 : [(478 ^ _103667) ^ [_119581] : [subactivity(_119484, _119581), atomic(_119581), occurrence_of(_119486, _119581)]]], (490 ^ _103667) ^ [_119944, _119946] : [-(root(_119946, _119944)), atocc(_119946, _119944), legal(_119946)], (500 ^ _103667) ^ [_120227] : [legal(_120227), -(arboreal(_120227))], (506 ^ _103667) ^ [_120413] : [activity_occurrence(_120413), 510 ^ _103667 : [(511 ^ _103667) ^ [] : [-(activity(509 ^ [_120413]))], (513 ^ _103667) ^ [] : [-(occurrence_of(_120413, 509 ^ [_120413]))]]], (515 ^ _103667) ^ [_120747, _120749] : [subactivity_occurrence(_120749, _120747), 518 ^ _103667 : [(519 ^ _103667) ^ [] : [-(activity_occurrence(_120749))], (521 ^ _103667) ^ [] : [-(activity_occurrence(_120747))]]], (523 ^ _103667) ^ [_121042, _121044, _121046] : [530 ^ _103667 : [(531 ^ _103667) ^ [_121257] : [min_precedes(_121257, _121044, _121042)]], occurrence_of(_121046, _121042), root_occ(_121044, _121046)], (533 ^ _103667) ^ [_121390, _121392, _121394] : [540 ^ _103667 : [(541 ^ _103667) ^ [_121605] : [min_precedes(_121392, _121605, _121390)]], occurrence_of(_121394, _121390), leaf_occ(_121392, _121394)], (543 ^ _103667) ^ [_121738, _121740, _121742] : [-(_121740 = _121738), occurrence_of(_121742, _121740), occurrence_of(_121742, _121738)], (553 ^ _103667) ^ [_122047, _122049] : [561 ^ _103667 : [(562 ^ _103667) ^ [] : [-(occurrence_of(560 ^ [_122047, _122049], _122047))], (564 ^ _103667) ^ [] : [-(leaf_occ(_122049, 560 ^ [_122047, _122049]))]], leaf(_122049, _122047), -(atomic(_122047))], (566 ^ _103667) ^ [_122506, _122508, _122510] : [min_precedes(_122508, _122506, _122510), 570 ^ _103667 : [(571 ^ _103667) ^ [] : [-(occurrence_of(569 ^ [_122506, _122508, _122510], _122510))], (573 ^ _103667) ^ [] : [-(subactivity_occurrence(_122508, 569 ^ [_122506, _122508, _122510]))], (575 ^ _103667) ^ [] : [-(subactivity_occurrence(_122506, 569 ^ [_122506, _122508, _122510]))]]], (577 ^ _103667) ^ [_122970, _122972] : [585 ^ _103667 : [(586 ^ _103667) ^ [] : [-(occurrence_of(584 ^ [_122970, _122972], _122970))], (588 ^ _103667) ^ [] : [-(leaf_occ(_122972, 584 ^ [_122970, _122972]))]], leaf(_122972, _122970), -(atomic(_122970))], (590 ^ _103667) ^ [_123429, _123431, _123433] : [min_precedes(_123431, _123429, _123433), 595 ^ _103667 : [(596 ^ _103667) ^ [] : [-(subactivity(593 ^ [_123429, _123431, _123433], _123433))], (598 ^ _103667) ^ [] : [-(subactivity(594 ^ [_123429, _123431, _123433], _123433))], (600 ^ _103667) ^ [] : [-(atocc(_123431, 593 ^ [_123429, _123431, _123433]))], (602 ^ _103667) ^ [] : [-(atocc(_123429, 594 ^ [_123429, _123431, _123433]))]]], (604 ^ _103667) ^ [_124079, _124081] : [root(_124079, _124081), 608 ^ _103667 : [(609 ^ _103667) ^ [] : [-(subactivity(607 ^ [_124079, _124081], _124081))], (611 ^ _103667) ^ [] : [-(atocc(_124079, 607 ^ [_124079, _124081]))]]], (613 ^ _103667) ^ [_124462, _124464, _124466, _124468] : [-(min_precedes(_124464, _124462, _124468)), -(min_precedes(_124462, _124464, _124468)), -(_124464 = _124462), occurrence_of(_124466, _124468), arboreal(_124464), arboreal(_124462), subactivity_occurrence(_124464, _124466), subactivity_occurrence(_124462, _124466)], (643 ^ _103667) ^ [_125272, _125274] : [occurrence_of(_125272, _125274), 646 ^ _103667 : [(647 ^ _103667) ^ [] : [-(activity(_125274))], (649 ^ _103667) ^ [] : [-(activity_occurrence(_125272))]]], (651 ^ _103667) ^ [_125553, _125555] : [659 ^ _103667 : [(660 ^ _103667) ^ [] : [-(root(658 ^ [_125553, _125555], _125555))], (662 ^ _103667) ^ [] : [-(subactivity_occurrence(658 ^ [_125553, _125555], _125553))]], occurrence_of(_125553, _125555), -(atomic(_125555))], (664 ^ _103667) ^ [_125984] : [activity(_125984), -(subactivity(_125984, _125984))], (695 ^ _103667) ^ [] : [-(activity(tptp0))], (697 ^ _103667) ^ [] : [atomic(tptp0)], (699 ^ _103667) ^ [] : [-(atomic(tptp4))], (701 ^ _103667) ^ [] : [-(atomic(tptp1))], (703 ^ _103667) ^ [] : [-(atomic(tptp2))], (705 ^ _103667) ^ [] : [-(atomic(tptp3))], (707 ^ _103667) ^ [] : [tptp4 = tptp3], (709 ^ _103667) ^ [] : [tptp4 = tptp1], (711 ^ _103667) ^ [] : [tptp4 = tptp2], (713 ^ _103667) ^ [] : [tptp3 = tptp1], (715 ^ _103667) ^ [] : [tptp3 = tptp2], (717 ^ _103667) ^ [] : [tptp1 = tptp2], (670 ^ _103667) ^ [_126172] : [occurrence_of(_126172, tptp0), 676 ^ _103667 : [(677 ^ _103667) ^ [] : [-(occurrence_of(673 ^ [_126172], tptp3))], (679 ^ _103667) ^ [] : [-(root_occ(673 ^ [_126172], _126172))], (681 ^ _103667) ^ [] : [-(occurrence_of(674 ^ [_126172], tptp4))], (683 ^ _103667) ^ [] : [-(next_subocc(673 ^ [_126172], 674 ^ [_126172], tptp0))], (691 ^ _103667) ^ [] : [-(next_subocc(674 ^ [_126172], 675 ^ [_126172], tptp0))], (693 ^ _103667) ^ [] : [-(leaf_occ(675 ^ [_126172], _126172))], (685 ^ _103667) ^ [] : [-(occurrence_of(675 ^ [_126172], tptp1)), -(occurrence_of(675 ^ [_126172], tptp2))]]]], input).
% 0.33/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([[_121390, _121392, _121394, _121605], [tptp0, 675 ^ [718 ^ []], 718 ^ [], 729 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]]]]))).
% 0.33/1.37 ncf('1.1',plain,[-(min_precedes(675 ^ [718 ^ []], 729 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0)), leaf_occ(675 ^ [718 ^ []], 718 ^ []), 740 : -(min_precedes(675 ^ [718 ^ []], 736 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0))],extension(722 ^ 3,bind([[_128277, _128279], [675 ^ [718 ^ []], 675 ^ [718 ^ []]]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(leaf_occ(675 ^ [718 ^ []], 718 ^ [])), occurrence_of(718 ^ [], tptp0)],extension(670 ^ 4,bind([[_126172], [718 ^ []]]))).
% 0.33/1.37 ncf('1.1.1.1',plain,[-(occurrence_of(718 ^ [], tptp0))],extension(720 ^ 5)).
% 0.33/1.37 ncf('1.1.2',plain,[min_precedes(675 ^ [718 ^ []], 736 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]], tptp0)],extension(541 ^ 6,bind([[_121605], [736 ^ [675 ^ [718 ^ []], 675 ^ [718 ^ []]]]]))).
% 0.33/1.37 ncf('1.2',plain,[-(occurrence_of(718 ^ [], tptp0))],extension(720 ^ 1)).
% 0.33/1.37 ncf('1.3',plain,[-(leaf_occ(675 ^ [718 ^ []], 718 ^ [])), leaf_occ(675 ^ [718 ^ []], 718 ^ []), 675 ^ [718 ^ []] = 675 ^ [718 ^ []], 718 ^ [] = 718 ^ []],extension(200 ^ 1,bind([[_110079, _110081, _110083, _110085], [718 ^ [], 718 ^ [], 675 ^ [718 ^ []], 675 ^ [718 ^ []]]]))).
% 0.33/1.37 ncf('1.3.1',plain,[-(leaf_occ(675 ^ [718 ^ []], 718 ^ [])), occurrence_of(718 ^ [], tptp0)],extension(670 ^ 2,bind([[_126172], [718 ^ []]]))).
% 0.33/1.37 ncf('1.3.1.1',plain,[-(occurrence_of(718 ^ [], tptp0))],extension(720 ^ 3)).
% 0.33/1.37 ncf('1.3.2',plain,[-(675 ^ [718 ^ []] = 675 ^ [718 ^ []])],extension(2 ^ 2,bind([[_103791], [675 ^ [718 ^ []]]]))).
% 0.33/1.37 ncf('1.3.3',plain,[-(718 ^ [] = 718 ^ [])],extension(2 ^ 2,bind([[_103791], [718 ^ []]]))).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------