%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO009+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:17 EDT 2023
% Result : Theorem 25.92s 26.17s
% Output : Proof 25.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : PRO009+1 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n012.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:29:16 EDT 2023
% 0.12/0.33 % CPUTime :
% 25.92/26.17
% 25.92/26.17 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 25.92/26.17 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.92/26.17 %-----------------------------------------------------
% 25.92/26.17 ncf(matrix, plain, [(771 ^ _135810) ^ [] : [-(occurrence_of(769 ^ [], tptp0))], (773 ^ _135810) ^ [_162026, _162028] : [occurrence_of(_162028, tptp3), root_occ(_162028, 769 ^ []), 782 ^ _135810 : [(783 ^ _135810) ^ [] : [occurrence_of(_162026, tptp2)], (785 ^ _135810) ^ [] : [occurrence_of(_162026, tptp1)]], min_precedes(_162028, _162026, tptp0), leaf_occ(_162026, 769 ^ [])], (2 ^ _135810) ^ [_135934] : [-(_135934 = _135934)], (4 ^ _135810) ^ [_136041, _136043] : [_136043 = _136041, -(_136041 = _136043)], (10 ^ _135810) ^ [_136245, _136247, _136249] : [-(_136249 = _136245), _136249 = _136247, _136247 = _136245], (20 ^ _135810) ^ [_136586, _136588, _136590, _136592] : [-(earlier(_136590, _136586)), earlier(_136592, _136588), _136592 = _136590, _136588 = _136586], (34 ^ _135810) ^ [_137002, _137004] : [-(legal(_137002)), _137004 = _137002, legal(_137004)], (44 ^ _135810) ^ [_137325, _137327, _137329, _137331] : [-(precedes(_137329, _137325)), precedes(_137331, _137327), _137331 = _137329, _137327 = _137325], (58 ^ _135810) ^ [_137769, _137771, _137773, _137775] : [-(atocc(_137773, _137769)), atocc(_137775, _137771), _137775 = _137773, _137771 = _137769], (72 ^ _135810) ^ [_138185, _138187] : [-(activity_occurrence(_138185)), _138187 = _138185, activity_occurrence(_138187)], (82 ^ _135810) ^ [_138480, _138482] : [-(arboreal(_138480)), _138482 = _138480, arboreal(_138482)], (92 ^ _135810) ^ [_138803, _138805, _138807, _138809] : [-(subactivity(_138807, _138803)), subactivity(_138809, _138805), _138809 = _138807, _138805 = _138803], (106 ^ _135810) ^ [_139247, _139249, _139251, _139253] : [-(root(_139251, _139247)), root(_139253, _139249), _139253 = _139251, _139249 = _139247], (120 ^ _135810) ^ [_139691, _139693, _139695, _139697] : [-(subactivity_occurrence(_139695, _139691)), subactivity_occurrence(_139697, _139693), _139697 = _139695, _139693 = _139691], (134 ^ _135810) ^ [_140135, _140137, _140139, _140141] : [-(leaf(_140139, _140135)), leaf(_140141, _140137), _140141 = _140139, _140137 = _140135], (148 ^ _135810) ^ [_140607, _140609, _140611, _140613, _140615, _140617] : [-(next_subocc(_140615, _140611, _140607)), next_subocc(_140617, _140613, _140609), _140617 = _140615, _140613 = _140611, _140609 = _140607], (166 ^ _135810) ^ [_141160, _141162] : [-(activity(_141160)), _141162 = _141160, activity(_141162)], (176 ^ _135810) ^ [_141455, _141457] : [-(atomic(_141455)), _141457 = _141455, atomic(_141457)], (186 ^ _135810) ^ [_141778, _141780, _141782, _141784] : [-(root_occ(_141782, _141778)), root_occ(_141784, _141780), _141784 = _141782, _141780 = _141778], (200 ^ _135810) ^ [_142222, _142224, _142226, _142228] : [-(occurrence_of(_142226, _142222)), occurrence_of(_142228, _142224), _142228 = _142226, _142224 = _142222], (232 ^ _135810) ^ [_143255, _143257, _143259, _143261] : [-(leaf_occ(_143259, _143255)), leaf_occ(_143261, _143257), _143261 = _143259, _143257 = _143255], (214 ^ _135810) ^ [_142694, _142696, _142698, _142700, _142702, _142704] : [-(min_precedes(_142702, _142698, _142694)), min_precedes(_142704, _142700, _142696), _142704 = _142702, _142700 = _142698, _142696 = _142694], (246 ^ _135810) ^ [_143745, _143747] : [occurrence_of(_143745, _143747), 249 ^ _135810 : [(250 ^ _135810) ^ [] : [-(activity(_143747))], (252 ^ _135810) ^ [] : [-(activity_occurrence(_143745))]]], (254 ^ _135810) ^ [_144012] : [activity_occurrence(_144012), 258 ^ _135810 : [(259 ^ _135810) ^ [] : [-(activity(257 ^ [_144012]))], (261 ^ _135810) ^ [] : [-(occurrence_of(_144012, 257 ^ [_144012]))]]], (263 ^ _135810) ^ [_144360, _144362, _144364] : [-(_144362 = _144360), occurrence_of(_144364, _144362), occurrence_of(_144364, _144360)], (273 ^ _135810) ^ [_144655] : [activity(_144655), -(subactivity(_144655, _144655))], (279 ^ _135810) ^ [_144857, _144859] : [earlier(_144859, _144857), earlier(_144857, _144859)], (285 ^ _135810) ^ [_145082, _145084, _145086] : [-(earlier(_145086, _145082)), earlier(_145086, _145084), earlier(_145084, _145082)], (295 ^ _135810) ^ [_145405, _145407, _145409] : [earlier(_145409, _145407), earlier(_145405, _145407), -(earlier(_145405, _145409)), -(earlier(_145409, _145405)), -(_145409 = _145405)], (313 ^ _135810) ^ [_145904, _145906] : [occurrence_of(_145906, _145904), 316 ^ _135810 : [(317 ^ _135810) ^ [] : [arboreal(_145906), -(atomic(_145904))], (323 ^ _135810) ^ [] : [atomic(_145904), -(arboreal(_145906))]]], (329 ^ _135810) ^ [_146344] : [legal(_146344), -(arboreal(_146344))], (335 ^ _135810) ^ [_146544, _146546] : [-(legal(_146544)), legal(_146546), earlier(_146544, _146546)], (345 ^ _135810) ^ [_146868, _146870] : [precedes(_146870, _146868), 348 ^ _135810 : [(349 ^ _135810) ^ [] : [-(earlier(_146870, _146868))], (351 ^ _135810) ^ [] : [-(legal(_146868))]]], (353 ^ _135810) ^ [_147103, _147105] : [-(precedes(_147105, _147103)), earlier(_147105, _147103), legal(_147103)], (363 ^ _135810) ^ [_147416, _147418, _147420] : [min_precedes(_147418, _147416, _147420), 368 ^ _135810 : [(369 ^ _135810) ^ [] : [-(subactivity(366 ^ [_147416, _147418, _147420], _147420))], (371 ^ _135810) ^ [] : [-(subactivity(367 ^ [_147416, _147418, _147420], _147420))], (373 ^ _135810) ^ [] : [-(atocc(_147418, 366 ^ [_147416, _147418, _147420]))], (375 ^ _135810) ^ [] : [-(atocc(_147416, 367 ^ [_147416, _147418, _147420]))]]], (377 ^ _135810) ^ [_148066, _148068] : [root(_148066, _148068), 381 ^ _135810 : [(382 ^ _135810) ^ [] : [-(subactivity(380 ^ [_148066, _148068], _148068))], (384 ^ _135810) ^ [] : [-(atocc(_148066, 380 ^ [_148066, _148068]))]]], (386 ^ _135810) ^ [_148435, _148437, _148439] : [min_precedes(_148439, _148437, _148435), 390 ^ _135810 : [(391 ^ _135810) ^ [] : [-(root(389 ^ [_148435, _148437, _148439], _148435))], (393 ^ _135810) ^ [] : [-(min_precedes(389 ^ [_148435, _148437, _148439], _148437, _148435))]]], (395 ^ _135810) ^ [_148825, _148827, _148829] : [min_precedes(_148829, _148827, _148825), root(_148827, _148825)], (401 ^ _135810) ^ [_149058, _149060, _149062] : [min_precedes(_149062, _149060, _149058), -(precedes(_149062, _149060))], (407 ^ _135810) ^ [_149276, _149278] : [root(_149278, _149276), -(legal(_149278))], (413 ^ _135810) ^ [_149484, _149486] : [-(root(_149486, _149484)), atocc(_149486, _149484), legal(_149486)], (423 ^ _135810) ^ [_149809, _149811, _149813, _149815] : [-(min_precedes(_149813, _149811, _149809)), min_precedes(_149815, _149813, _149809), min_precedes(_149815, _149811, _149809), precedes(_149813, _149811)], (437 ^ _135810) ^ [_150245, _150247, _150249] : [min_precedes(_150249, _150247, _150245), atomic(_150245)], (443 ^ _135810) ^ [_150490, _150492, _150494, _150496] : [-(min_precedes(_150494, _150492, _150490)), min_precedes(_150494, _150496, _150490), min_precedes(_150492, _150496, _150490), precedes(_150494, _150492)], (457 ^ _135810) ^ [_150941, _150943] : [leaf(_150943, _150941), 460 ^ _135810 : [(468 ^ _135810) ^ [_151281] : [min_precedes(_150943, _151281, _150941)], (461 ^ _135810) ^ [] : [-(root(_150943, _150941)), -(min_precedes(464 ^ [_150941, _150943], _150943, _150941))]]], (470 ^ _135810) ^ [_151352, _151354] : [-(leaf(_151354, _151352)), 473 ^ _135810 : [(474 ^ _135810) ^ [] : [root(_151354, _151352)], (476 ^ _135810) ^ [_151542] : [min_precedes(_151542, _151354, _151352)]], -(min_precedes(_151354, 477 ^ [_151352, _151354], _151352))], (483 ^ _135810) ^ [_151856, _151858, _151860] : [next_subocc(_151860, _151858, _151856), 486 ^ _135810 : [(487 ^ _135810) ^ [] : [-(min_precedes(_151860, _151858, _151856))], (489 ^ _135810) ^ [_152079] : [min_precedes(_151860, _152079, _151856), min_precedes(_152079, _151858, _151856)]]], (495 ^ _135810) ^ [_152269, _152271, _152273] : [-(next_subocc(_152273, _152271, _152269)), min_precedes(_152273, _152271, _152269), 501 ^ _135810 : [(502 ^ _135810) ^ [] : [-(min_precedes(_152273, 500 ^ [_152269, _152271, _152273], _152269))], (504 ^ _135810) ^ [] : [-(min_precedes(500 ^ [_152269, _152271, _152273], _152271, _152269))]]], (508 ^ _135810) ^ [_152777, _152779] : [atocc(_152779, _152777), 512 ^ _135810 : [(513 ^ _135810) ^ [] : [-(subactivity(_152777, 511 ^ [_152777, _152779]))], (515 ^ _135810) ^ [] : [-(atomic(511 ^ [_152777, _152779]))], (517 ^ _135810) ^ [] : [-(occurrence_of(_152779, 511 ^ [_152777, _152779]))]]], (519 ^ _135810) ^ [_153168, _153170] : [-(atocc(_153170, _153168)), 520 ^ _135810 : [(521 ^ _135810) ^ [_153265] : [subactivity(_153168, _153265), atomic(_153265), occurrence_of(_153170, _153265)]]], (533 ^ _135810) ^ [_153628, _153630] : [subactivity_occurrence(_153630, _153628), 536 ^ _135810 : [(537 ^ _135810) ^ [] : [-(activity_occurrence(_153630))], (539 ^ _135810) ^ [] : [-(activity_occurrence(_153628))]]], (541 ^ _135810) ^ [_153923, _153925, _153927] : [min_precedes(_153925, _153923, _153927), 545 ^ _135810 : [(546 ^ _135810) ^ [] : [-(occurrence_of(544 ^ [_153923, _153925, _153927], _153927))], (548 ^ _135810) ^ [] : [-(subactivity_occurrence(_153925, 544 ^ [_153923, _153925, _153927]))], (550 ^ _135810) ^ [] : [-(subactivity_occurrence(_153923, 544 ^ [_153923, _153925, _153927]))]]], (552 ^ _135810) ^ [_154387, _154389] : [560 ^ _135810 : [(561 ^ _135810) ^ [] : [-(occurrence_of(559 ^ [_154387, _154389], _154389))], (563 ^ _135810) ^ [] : [-(subactivity_occurrence(_154387, 559 ^ [_154387, _154389]))]], root(_154387, _154389), -(atomic(_154389))], (565 ^ _135810) ^ [_154832, _154834] : [573 ^ _135810 : [(574 ^ _135810) ^ [] : [-(root(572 ^ [_154832, _154834], _154834))], (576 ^ _135810) ^ [] : [-(subactivity_occurrence(572 ^ [_154832, _154834], _154832))]], occurrence_of(_154832, _154834), -(atomic(_154834))], (578 ^ _135810) ^ [_155305, _155307, _155309, _155311] : [-(min_precedes(_155307, _155305, _155311)), -(min_precedes(_155305, _155307, _155311)), -(_155307 = _155305), occurrence_of(_155309, _155311), arboreal(_155307), arboreal(_155305), subactivity_occurrence(_155307, _155309), subactivity_occurrence(_155305, _155309)], (608 ^ _135810) ^ [_156143, _156145, _156147, _156149] : [-(subactivity_occurrence(_156149, _156143)), min_precedes(_156149, _156147, _156145), occurrence_of(_156143, _156145), subactivity_occurrence(_156147, _156143)], (622 ^ _135810) ^ [_156589, _156591, _156593, _156595] : [-(subactivity(_156595, _156593)), occurrence_of(_156591, _156595), occurrence_of(_156589, _156593), -(atomic(_156595)), subactivity_occurrence(_156591, _156589)], (640 ^ _135810) ^ [_157117, _157119, _157121] : [-(subactivity_occurrence(_157121, _157117)), subactivity_occurrence(_157121, _157119), subactivity_occurrence(_157119, _157117)], (650 ^ _135810) ^ [_157454, _157456, _157458, _157460] : [666 ^ _135810 : [(667 ^ _135810) ^ [] : [-(subactivity_occurrence(665 ^ [_157454, _157456, _157458, _157460], _157454))], (669 ^ _135810) ^ [] : [subactivity_occurrence(665 ^ [_157454, _157456, _157458, _157460], _157456)]], occurrence_of(_157456, _157460), occurrence_of(_157454, _157458), subactivity(_157460, _157458), -(subactivity_occurrence(_157456, _157454))], (671 ^ _135810) ^ [_158167, _158169] : [root_occ(_158169, _158167), 675 ^ _135810 : [(676 ^ _135810) ^ [] : [-(occurrence_of(_158167, 674 ^ [_158167, _158169]))], (678 ^ _135810) ^ [] : [-(subactivity_occurrence(_158169, _158167))], (680 ^ _135810) ^ [] : [-(root(_158169, 674 ^ [_158167, _158169]))]]], (682 ^ _135810) ^ [_158554, _158556] : [-(root_occ(_158556, _158554)), 683 ^ _135810 : [(684 ^ _135810) ^ [_158652] : [occurrence_of(_158554, _158652), subactivity_occurrence(_158556, _158554), root(_158556, _158652)]]], (746 ^ _135810) ^ [] : [-(activity(tptp0))], (748 ^ _135810) ^ [] : [atomic(tptp0)], (750 ^ _135810) ^ [] : [-(atomic(tptp4))], (752 ^ _135810) ^ [] : [-(atomic(tptp2))], (754 ^ _135810) ^ [] : [-(atomic(tptp1))], (756 ^ _135810) ^ [] : [-(atomic(tptp3))], (758 ^ _135810) ^ [] : [tptp4 = tptp3], (760 ^ _135810) ^ [] : [tptp4 = tptp2], (762 ^ _135810) ^ [] : [tptp4 = tptp1], (764 ^ _135810) ^ [] : [tptp3 = tptp2], (766 ^ _135810) ^ [] : [tptp3 = tptp1], (768 ^ _135810) ^ [] : [tptp2 = tptp1], (721 ^ _135810) ^ [_159882] : [occurrence_of(_159882, tptp0), 727 ^ _135810 : [(728 ^ _135810) ^ [] : [-(occurrence_of(724 ^ [_159882], tptp3))], (730 ^ _135810) ^ [] : [-(root_occ(724 ^ [_159882], _159882))], (732 ^ _135810) ^ [] : [-(occurrence_of(725 ^ [_159882], tptp4))], (734 ^ _135810) ^ [] : [-(next_subocc(724 ^ [_159882], 725 ^ [_159882], tptp0))], (742 ^ _135810) ^ [] : [-(next_subocc(725 ^ [_159882], 726 ^ [_159882], tptp0))], (744 ^ _135810) ^ [] : [-(leaf_occ(726 ^ [_159882], _159882))], (736 ^ _135810) ^ [] : [-(occurrence_of(726 ^ [_159882], tptp2)), -(occurrence_of(726 ^ [_159882], tptp1))]]], (696 ^ _135810) ^ [_159046, _159048] : [leaf_occ(_159048, _159046), 700 ^ _135810 : [(701 ^ _135810) ^ [] : [-(occurrence_of(_159046, 699 ^ [_159046, _159048]))], (703 ^ _135810) ^ [] : [-(subactivity_occurrence(_159048, _159046))], (705 ^ _135810) ^ [] : [-(leaf(_159048, 699 ^ [_159046, _159048]))]]], (707 ^ _135810) ^ [_159433, _159435] : [-(leaf_occ(_159435, _159433)), 708 ^ _135810 : [(709 ^ _135810) ^ [_159531] : [occurrence_of(_159433, _159531), subactivity_occurrence(_159435, _159433), leaf(_159435, _159531)]]]], input).
% 25.92/26.17 ncf('1',plain,[occurrence_of(724 ^ [769 ^ []], tptp3), root_occ(724 ^ [769 ^ []], 769 ^ []), 783 : occurrence_of(726 ^ [769 ^ []], tptp2), 783 : min_precedes(724 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0), 783 : leaf_occ(726 ^ [769 ^ []], 769 ^ [])],start(773 ^ 0,bind([[_162026, _162028], [726 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.1',plain,[-(occurrence_of(724 ^ [769 ^ []], tptp3)), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 1,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 2)).
% 25.92/26.17 ncf('1.2',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), root_occ(724 ^ [769 ^ []], 769 ^ []), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(186 ^ 1,bind([[_141778, _141780, _141782, _141784], [769 ^ [], 769 ^ [], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), root_occ(724 ^ [769 ^ []], 769 ^ []), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(186 ^ 2,bind([[_141778, _141780, _141782, _141784], [769 ^ [], 769 ^ [], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), root_occ(724 ^ [769 ^ []], 769 ^ []), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(186 ^ 3,bind([[_141778, _141780, _141782, _141784], [769 ^ [], 769 ^ [], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), root_occ(724 ^ [769 ^ []], 769 ^ []), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(186 ^ 4,bind([[_141778, _141780, _141782, _141784], [769 ^ [], 769 ^ [], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1.1.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), root_occ(724 ^ [769 ^ []], 769 ^ []), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(186 ^ 5,bind([[_141778, _141780, _141782, _141784], [769 ^ [], 769 ^ [], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1.1.1.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.2.1.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.2.1.1.1.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 6,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 6,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.2.1.1.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 5,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.2.1.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 4,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 4,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.2.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 3,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 3,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.2.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 2,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.2.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 2,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.3',plain,[-(occurrence_of(726 ^ [769 ^ []], tptp2)), 736 : -(occurrence_of(726 ^ [769 ^ []], tptp1)), 736 : occurrence_of(769 ^ [], tptp0)],extension(721 ^ 3,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.3.1',plain,[occurrence_of(726 ^ [769 ^ []], tptp1)],extension(785 ^ 6)).
% 25.92/26.17 ncf('1.3.2',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 4)).
% 25.92/26.17 ncf('1.4',plain,[-(min_precedes(724 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)), -(min_precedes(726 ^ [769 ^ []], 724 ^ [769 ^ []], tptp0)), -(724 ^ [769 ^ []] = 726 ^ [769 ^ []]), occurrence_of(769 ^ [], tptp0), arboreal(724 ^ [769 ^ []]), arboreal(726 ^ [769 ^ []]), subactivity_occurrence(724 ^ [769 ^ []], 769 ^ []), subactivity_occurrence(726 ^ [769 ^ []], 769 ^ [])],extension(578 ^ 1,bind([[_155305, _155307, _155309, _155311], [726 ^ [769 ^ []], 724 ^ [769 ^ []], 769 ^ [], tptp0]]))).
% 25.92/26.17 ncf('1.4.1',plain,[min_precedes(726 ^ [769 ^ []], 724 ^ [769 ^ []], tptp0), leaf(726 ^ [769 ^ []], tptp0)],extension(457 ^ 2,bind([[_150941, _150943, _151281], [tptp0, 726 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1',plain,[-(leaf(726 ^ [769 ^ []], tptp0)), leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]] = tptp0],extension(134 ^ 3,bind([[_140135, _140137, _140139, _140141], [tptp0, 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1.1',plain,[-(leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]]],extension(134 ^ 4,bind([[_140135, _140137, _140139, _140141], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1.1.1',plain,[-(leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 5,bind([[_159046, _159048], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.1.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.1.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(2 ^ 5,bind([[_135934], [699 ^ [769 ^ [], 726 ^ [769 ^ []]]]]))).
% 25.92/26.17 ncf('1.4.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 4,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = tptp0), occurrence_of(769 ^ [], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), occurrence_of(769 ^ [], tptp0)],extension(263 ^ 4,bind([[_144360, _144362, _144364], [tptp0, 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 769 ^ []]]))).
% 25.92/26.17 ncf('1.4.1.1.3.1',plain,[-(occurrence_of(769 ^ [], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 5,bind([[_159046, _159048], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.1.1.3.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.1.1.3.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.1.1.3.2',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 5)).
% 25.92/26.17 ncf('1.4.2',plain,[724 ^ [769 ^ []] = 726 ^ [769 ^ []], -(726 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(4 ^ 2,bind([[_136041, _136043], [726 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1',plain,[726 ^ [769 ^ []] = 724 ^ [769 ^ []], -(leaf(724 ^ [769 ^ []], tptp0)), leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 699 ^ [769 ^ [], 726 ^ [769 ^ []]] = tptp0],extension(134 ^ 3,bind([[_140135, _140137, _140139, _140141], [tptp0, 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 724 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.1',plain,[leaf(724 ^ [769 ^ []], tptp0), 468 : min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)],extension(457 ^ 4,bind([[_150941, _150943, _151281], [tptp0, 724 ^ [769 ^ []], 725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.1.1',plain,[-(min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)), next_subocc(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)],extension(483 ^ 7,bind([[_151856, _151858, _151860], [tptp0, 725 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.1.1.1',plain,[-(next_subocc(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 8,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.2.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 9)).
% 25.92/26.17 ncf('1.4.2.1.2',plain,[-(leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]]],extension(134 ^ 4,bind([[_140135, _140137, _140139, _140141], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.2.1',plain,[-(leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 5,bind([[_159046, _159048], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.2.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.2.1.2.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.2.1.2.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.2.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(2 ^ 5,bind([[_135934], [699 ^ [769 ^ [], 726 ^ [769 ^ []]]]]))).
% 25.92/26.17 ncf('1.4.2.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = tptp0), occurrence_of(769 ^ [], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), occurrence_of(769 ^ [], tptp0)],extension(263 ^ 4,bind([[_144360, _144362, _144364], [tptp0, 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 769 ^ []]]))).
% 25.92/26.17 ncf('1.4.2.1.3.1',plain,[-(occurrence_of(769 ^ [], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 5,bind([[_159046, _159048], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.2.1.3.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.2.1.3.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.2.1.3.2',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 5)).
% 25.92/26.17 ncf('1.4.3',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 2)).
% 25.92/26.17 ncf('1.4.4',plain,[-(arboreal(724 ^ [769 ^ []])), legal(724 ^ [769 ^ []])],extension(329 ^ 2,bind([[_146344], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.4.1',plain,[-(legal(724 ^ [769 ^ []])), root(724 ^ [769 ^ []], 674 ^ [769 ^ [], 724 ^ [769 ^ []]])],extension(407 ^ 3,bind([[_149276, _149278], [674 ^ [769 ^ [], 724 ^ [769 ^ []]], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.4.1.1',plain,[-(root(724 ^ [769 ^ []], 674 ^ [769 ^ [], 724 ^ [769 ^ []]])), root_occ(724 ^ [769 ^ []], 769 ^ [])],extension(671 ^ 4,bind([[_158167, _158169], [769 ^ [], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.4.1.1.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), root_occ(724 ^ [769 ^ []], 769 ^ []), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(186 ^ 5,bind([[_141778, _141780, _141782, _141784], [769 ^ [], 769 ^ [], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.4.1.1.1.1',plain,[-(root_occ(724 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.4.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.4.1.1.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 6,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.4.1.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 6,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.5',plain,[-(arboreal(726 ^ [769 ^ []])), legal(726 ^ [769 ^ []])],extension(329 ^ 2,bind([[_146344], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.5.1',plain,[-(legal(726 ^ [769 ^ []])), precedes(725 ^ [769 ^ []], 726 ^ [769 ^ []])],extension(345 ^ 3,bind([[_146868, _146870], [726 ^ [769 ^ []], 725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.5.1.1',plain,[-(precedes(725 ^ [769 ^ []], 726 ^ [769 ^ []])), min_precedes(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)],extension(401 ^ 4,bind([[_149058, _149060, _149062], [tptp0, 726 ^ [769 ^ []], 725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.5.1.1.1',plain,[-(min_precedes(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)), next_subocc(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)],extension(483 ^ 5,bind([[_151856, _151858, _151860], [tptp0, 726 ^ [769 ^ []], 725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.5.1.1.1.1',plain,[-(next_subocc(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.5.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],lemmata('[1].x')).
% 25.92/26.17 ncf('1.4.6',plain,[-(subactivity_occurrence(724 ^ [769 ^ []], 769 ^ [])), min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0), occurrence_of(769 ^ [], tptp0), subactivity_occurrence(725 ^ [769 ^ []], 769 ^ [])],extension(608 ^ 2,bind([[_156143, _156145, _156147, _156149], [769 ^ [], tptp0, 725 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1',plain,[-(min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)), min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 725 ^ [769 ^ []] = 725 ^ [769 ^ []], tptp0 = tptp0],extension(214 ^ 3,bind([[_142694, _142696, _142698, _142700, _142702, _142704], [tptp0, tptp0, 725 ^ [769 ^ []], 725 ^ [769 ^ []], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.1',plain,[-(min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)), min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0), 724 ^ [769 ^ []] = 724 ^ [769 ^ []], 725 ^ [769 ^ []] = 725 ^ [769 ^ []], tptp0 = tptp0],extension(214 ^ 4,bind([[_142694, _142696, _142698, _142700, _142702, _142704], [tptp0, tptp0, 725 ^ [769 ^ []], 725 ^ [769 ^ []], 724 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.1.1',plain,[-(min_precedes(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)), next_subocc(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)],extension(483 ^ 5,bind([[_151856, _151858, _151860], [tptp0, 725 ^ [769 ^ []], 724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.1.1.1',plain,[-(next_subocc(724 ^ [769 ^ []], 725 ^ [769 ^ []], tptp0)), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.6.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.6.1.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.1.3',plain,[-(725 ^ [769 ^ []] = 725 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.1.4',plain,[-(tptp0 = tptp0)],extension(2 ^ 5,bind([[_135934], [tptp0]]))).
% 25.92/26.17 ncf('1.4.6.1.2',plain,[-(724 ^ [769 ^ []] = 724 ^ [769 ^ []])],extension(2 ^ 4,bind([[_135934], [724 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.3',plain,[-(725 ^ [769 ^ []] = 725 ^ [769 ^ []])],extension(2 ^ 4,bind([[_135934], [725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.1.4',plain,[-(tptp0 = tptp0)],extension(2 ^ 4,bind([[_135934], [tptp0]]))).
% 25.92/26.17 ncf('1.4.6.2',plain,[-(occurrence_of(769 ^ [], tptp0))],lemmata('[1].x')).
% 25.92/26.17 ncf('1.4.6.3',plain,[-(subactivity_occurrence(725 ^ [769 ^ []], 769 ^ [])), min_precedes(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0), occurrence_of(769 ^ [], tptp0), subactivity_occurrence(726 ^ [769 ^ []], 769 ^ [])],extension(608 ^ 3,bind([[_156143, _156145, _156147, _156149], [769 ^ [], tptp0, 726 ^ [769 ^ []], 725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.3.1',plain,[-(min_precedes(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)), next_subocc(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)],extension(483 ^ 4,bind([[_151856, _151858, _151860], [tptp0, 726 ^ [769 ^ []], 725 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.3.1.1',plain,[-(next_subocc(725 ^ [769 ^ []], 726 ^ [769 ^ []], tptp0)), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 5,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.6.3.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],lemmata('[4, 1].x')).
% 25.92/26.17 ncf('1.4.6.3.2',plain,[-(occurrence_of(769 ^ [], tptp0))],lemmata('[4, 1].x')).
% 25.92/26.17 ncf('1.4.6.3.3',plain,[-(subactivity_occurrence(726 ^ [769 ^ []], 769 ^ [])), subactivity_occurrence(726 ^ [769 ^ []], 769 ^ []), subactivity_occurrence(769 ^ [], 769 ^ [])],extension(640 ^ 4,bind([[_157117, _157119, _157121], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.3.3.1',plain,[-(subactivity_occurrence(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 5,bind([[_159046, _159048], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.6.3.3.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.6.3.3.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],lemmata('[6, 4, 1].x')).
% 25.92/26.17 ncf('1.4.6.3.3.2',plain,[-(subactivity_occurrence(769 ^ [], 769 ^ [])), 667 : -(subactivity_occurrence(665 ^ [769 ^ [], 769 ^ [], tptp0, tptp0], 769 ^ [])), 667 : occurrence_of(769 ^ [], tptp0), 667 : occurrence_of(769 ^ [], tptp0), 667 : subactivity(tptp0, tptp0)],extension(650 ^ 5,bind([[_157454, _157456, _157458, _157460], [769 ^ [], 769 ^ [], tptp0, tptp0]]))).
% 25.92/26.17 ncf('1.4.6.3.3.2.1',plain,[subactivity_occurrence(665 ^ [769 ^ [], 769 ^ [], tptp0, tptp0], 769 ^ [])],extension(669 ^ 8)).
% 25.92/26.17 ncf('1.4.6.3.3.2.2',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 6)).
% 25.92/26.17 ncf('1.4.6.3.3.2.3',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 6)).
% 25.92/26.17 ncf('1.4.6.3.3.2.4',plain,[-(subactivity(tptp0, tptp0)), activity(tptp0)],extension(273 ^ 6,bind([[_144655], [tptp0]]))).
% 25.92/26.17 ncf('1.4.6.3.3.2.4.1',plain,[-(activity(tptp0))],extension(746 ^ 7)).
% 25.92/26.17 ncf('1.4.7',plain,[-(subactivity_occurrence(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 2,bind([[_159046, _159048], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 3,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 4,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 5,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.7.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.4.7.1.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 6,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 6,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.7.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 5,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.4.7.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 4,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.4.7.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 4,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.5',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 1,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 2,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 3,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 4,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 769 ^ [] = 769 ^ []],extension(232 ^ 5,bind([[_143255, _143257, _143259, _143261], [769 ^ [], 769 ^ [], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 6,bind([[_159882], [769 ^ []]]))).
% 25.92/26.17 ncf('1.5.1.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 7)).
% 25.92/26.17 ncf('1.5.1.1.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 6,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 6,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.5.1.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 5,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 5,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.5.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 4,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 4,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.5.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 3,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.1.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 3,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 ncf('1.5.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 2,bind([[_135934], [726 ^ [769 ^ []]]]))).
% 25.92/26.17 ncf('1.5.3',plain,[-(769 ^ [] = 769 ^ [])],extension(2 ^ 2,bind([[_135934], [769 ^ []]]))).
% 25.92/26.17 %-----------------------------------------------------
% 25.92/26.17 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------