%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO010+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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 7.85s 8.60s
% Output : Proof 7.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : PRO010+1 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n006.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri May 19 01:32:21 EDT 2023
% 0.11/0.33 % CPUTime :
% 7.85/8.60
% 7.85/8.60 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 7.85/8.60 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.85/8.60 %-----------------------------------------------------
% 7.85/8.60 ncf(matrix, plain, [(771 ^ _116140) ^ [] : [-(occurrence_of(769 ^ [], tptp0))], (773 ^ _116140) ^ [_142377, _142379] : [leaf_occ(_142377, 769 ^ []), 778 ^ _116140 : [(779 ^ _116140) ^ [] : [-(occurrence_of(_142377, tptp1))], (782 ^ _116140) ^ [] : [-(occurrence_of(780 ^ [_142377, _142379], tptp2))], (784 ^ _116140) ^ [] : [-(min_precedes(_142379, 780 ^ [_142377, _142379], tptp0))]], 785 ^ _116140 : [(786 ^ _116140) ^ [] : [-(occurrence_of(_142377, tptp2))], (789 ^ _116140) ^ [] : [-(occurrence_of(787 ^ [_142377, _142379], tptp1))], (791 ^ _116140) ^ [] : [-(min_precedes(_142379, 787 ^ [_142377, _142379], tptp0))]]], (2 ^ _116140) ^ [_116264] : [-(_116264 = _116264)], (4 ^ _116140) ^ [_116371, _116373] : [_116373 = _116371, -(_116371 = _116373)], (10 ^ _116140) ^ [_116575, _116577, _116579] : [-(_116579 = _116575), _116579 = _116577, _116577 = _116575], (20 ^ _116140) ^ [_116916, _116918, _116920, _116922] : [-(earlier(_116920, _116916)), earlier(_116922, _116918), _116922 = _116920, _116918 = _116916], (34 ^ _116140) ^ [_117332, _117334] : [-(legal(_117332)), _117334 = _117332, legal(_117334)], (44 ^ _116140) ^ [_117655, _117657, _117659, _117661] : [-(precedes(_117659, _117655)), precedes(_117661, _117657), _117661 = _117659, _117657 = _117655], (58 ^ _116140) ^ [_118099, _118101, _118103, _118105] : [-(atocc(_118103, _118099)), atocc(_118105, _118101), _118105 = _118103, _118101 = _118099], (72 ^ _116140) ^ [_118515, _118517] : [-(activity_occurrence(_118515)), _118517 = _118515, activity_occurrence(_118517)], (82 ^ _116140) ^ [_118810, _118812] : [-(arboreal(_118810)), _118812 = _118810, arboreal(_118812)], (92 ^ _116140) ^ [_119133, _119135, _119137, _119139] : [-(subactivity(_119137, _119133)), subactivity(_119139, _119135), _119139 = _119137, _119135 = _119133], (106 ^ _116140) ^ [_119577, _119579, _119581, _119583] : [-(root(_119581, _119577)), root(_119583, _119579), _119583 = _119581, _119579 = _119577], (120 ^ _116140) ^ [_120021, _120023, _120025, _120027] : [-(subactivity_occurrence(_120025, _120021)), subactivity_occurrence(_120027, _120023), _120027 = _120025, _120023 = _120021], (134 ^ _116140) ^ [_120465, _120467, _120469, _120471] : [-(leaf(_120469, _120465)), leaf(_120471, _120467), _120471 = _120469, _120467 = _120465], (148 ^ _116140) ^ [_120909, _120911, _120913, _120915] : [-(root_occ(_120913, _120909)), root_occ(_120915, _120911), _120915 = _120913, _120911 = _120909], (162 ^ _116140) ^ [_121381, _121383, _121385, _121387, _121389, _121391] : [-(next_subocc(_121389, _121385, _121381)), next_subocc(_121391, _121387, _121383), _121391 = _121389, _121387 = _121385, _121383 = _121381], (180 ^ _116140) ^ [_121934, _121936] : [-(activity(_121934)), _121936 = _121934, activity(_121936)], (190 ^ _116140) ^ [_122229, _122231] : [-(atomic(_122229)), _122231 = _122229, atomic(_122231)], (200 ^ _116140) ^ [_122552, _122554, _122556, _122558] : [-(leaf_occ(_122556, _122552)), leaf_occ(_122558, _122554), _122558 = _122556, _122554 = _122552], (214 ^ _116140) ^ [_122996, _122998, _123000, _123002] : [-(occurrence_of(_123000, _122996)), occurrence_of(_123002, _122998), _123002 = _123000, _122998 = _122996], (228 ^ _116140) ^ [_123448, _123450, _123452, _123454, _123456, _123458] : [-(min_precedes(_123456, _123452, _123448)), min_precedes(_123458, _123454, _123450), _123458 = _123456, _123454 = _123452, _123450 = _123448], (246 ^ _116140) ^ [_124075, _124077] : [occurrence_of(_124075, _124077), 249 ^ _116140 : [(250 ^ _116140) ^ [] : [-(activity(_124077))], (252 ^ _116140) ^ [] : [-(activity_occurrence(_124075))]]], (254 ^ _116140) ^ [_124342] : [activity_occurrence(_124342), 258 ^ _116140 : [(259 ^ _116140) ^ [] : [-(activity(257 ^ [_124342]))], (261 ^ _116140) ^ [] : [-(occurrence_of(_124342, 257 ^ [_124342]))]]], (263 ^ _116140) ^ [_124690, _124692, _124694] : [-(_124692 = _124690), occurrence_of(_124694, _124692), occurrence_of(_124694, _124690)], (273 ^ _116140) ^ [_124985] : [activity(_124985), -(subactivity(_124985, _124985))], (279 ^ _116140) ^ [_125187, _125189] : [earlier(_125189, _125187), earlier(_125187, _125189)], (285 ^ _116140) ^ [_125412, _125414, _125416] : [-(earlier(_125416, _125412)), earlier(_125416, _125414), earlier(_125414, _125412)], (295 ^ _116140) ^ [_125735, _125737, _125739] : [earlier(_125739, _125737), earlier(_125735, _125737), -(earlier(_125735, _125739)), -(earlier(_125739, _125735)), -(_125739 = _125735)], (313 ^ _116140) ^ [_126234, _126236] : [occurrence_of(_126236, _126234), 316 ^ _116140 : [(317 ^ _116140) ^ [] : [arboreal(_126236), -(atomic(_126234))], (323 ^ _116140) ^ [] : [atomic(_126234), -(arboreal(_126236))]]], (329 ^ _116140) ^ [_126674] : [legal(_126674), -(arboreal(_126674))], (335 ^ _116140) ^ [_126874, _126876] : [-(legal(_126874)), legal(_126876), earlier(_126874, _126876)], (345 ^ _116140) ^ [_127198, _127200] : [precedes(_127200, _127198), 348 ^ _116140 : [(349 ^ _116140) ^ [] : [-(earlier(_127200, _127198))], (351 ^ _116140) ^ [] : [-(legal(_127198))]]], (353 ^ _116140) ^ [_127433, _127435] : [-(precedes(_127435, _127433)), earlier(_127435, _127433), legal(_127433)], (363 ^ _116140) ^ [_127746, _127748, _127750] : [min_precedes(_127748, _127746, _127750), 368 ^ _116140 : [(369 ^ _116140) ^ [] : [-(subactivity(366 ^ [_127746, _127748, _127750], _127750))], (371 ^ _116140) ^ [] : [-(subactivity(367 ^ [_127746, _127748, _127750], _127750))], (373 ^ _116140) ^ [] : [-(atocc(_127748, 366 ^ [_127746, _127748, _127750]))], (375 ^ _116140) ^ [] : [-(atocc(_127746, 367 ^ [_127746, _127748, _127750]))]]], (377 ^ _116140) ^ [_128396, _128398] : [root(_128396, _128398), 381 ^ _116140 : [(382 ^ _116140) ^ [] : [-(subactivity(380 ^ [_128396, _128398], _128398))], (384 ^ _116140) ^ [] : [-(atocc(_128396, 380 ^ [_128396, _128398]))]]], (386 ^ _116140) ^ [_128765, _128767, _128769] : [min_precedes(_128769, _128767, _128765), 390 ^ _116140 : [(391 ^ _116140) ^ [] : [-(root(389 ^ [_128765, _128767, _128769], _128765))], (393 ^ _116140) ^ [] : [-(min_precedes(389 ^ [_128765, _128767, _128769], _128767, _128765))]]], (395 ^ _116140) ^ [_129155, _129157, _129159] : [min_precedes(_129159, _129157, _129155), root(_129157, _129155)], (401 ^ _116140) ^ [_129388, _129390, _129392] : [min_precedes(_129392, _129390, _129388), -(precedes(_129392, _129390))], (407 ^ _116140) ^ [_129606, _129608] : [root(_129608, _129606), -(legal(_129608))], (413 ^ _116140) ^ [_129814, _129816] : [-(root(_129816, _129814)), atocc(_129816, _129814), legal(_129816)], (423 ^ _116140) ^ [_130139, _130141, _130143, _130145] : [-(min_precedes(_130143, _130141, _130139)), min_precedes(_130145, _130143, _130139), min_precedes(_130145, _130141, _130139), precedes(_130143, _130141)], (437 ^ _116140) ^ [_130575, _130577, _130579] : [min_precedes(_130579, _130577, _130575), atomic(_130575)], (443 ^ _116140) ^ [_130820, _130822, _130824, _130826] : [-(min_precedes(_130824, _130822, _130820)), min_precedes(_130824, _130826, _130820), min_precedes(_130822, _130826, _130820), precedes(_130824, _130822)], (457 ^ _116140) ^ [_131271, _131273] : [leaf(_131273, _131271), 460 ^ _116140 : [(468 ^ _116140) ^ [_131611] : [min_precedes(_131273, _131611, _131271)], (461 ^ _116140) ^ [] : [-(root(_131273, _131271)), -(min_precedes(464 ^ [_131271, _131273], _131273, _131271))]]], (470 ^ _116140) ^ [_131682, _131684] : [-(leaf(_131684, _131682)), 473 ^ _116140 : [(474 ^ _116140) ^ [] : [root(_131684, _131682)], (476 ^ _116140) ^ [_131872] : [min_precedes(_131872, _131684, _131682)]], -(min_precedes(_131684, 477 ^ [_131682, _131684], _131682))], (483 ^ _116140) ^ [_132186, _132188, _132190] : [next_subocc(_132190, _132188, _132186), 486 ^ _116140 : [(487 ^ _116140) ^ [] : [-(min_precedes(_132190, _132188, _132186))], (489 ^ _116140) ^ [_132409] : [min_precedes(_132190, _132409, _132186), min_precedes(_132409, _132188, _132186)]]], (495 ^ _116140) ^ [_132599, _132601, _132603] : [-(next_subocc(_132603, _132601, _132599)), min_precedes(_132603, _132601, _132599), 501 ^ _116140 : [(502 ^ _116140) ^ [] : [-(min_precedes(_132603, 500 ^ [_132599, _132601, _132603], _132599))], (504 ^ _116140) ^ [] : [-(min_precedes(500 ^ [_132599, _132601, _132603], _132601, _132599))]]], (508 ^ _116140) ^ [_133107, _133109] : [atocc(_133109, _133107), 512 ^ _116140 : [(513 ^ _116140) ^ [] : [-(subactivity(_133107, 511 ^ [_133107, _133109]))], (515 ^ _116140) ^ [] : [-(atomic(511 ^ [_133107, _133109]))], (517 ^ _116140) ^ [] : [-(occurrence_of(_133109, 511 ^ [_133107, _133109]))]]], (519 ^ _116140) ^ [_133498, _133500] : [-(atocc(_133500, _133498)), 520 ^ _116140 : [(521 ^ _116140) ^ [_133595] : [subactivity(_133498, _133595), atomic(_133595), occurrence_of(_133500, _133595)]]], (533 ^ _116140) ^ [_133958, _133960] : [subactivity_occurrence(_133960, _133958), 536 ^ _116140 : [(537 ^ _116140) ^ [] : [-(activity_occurrence(_133960))], (539 ^ _116140) ^ [] : [-(activity_occurrence(_133958))]]], (541 ^ _116140) ^ [_134253, _134255, _134257] : [min_precedes(_134255, _134253, _134257), 545 ^ _116140 : [(546 ^ _116140) ^ [] : [-(occurrence_of(544 ^ [_134253, _134255, _134257], _134257))], (548 ^ _116140) ^ [] : [-(subactivity_occurrence(_134255, 544 ^ [_134253, _134255, _134257]))], (550 ^ _116140) ^ [] : [-(subactivity_occurrence(_134253, 544 ^ [_134253, _134255, _134257]))]]], (552 ^ _116140) ^ [_134717, _134719] : [560 ^ _116140 : [(561 ^ _116140) ^ [] : [-(occurrence_of(559 ^ [_134717, _134719], _134719))], (563 ^ _116140) ^ [] : [-(subactivity_occurrence(_134717, 559 ^ [_134717, _134719]))]], root(_134717, _134719), -(atomic(_134719))], (565 ^ _116140) ^ [_135162, _135164] : [573 ^ _116140 : [(574 ^ _116140) ^ [] : [-(root(572 ^ [_135162, _135164], _135164))], (576 ^ _116140) ^ [] : [-(subactivity_occurrence(572 ^ [_135162, _135164], _135162))]], occurrence_of(_135162, _135164), -(atomic(_135164))], (578 ^ _116140) ^ [_135635, _135637, _135639, _135641] : [-(min_precedes(_135637, _135635, _135641)), -(min_precedes(_135635, _135637, _135641)), -(_135637 = _135635), occurrence_of(_135639, _135641), arboreal(_135637), arboreal(_135635), subactivity_occurrence(_135637, _135639), subactivity_occurrence(_135635, _135639)], (608 ^ _116140) ^ [_136473, _136475, _136477, _136479] : [-(subactivity_occurrence(_136479, _136473)), min_precedes(_136479, _136477, _136475), occurrence_of(_136473, _136475), subactivity_occurrence(_136477, _136473)], (622 ^ _116140) ^ [_136919, _136921, _136923, _136925] : [-(subactivity(_136925, _136923)), occurrence_of(_136921, _136925), occurrence_of(_136919, _136923), -(atomic(_136925)), subactivity_occurrence(_136921, _136919)], (640 ^ _116140) ^ [_137447, _137449, _137451] : [-(subactivity_occurrence(_137451, _137447)), subactivity_occurrence(_137451, _137449), subactivity_occurrence(_137449, _137447)], (650 ^ _116140) ^ [_137784, _137786, _137788, _137790] : [666 ^ _116140 : [(667 ^ _116140) ^ [] : [-(subactivity_occurrence(665 ^ [_137784, _137786, _137788, _137790], _137784))], (669 ^ _116140) ^ [] : [subactivity_occurrence(665 ^ [_137784, _137786, _137788, _137790], _137786)]], occurrence_of(_137786, _137790), occurrence_of(_137784, _137788), subactivity(_137790, _137788), -(subactivity_occurrence(_137786, _137784))], (671 ^ _116140) ^ [_138497, _138499] : [root_occ(_138499, _138497), 675 ^ _116140 : [(676 ^ _116140) ^ [] : [-(occurrence_of(_138497, 674 ^ [_138497, _138499]))], (678 ^ _116140) ^ [] : [-(subactivity_occurrence(_138499, _138497))], (680 ^ _116140) ^ [] : [-(root(_138499, 674 ^ [_138497, _138499]))]]], (682 ^ _116140) ^ [_138884, _138886] : [-(root_occ(_138886, _138884)), 683 ^ _116140 : [(684 ^ _116140) ^ [_138982] : [occurrence_of(_138884, _138982), subactivity_occurrence(_138886, _138884), root(_138886, _138982)]]], (746 ^ _116140) ^ [] : [-(activity(tptp0))], (748 ^ _116140) ^ [] : [atomic(tptp0)], (750 ^ _116140) ^ [] : [-(atomic(tptp4))], (752 ^ _116140) ^ [] : [-(atomic(tptp1))], (754 ^ _116140) ^ [] : [-(atomic(tptp2))], (756 ^ _116140) ^ [] : [-(atomic(tptp3))], (758 ^ _116140) ^ [] : [tptp4 = tptp3], (760 ^ _116140) ^ [] : [tptp4 = tptp1], (762 ^ _116140) ^ [] : [tptp4 = tptp2], (764 ^ _116140) ^ [] : [tptp3 = tptp1], (766 ^ _116140) ^ [] : [tptp3 = tptp2], (768 ^ _116140) ^ [] : [tptp1 = tptp2], (721 ^ _116140) ^ [_140212] : [occurrence_of(_140212, tptp0), 727 ^ _116140 : [(728 ^ _116140) ^ [] : [-(occurrence_of(724 ^ [_140212], tptp3))], (730 ^ _116140) ^ [] : [-(root_occ(724 ^ [_140212], _140212))], (732 ^ _116140) ^ [] : [-(occurrence_of(725 ^ [_140212], tptp4))], (734 ^ _116140) ^ [] : [-(next_subocc(724 ^ [_140212], 725 ^ [_140212], tptp0))], (742 ^ _116140) ^ [] : [-(next_subocc(725 ^ [_140212], 726 ^ [_140212], tptp0))], (744 ^ _116140) ^ [] : [-(leaf_occ(726 ^ [_140212], _140212))], (736 ^ _116140) ^ [] : [-(occurrence_of(726 ^ [_140212], tptp1)), -(occurrence_of(726 ^ [_140212], tptp2))]]], (696 ^ _116140) ^ [_139376, _139378] : [leaf_occ(_139378, _139376), 700 ^ _116140 : [(701 ^ _116140) ^ [] : [-(occurrence_of(_139376, 699 ^ [_139376, _139378]))], (703 ^ _116140) ^ [] : [-(subactivity_occurrence(_139378, _139376))], (705 ^ _116140) ^ [] : [-(leaf(_139378, 699 ^ [_139376, _139378]))]]], (707 ^ _116140) ^ [_139763, _139765] : [-(leaf_occ(_139765, _139763)), 708 ^ _116140 : [(709 ^ _116140) ^ [_139861] : [occurrence_of(_139763, _139861), subactivity_occurrence(_139765, _139763), leaf(_139765, _139861)]]]], input).
% 7.85/8.60 ncf('1',plain,[leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 468 : min_precedes(726 ^ [769 ^ []], 477 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],start(457 ^ 0,bind([[_131271, _131273, _131611], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 477 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('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 ^ 1,bind([[_120465, _120467, _120469, _120471], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('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 ^ 2,bind([[_120465, _120467, _120469, _120471], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.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 ^ 3,bind([[_120465, _120467, _120469, _120471], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.1.1.1.1',plain,[-(leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 4,bind([[_139376, _139378], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.1.1.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 5,bind([[_140212], [769 ^ []]]))).
% 7.85/8.60 ncf('1.1.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 6)).
% 7.85/8.60 ncf('1.1.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 4,bind([[_116264], [726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.1.1.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(2 ^ 4,bind([[_116264], [699 ^ [769 ^ [], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('1.1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 3,bind([[_116264], [726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.1.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(2 ^ 3,bind([[_116264], [699 ^ [769 ^ [], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('1.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 2,bind([[_116264], [726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(2 ^ 2,bind([[_116264], [699 ^ [769 ^ [], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('1.2',plain,[-(min_precedes(726 ^ [769 ^ []], 477 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), -(leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), 474 : root(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(470 ^ 3,bind([[_131682, _131684], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.2.1',plain,[leaf(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), -(leaf(726 ^ [769 ^ []], tptp0)), 726 ^ [769 ^ []] = 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]] = tptp0],extension(134 ^ 4,bind([[_120465, _120467, _120469, _120471], [tptp0, 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.2.1.1',plain,[leaf(726 ^ [769 ^ []], tptp0), 468 : min_precedes(726 ^ [769 ^ []], 780 ^ [726 ^ [769 ^ []], 726 ^ [769 ^ []]], tptp0)],extension(457 ^ 5,bind([[_131271, _131273, _131611], [tptp0, 726 ^ [769 ^ []], 780 ^ [726 ^ [769 ^ []], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('1.2.1.1.1',plain,[-(min_precedes(726 ^ [769 ^ []], 780 ^ [726 ^ [769 ^ []], 726 ^ [769 ^ []]], tptp0)), leaf_occ(726 ^ [769 ^ []], 769 ^ []), 791 : -(min_precedes(726 ^ [769 ^ []], 787 ^ [726 ^ [769 ^ []], 726 ^ [769 ^ []]], tptp0))],extension(773 ^ 8,bind([[_142377, _142379], [726 ^ [769 ^ []], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.2.1.1.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 9,bind([[_140212], [769 ^ []]]))).
% 7.85/8.60 ncf('1.2.1.1.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 10)).
% 7.85/8.60 ncf('1.2.1.1.1.2',plain,[min_precedes(726 ^ [769 ^ []], 787 ^ [726 ^ [769 ^ []], 726 ^ [769 ^ []]], tptp0)],extension(468 ^ 11,bind([[_131611], [787 ^ [726 ^ [769 ^ []], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('1.2.1.2',plain,[-(726 ^ [769 ^ []] = 726 ^ [769 ^ []])],extension(2 ^ 5,bind([[_116264], [726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.2.1.3',plain,[-(699 ^ [769 ^ [], 726 ^ [769 ^ []]] = tptp0), occurrence_of(769 ^ [], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), occurrence_of(769 ^ [], tptp0)],extension(263 ^ 5,bind([[_124690, _124692, _124694], [tptp0, 699 ^ [769 ^ [], 726 ^ [769 ^ []]], 769 ^ []]]))).
% 7.85/8.60 ncf('1.2.1.3.1',plain,[-(occurrence_of(769 ^ [], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), leaf_occ(726 ^ [769 ^ []], 769 ^ [])],extension(696 ^ 6,bind([[_139376, _139378], [769 ^ [], 726 ^ [769 ^ []]]]))).
% 7.85/8.60 ncf('1.2.1.3.1.1',plain,[-(leaf_occ(726 ^ [769 ^ []], 769 ^ [])), occurrence_of(769 ^ [], tptp0)],extension(721 ^ 7,bind([[_140212], [769 ^ []]]))).
% 7.85/8.60 ncf('1.2.1.3.1.1.1',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 8)).
% 7.85/8.60 ncf('1.2.1.3.2',plain,[-(occurrence_of(769 ^ [], tptp0))],extension(771 ^ 6)).
% 7.85/8.60 ncf('1.2.2',plain,[-(root(726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])), -(min_precedes(464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]))],extension(461 ^ 6)).
% 7.85/8.60 ncf('1.2.2.1',plain,[min_precedes(464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 393 : -(min_precedes(389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]], 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]))],extension(386 ^ 7,bind([[_128765, _128767, _128769], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]]))).
% 7.85/8.60 ncf('1.2.2.1.1',plain,[min_precedes(389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]], 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]), 393 : -(min_precedes(389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]], 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]]))],extension(386 ^ 10,bind([[_128765, _128767, _128769], [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]]]))).
% 7.85/8.60 ncf('1.2.2.1.1.1',plain,[min_precedes(389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]], 726 ^ [769 ^ []], 699 ^ [769 ^ [], 726 ^ [769 ^ []]])],extension(476 ^ 13,bind([[_131872], [389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 389 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []], 464 ^ [699 ^ [769 ^ [], 726 ^ [769 ^ []]], 726 ^ [769 ^ []]]]]]]))).
% 7.85/8.60 %-----------------------------------------------------
% 7.85/8.60 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------