%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO012+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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:19 EDT 2023
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PRO012+2 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n018.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:41:58 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(728 ^ _105128) ^ [] : [-(occurrence_of(726 ^ [], tptp0))], (730 ^ _105128) ^ [_130051, _130053] : [occurrence_of(_130053, tptp3), root_occ(_130053, 726 ^ []), 739 ^ _105128 : [(740 ^ _105128) ^ [] : [occurrence_of(_130051, tptp2)], (742 ^ _105128) ^ [] : [occurrence_of(_130051, tptp1)]], min_precedes(_130053, _130051, tptp0)], (2 ^ _105128) ^ [_105252] : [-(_105252 = _105252)], (4 ^ _105128) ^ [_105359, _105361] : [_105361 = _105359, -(_105359 = _105361)], (10 ^ _105128) ^ [_105563, _105565, _105567] : [-(_105567 = _105563), _105567 = _105565, _105565 = _105563], (20 ^ _105128) ^ [_105932, _105934, _105936, _105938, _105940, _105942] : [-(next_subocc(_105940, _105936, _105932)), next_subocc(_105942, _105938, _105934), _105942 = _105940, _105938 = _105936, _105934 = _105932], (38 ^ _105128) ^ [_106513, _106515, _106517, _106519] : [-(precedes(_106517, _106513)), precedes(_106519, _106515), _106519 = _106517, _106515 = _106513], (52 ^ _105128) ^ [_106957, _106959, _106961, _106963] : [-(earlier(_106961, _106957)), earlier(_106963, _106959), _106963 = _106961, _106959 = _106957], (66 ^ _105128) ^ [_107373, _107375] : [-(legal(_107373)), _107375 = _107373, legal(_107375)], (76 ^ _105128) ^ [_107696, _107698, _107700, _107702] : [-(leaf(_107700, _107696)), leaf(_107702, _107698), _107702 = _107700, _107698 = _107696], (90 ^ _105128) ^ [_108140, _108142, _108144, _108146] : [-(leaf_occ(_108144, _108140)), leaf_occ(_108146, _108142), _108146 = _108144, _108142 = _108140], (104 ^ _105128) ^ [_108584, _108586, _108588, _108590] : [-(atocc(_108588, _108584)), atocc(_108590, _108586), _108590 = _108588, _108586 = _108584], (118 ^ _105128) ^ [_109000, _109002] : [-(arboreal(_109000)), _109002 = _109000, arboreal(_109002)], (128 ^ _105128) ^ [_109295, _109297] : [-(activity_occurrence(_109295)), _109297 = _109295, activity_occurrence(_109297)], (138 ^ _105128) ^ [_109618, _109620, _109622, _109624] : [-(root(_109622, _109618)), root(_109624, _109620), _109624 = _109622, _109620 = _109618], (152 ^ _105128) ^ [_110062, _110064, _110066, _110068] : [-(subactivity_occurrence(_110066, _110062)), subactivity_occurrence(_110068, _110064), _110068 = _110066, _110064 = _110062], (166 ^ _105128) ^ [_110506, _110508, _110510, _110512] : [-(subactivity(_110510, _110506)), subactivity(_110512, _110508), _110512 = _110510, _110508 = _110506], (180 ^ _105128) ^ [_110922, _110924] : [-(activity(_110922)), _110924 = _110922, activity(_110924)], (190 ^ _105128) ^ [_111217, _111219] : [-(atomic(_111217)), _111219 = _111217, atomic(_111219)], (200 ^ _105128) ^ [_111540, _111542, _111544, _111546] : [-(root_occ(_111544, _111540)), root_occ(_111546, _111542), _111546 = _111544, _111542 = _111540], (214 ^ _105128) ^ [_111984, _111986, _111988, _111990] : [-(occurrence_of(_111988, _111984)), occurrence_of(_111990, _111986), _111990 = _111988, _111986 = _111984], (228 ^ _105128) ^ [_112436, _112438, _112440, _112442, _112444, _112446] : [-(min_precedes(_112444, _112440, _112436)), min_precedes(_112446, _112442, _112438), _112446 = _112444, _112442 = _112440, _112438 = _112436], (246 ^ _105128) ^ [_113091, _113093, _113095, _113097] : [-(min_precedes(_113097, _113093, _113091)), min_precedes(_113097, _113095, _113091), min_precedes(_113095, _113093, _113091)], (256 ^ _105128) ^ [_113430, _113432, _113434] : [-(earlier(_113434, _113430)), earlier(_113434, _113432), earlier(_113432, _113430)], (266 ^ _105128) ^ [_113767, _113769, _113771, _113773] : [-(_113773 = _113771), occurrence_of(_113769, _113767), root_occ(_113773, _113769), root_occ(_113771, _113769)], (280 ^ _105128) ^ [_114211, _114213, _114215, _114217] : [-(_114217 = _114215), occurrence_of(_114213, _114211), -(atomic(_114211)), leaf_occ(_114217, _114213), leaf_occ(_114215, _114213)], (298 ^ _105128) ^ [_114768, _114770, _114772] : [next_subocc(_114772, _114770, _114768), 301 ^ _105128 : [(302 ^ _105128) ^ [] : [-(min_precedes(_114772, _114770, _114768))], (304 ^ _105128) ^ [_114991] : [min_precedes(_114772, _114991, _114768), min_precedes(_114991, _114770, _114768)]]], (310 ^ _105128) ^ [_115181, _115183, _115185] : [-(next_subocc(_115185, _115183, _115181)), min_precedes(_115185, _115183, _115181), 316 ^ _105128 : [(317 ^ _105128) ^ [] : [-(min_precedes(_115185, 315 ^ [_115181, _115183, _115185], _115181))], (319 ^ _105128) ^ [] : [-(min_precedes(315 ^ [_115181, _115183, _115185], _115183, _115181))]]], (323 ^ _105128) ^ [_115674, _115676, _115678] : [next_subocc(_115678, _115676, _115674), 326 ^ _105128 : [(327 ^ _105128) ^ [] : [-(arboreal(_115678))], (329 ^ _105128) ^ [] : [-(arboreal(_115676))]]], (331 ^ _105128) ^ [_115979, _115981, _115983] : [min_precedes(_115983, _115981, _115979), -(precedes(_115983, _115981))], (337 ^ _105128) ^ [_116211, _116213, _116215] : [min_precedes(_116215, _116213, _116211), root(_116213, _116211)], (343 ^ _105128) ^ [_116459, _116461] : [precedes(_116461, _116459), 346 ^ _105128 : [(347 ^ _105128) ^ [] : [-(earlier(_116461, _116459))], (349 ^ _105128) ^ [] : [-(legal(_116459))]]], (351 ^ _105128) ^ [_116694, _116696] : [-(precedes(_116696, _116694)), earlier(_116696, _116694), legal(_116694)], (361 ^ _105128) ^ [_116993, _116995] : [earlier(_116995, _116993), earlier(_116993, _116995)], (367 ^ _105128) ^ [_117233, _117235] : [root_occ(_117235, _117233), 371 ^ _105128 : [(372 ^ _105128) ^ [] : [-(occurrence_of(_117233, 370 ^ [_117233, _117235]))], (374 ^ _105128) ^ [] : [-(subactivity_occurrence(_117235, _117233))], (376 ^ _105128) ^ [] : [-(root(_117235, 370 ^ [_117233, _117235]))]]], (378 ^ _105128) ^ [_117620, _117622] : [-(root_occ(_117622, _117620)), 379 ^ _105128 : [(380 ^ _105128) ^ [_117718] : [occurrence_of(_117620, _117718), subactivity_occurrence(_117622, _117620), root(_117622, _117718)]]], (392 ^ _105128) ^ [_118112, _118114] : [leaf_occ(_118114, _118112), 396 ^ _105128 : [(397 ^ _105128) ^ [] : [-(occurrence_of(_118112, 395 ^ [_118112, _118114]))], (399 ^ _105128) ^ [] : [-(subactivity_occurrence(_118114, _118112))], (401 ^ _105128) ^ [] : [-(leaf(_118114, 395 ^ [_118112, _118114]))]]], (403 ^ _105128) ^ [_118499, _118501] : [-(leaf_occ(_118501, _118499)), 404 ^ _105128 : [(405 ^ _105128) ^ [_118597] : [occurrence_of(_118499, _118597), subactivity_occurrence(_118501, _118499), leaf(_118501, _118597)]]], (417 ^ _105128) ^ [_118962, _118964] : [root(_118964, _118962), -(legal(_118964))], (423 ^ _105128) ^ [_119170, _119172] : [occurrence_of(_119172, _119170), 426 ^ _105128 : [(427 ^ _105128) ^ [] : [arboreal(_119172), -(atomic(_119170))], (433 ^ _105128) ^ [] : [atomic(_119170), -(arboreal(_119172))]]], (439 ^ _105128) ^ [_119653, _119655] : [leaf(_119655, _119653), 442 ^ _105128 : [(450 ^ _105128) ^ [_119993] : [min_precedes(_119655, _119993, _119653)], (443 ^ _105128) ^ [] : [-(root(_119655, _119653)), -(min_precedes(446 ^ [_119653, _119655], _119655, _119653))]]], (452 ^ _105128) ^ [_120064, _120066] : [-(leaf(_120066, _120064)), 455 ^ _105128 : [(456 ^ _105128) ^ [] : [root(_120066, _120064)], (458 ^ _105128) ^ [_120254] : [min_precedes(_120254, _120066, _120064)]], -(min_precedes(_120066, 459 ^ [_120064, _120066], _120064))], (465 ^ _105128) ^ [_120554, _120556] : [atocc(_120556, _120554), 469 ^ _105128 : [(470 ^ _105128) ^ [] : [-(subactivity(_120554, 468 ^ [_120554, _120556]))], (472 ^ _105128) ^ [] : [-(atomic(468 ^ [_120554, _120556]))], (474 ^ _105128) ^ [] : [-(occurrence_of(_120556, 468 ^ [_120554, _120556]))]]], (476 ^ _105128) ^ [_120945, _120947] : [-(atocc(_120947, _120945)), 477 ^ _105128 : [(478 ^ _105128) ^ [_121042] : [subactivity(_120945, _121042), atomic(_121042), occurrence_of(_120947, _121042)]]], (490 ^ _105128) ^ [_121405, _121407] : [-(root(_121407, _121405)), atocc(_121407, _121405), legal(_121407)], (500 ^ _105128) ^ [_121688] : [legal(_121688), -(arboreal(_121688))], (506 ^ _105128) ^ [_121874] : [activity_occurrence(_121874), 510 ^ _105128 : [(511 ^ _105128) ^ [] : [-(activity(509 ^ [_121874]))], (513 ^ _105128) ^ [] : [-(occurrence_of(_121874, 509 ^ [_121874]))]]], (515 ^ _105128) ^ [_122208, _122210] : [subactivity_occurrence(_122210, _122208), 518 ^ _105128 : [(519 ^ _105128) ^ [] : [-(activity_occurrence(_122210))], (521 ^ _105128) ^ [] : [-(activity_occurrence(_122208))]]], (523 ^ _105128) ^ [_122503, _122505, _122507] : [530 ^ _105128 : [(531 ^ _105128) ^ [_122718] : [min_precedes(_122718, _122505, _122503)]], occurrence_of(_122507, _122503), root_occ(_122505, _122507)], (533 ^ _105128) ^ [_122851, _122853, _122855] : [540 ^ _105128 : [(541 ^ _105128) ^ [_123066] : [min_precedes(_122853, _123066, _122851)]], occurrence_of(_122855, _122851), leaf_occ(_122853, _122855)], (543 ^ _105128) ^ [_123199, _123201, _123203] : [-(_123201 = _123199), occurrence_of(_123203, _123201), occurrence_of(_123203, _123199)], (553 ^ _105128) ^ [_123508, _123510] : [561 ^ _105128 : [(562 ^ _105128) ^ [] : [-(occurrence_of(560 ^ [_123508, _123510], _123508))], (564 ^ _105128) ^ [] : [-(leaf_occ(_123510, 560 ^ [_123508, _123510]))]], leaf(_123510, _123508), -(atomic(_123508))], (566 ^ _105128) ^ [_123967, _123969, _123971] : [min_precedes(_123969, _123967, _123971), 570 ^ _105128 : [(571 ^ _105128) ^ [] : [-(occurrence_of(569 ^ [_123967, _123969, _123971], _123971))], (573 ^ _105128) ^ [] : [-(subactivity_occurrence(_123969, 569 ^ [_123967, _123969, _123971]))], (575 ^ _105128) ^ [] : [-(subactivity_occurrence(_123967, 569 ^ [_123967, _123969, _123971]))]]], (577 ^ _105128) ^ [_124431, _124433] : [585 ^ _105128 : [(586 ^ _105128) ^ [] : [-(occurrence_of(584 ^ [_124431, _124433], _124431))], (588 ^ _105128) ^ [] : [-(leaf_occ(_124433, 584 ^ [_124431, _124433]))]], leaf(_124433, _124431), -(atomic(_124431))], (590 ^ _105128) ^ [_124890, _124892, _124894] : [min_precedes(_124892, _124890, _124894), 595 ^ _105128 : [(596 ^ _105128) ^ [] : [-(subactivity(593 ^ [_124890, _124892, _124894], _124894))], (598 ^ _105128) ^ [] : [-(subactivity(594 ^ [_124890, _124892, _124894], _124894))], (600 ^ _105128) ^ [] : [-(atocc(_124892, 593 ^ [_124890, _124892, _124894]))], (602 ^ _105128) ^ [] : [-(atocc(_124890, 594 ^ [_124890, _124892, _124894]))]]], (604 ^ _105128) ^ [_125540, _125542] : [root(_125540, _125542), 608 ^ _105128 : [(609 ^ _105128) ^ [] : [-(subactivity(607 ^ [_125540, _125542], _125542))], (611 ^ _105128) ^ [] : [-(atocc(_125540, 607 ^ [_125540, _125542]))]]], (613 ^ _105128) ^ [_125923, _125925, _125927, _125929] : [-(min_precedes(_125925, _125923, _125929)), -(min_precedes(_125923, _125925, _125929)), -(_125925 = _125923), occurrence_of(_125927, _125929), arboreal(_125925), arboreal(_125923), subactivity_occurrence(_125925, _125927), subactivity_occurrence(_125923, _125927)], (643 ^ _105128) ^ [_126733, _126735] : [occurrence_of(_126733, _126735), 646 ^ _105128 : [(647 ^ _105128) ^ [] : [-(activity(_126735))], (649 ^ _105128) ^ [] : [-(activity_occurrence(_126733))]]], (651 ^ _105128) ^ [_127014, _127016] : [659 ^ _105128 : [(660 ^ _105128) ^ [] : [-(root(658 ^ [_127014, _127016], _127016))], (662 ^ _105128) ^ [] : [-(subactivity_occurrence(658 ^ [_127014, _127016], _127014))]], occurrence_of(_127014, _127016), -(atomic(_127016))], (664 ^ _105128) ^ [_127445] : [activity(_127445), -(subactivity(_127445, _127445))], (703 ^ _105128) ^ [] : [-(activity(tptp0))], (705 ^ _105128) ^ [] : [atomic(tptp0)], (707 ^ _105128) ^ [] : [-(atomic(tptp4))], (709 ^ _105128) ^ [] : [-(atomic(tptp2))], (711 ^ _105128) ^ [] : [-(atomic(tptp1))], (713 ^ _105128) ^ [] : [-(atomic(tptp3))], (715 ^ _105128) ^ [] : [tptp4 = tptp3], (717 ^ _105128) ^ [] : [tptp4 = tptp2], (719 ^ _105128) ^ [] : [tptp4 = tptp1], (721 ^ _105128) ^ [] : [tptp3 = tptp2], (723 ^ _105128) ^ [] : [tptp3 = tptp1], (725 ^ _105128) ^ [] : [tptp2 = tptp1], (670 ^ _105128) ^ [_127633] : [occurrence_of(_127633, tptp0), 676 ^ _105128 : [(677 ^ _105128) ^ [] : [-(occurrence_of(673 ^ [_127633], tptp3))], (679 ^ _105128) ^ [] : [-(root_occ(673 ^ [_127633], _127633))], (681 ^ _105128) ^ [] : [-(occurrence_of(674 ^ [_127633], tptp4))], (683 ^ _105128) ^ [] : [-(min_precedes(673 ^ [_127633], 674 ^ [_127633], tptp0))], (685 ^ _105128) ^ [] : [-(occurrence_of(675 ^ [_127633], tptp2)), -(occurrence_of(675 ^ [_127633], tptp1))], (691 ^ _105128) ^ [] : [-(min_precedes(674 ^ [_127633], 675 ^ [_127633], tptp0))], (693 ^ _105128) ^ [_128727] : [min_precedes(673 ^ [_127633], _128727, tptp0), -(_128727 = 674 ^ [_127633]), -(_128727 = 675 ^ [_127633])]]]], input).
% 0.32/1.38 ncf('1',plain,[occurrence_of(673 ^ [726 ^ []], tptp3), root_occ(673 ^ [726 ^ []], 726 ^ []), 740 : occurrence_of(675 ^ [726 ^ []], tptp2), 740 : min_precedes(673 ^ [726 ^ []], 675 ^ [726 ^ []], tptp0)],start(730 ^ 0,bind([[_130051, _130053], [675 ^ [726 ^ []], 673 ^ [726 ^ []]]]))).
% 0.32/1.38 ncf('1.1',plain,[-(occurrence_of(673 ^ [726 ^ []], tptp3)), occurrence_of(726 ^ [], tptp0)],extension(670 ^ 1,bind([[_127633], [726 ^ []]]))).
% 0.32/1.38 ncf('1.1.1',plain,[-(occurrence_of(726 ^ [], tptp0))],extension(728 ^ 2)).
% 0.32/1.38 ncf('1.2',plain,[-(root_occ(673 ^ [726 ^ []], 726 ^ [])), root_occ(673 ^ [726 ^ []], 726 ^ []), 673 ^ [726 ^ []] = 673 ^ [726 ^ []], 726 ^ [] = 726 ^ []],extension(200 ^ 1,bind([[_111540, _111542, _111544, _111546], [726 ^ [], 726 ^ [], 673 ^ [726 ^ []], 673 ^ [726 ^ []]]]))).
% 0.32/1.38 ncf('1.2.1',plain,[-(root_occ(673 ^ [726 ^ []], 726 ^ [])), occurrence_of(726 ^ [], tptp0)],extension(670 ^ 2,bind([[_127633], [726 ^ []]]))).
% 0.32/1.38 ncf('1.2.1.1',plain,[-(occurrence_of(726 ^ [], tptp0))],extension(728 ^ 3)).
% 0.32/1.38 ncf('1.2.2',plain,[-(673 ^ [726 ^ []] = 673 ^ [726 ^ []])],extension(2 ^ 2,bind([[_105252], [673 ^ [726 ^ []]]]))).
% 0.32/1.38 ncf('1.2.3',plain,[-(726 ^ [] = 726 ^ [])],extension(2 ^ 2,bind([[_105252], [726 ^ []]]))).
% 0.32/1.38 ncf('1.3',plain,[-(occurrence_of(675 ^ [726 ^ []], tptp2)), 685 : -(occurrence_of(675 ^ [726 ^ []], tptp1)), 685 : occurrence_of(726 ^ [], tptp0)],extension(670 ^ 3,bind([[_127633], [726 ^ []]]))).
% 0.32/1.38 ncf('1.3.1',plain,[occurrence_of(675 ^ [726 ^ []], tptp1)],extension(742 ^ 6)).
% 0.32/1.38 ncf('1.3.2',plain,[-(occurrence_of(726 ^ [], tptp0))],extension(728 ^ 4)).
% 0.32/1.38 ncf('1.4',plain,[-(min_precedes(673 ^ [726 ^ []], 675 ^ [726 ^ []], tptp0)), min_precedes(673 ^ [726 ^ []], 674 ^ [726 ^ []], tptp0), min_precedes(674 ^ [726 ^ []], 675 ^ [726 ^ []], tptp0)],extension(246 ^ 1,bind([[_113091, _113093, _113095, _113097], [tptp0, 675 ^ [726 ^ []], 674 ^ [726 ^ []], 673 ^ [726 ^ []]]]))).
% 0.32/1.38 ncf('1.4.1',plain,[-(min_precedes(673 ^ [726 ^ []], 674 ^ [726 ^ []], tptp0)), occurrence_of(726 ^ [], tptp0)],extension(670 ^ 2,bind([[_127633], [726 ^ []]]))).
% 0.32/1.38 ncf('1.4.1.1',plain,[-(occurrence_of(726 ^ [], tptp0))],extension(728 ^ 3)).
% 0.32/1.38 ncf('1.4.2',plain,[-(min_precedes(674 ^ [726 ^ []], 675 ^ [726 ^ []], tptp0)), occurrence_of(726 ^ [], tptp0)],extension(670 ^ 2,bind([[_127633], [726 ^ []]]))).
% 0.32/1.38 ncf('1.4.2.1',plain,[-(occurrence_of(726 ^ [], tptp0))],extension(728 ^ 3)).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------