%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO009+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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 14.99s 14.81s
% Output : Proof 14.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PRO009+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n005.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:28:53 EDT 2023
% 0.12/0.33 % CPUTime :
% 14.99/14.81
% 14.99/14.81 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 14.99/14.81 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.99/14.81 %-----------------------------------------------------
% 14.99/14.81 ncf(matrix, plain, [(996 ^ _162905) ^ [] : [-(occurrence_of(994 ^ [], tptp0))], (998 ^ _162905) ^ [_196306, _196308] : [occurrence_of(_196308, tptp3), root_occ(_196308, 994 ^ []), 1007 ^ _162905 : [(1008 ^ _162905) ^ [] : [occurrence_of(_196306, tptp2)], (1010 ^ _162905) ^ [] : [occurrence_of(_196306, tptp1)]], min_precedes(_196308, _196306, tptp0), leaf_occ(_196306, 994 ^ [])], (2 ^ _162905) ^ [_163029] : [-(_163029 = _163029)], (4 ^ _162905) ^ [_163136, _163138] : [_163138 = _163136, -(_163136 = _163138)], (10 ^ _162905) ^ [_163340, _163342, _163344] : [-(_163344 = _163340), _163344 = _163342, _163342 = _163340], (20 ^ _162905) ^ [_163681, _163683, _163685, _163687] : [-(earlier(_163685, _163681)), earlier(_163687, _163683), _163687 = _163685, _163683 = _163681], (34 ^ _162905) ^ [_164097, _164099] : [-(legal(_164097)), _164099 = _164097, legal(_164099)], (44 ^ _162905) ^ [_164420, _164422, _164424, _164426] : [-(precedes(_164424, _164420)), precedes(_164426, _164422), _164426 = _164424, _164422 = _164420], (58 ^ _162905) ^ [_164864, _164866, _164868, _164870] : [-(atocc(_164868, _164864)), atocc(_164870, _164866), _164870 = _164868, _164866 = _164864], (72 ^ _162905) ^ [_165280, _165282] : [-(activity_occurrence(_165280)), _165282 = _165280, activity_occurrence(_165282)], (82 ^ _162905) ^ [_165603, _165605, _165607, _165609] : [-(subactivity(_165607, _165603)), subactivity(_165609, _165605), _165609 = _165607, _165605 = _165603], (96 ^ _162905) ^ [_166047, _166049, _166051, _166053] : [-(root(_166051, _166047)), root(_166053, _166049), _166053 = _166051, _166049 = _166047], (110 ^ _162905) ^ [_166491, _166493, _166495, _166497] : [-(leaf(_166495, _166491)), leaf(_166497, _166493), _166497 = _166495, _166493 = _166491], (124 ^ _162905) ^ [_166907, _166909] : [-(arboreal(_166907)), _166909 = _166907, arboreal(_166909)], (134 ^ _162905) ^ [_167230, _167232, _167234, _167236] : [-(subactivity_occurrence(_167234, _167230)), subactivity_occurrence(_167236, _167232), _167236 = _167234, _167232 = _167230], (148 ^ _162905) ^ [_167702, _167704, _167706, _167708, _167710, _167712] : [-(next_subocc(_167710, _167706, _167702)), next_subocc(_167712, _167708, _167704), _167712 = _167710, _167708 = _167706, _167704 = _167702], (166 ^ _162905) ^ [_168255, _168257] : [-(activity(_168255)), _168257 = _168255, activity(_168257)], (176 ^ _162905) ^ [_168550, _168552] : [-(atomic(_168550)), _168552 = _168550, atomic(_168552)], (186 ^ _162905) ^ [_168873, _168875, _168877, _168879] : [-(root_occ(_168877, _168873)), root_occ(_168879, _168875), _168879 = _168877, _168875 = _168873], (200 ^ _162905) ^ [_169317, _169319, _169321, _169323] : [-(occurrence_of(_169321, _169317)), occurrence_of(_169323, _169319), _169323 = _169321, _169319 = _169317], (232 ^ _162905) ^ [_170350, _170352, _170354, _170356] : [-(leaf_occ(_170354, _170350)), leaf_occ(_170356, _170352), _170356 = _170354, _170352 = _170350], (214 ^ _162905) ^ [_169789, _169791, _169793, _169795, _169797, _169799] : [-(min_precedes(_169797, _169793, _169789)), min_precedes(_169799, _169795, _169791), _169799 = _169797, _169795 = _169793, _169791 = _169789], (246 ^ _162905) ^ [_170840, _170842] : [occurrence_of(_170840, _170842), 249 ^ _162905 : [(250 ^ _162905) ^ [] : [-(activity(_170842))], (252 ^ _162905) ^ [] : [-(activity_occurrence(_170840))]]], (254 ^ _162905) ^ [_171107] : [activity_occurrence(_171107), 258 ^ _162905 : [(259 ^ _162905) ^ [] : [-(activity(257 ^ [_171107]))], (261 ^ _162905) ^ [] : [-(occurrence_of(_171107, 257 ^ [_171107]))]]], (263 ^ _162905) ^ [_171455, _171457, _171459] : [-(_171457 = _171455), occurrence_of(_171459, _171457), occurrence_of(_171459, _171455)], (273 ^ _162905) ^ [_171750] : [activity(_171750), -(subactivity(_171750, _171750))], (279 ^ _162905) ^ [_171952, _171954] : [earlier(_171954, _171952), earlier(_171952, _171954)], (285 ^ _162905) ^ [_172177, _172179, _172181] : [-(earlier(_172181, _172177)), earlier(_172181, _172179), earlier(_172179, _172177)], (295 ^ _162905) ^ [_172500, _172502, _172504] : [earlier(_172504, _172502), earlier(_172500, _172502), -(earlier(_172500, _172504)), -(earlier(_172504, _172500)), -(_172504 = _172500)], (313 ^ _162905) ^ [_172999, _173001] : [occurrence_of(_173001, _172999), 316 ^ _162905 : [(317 ^ _162905) ^ [] : [arboreal(_173001), -(atomic(_172999))], (323 ^ _162905) ^ [] : [atomic(_172999), -(arboreal(_173001))]]], (329 ^ _162905) ^ [_173439] : [legal(_173439), -(arboreal(_173439))], (335 ^ _162905) ^ [_173639, _173641] : [-(legal(_173639)), legal(_173641), earlier(_173639, _173641)], (345 ^ _162905) ^ [_173963, _173965] : [precedes(_173965, _173963), 348 ^ _162905 : [(349 ^ _162905) ^ [] : [-(earlier(_173965, _173963))], (351 ^ _162905) ^ [] : [-(legal(_173963))]]], (353 ^ _162905) ^ [_174198, _174200] : [-(precedes(_174200, _174198)), earlier(_174200, _174198), legal(_174198)], (363 ^ _162905) ^ [_174511, _174513, _174515] : [min_precedes(_174513, _174511, _174515), 368 ^ _162905 : [(369 ^ _162905) ^ [] : [-(subactivity(366 ^ [_174511, _174513, _174515], _174515))], (371 ^ _162905) ^ [] : [-(subactivity(367 ^ [_174511, _174513, _174515], _174515))], (373 ^ _162905) ^ [] : [-(atocc(_174513, 366 ^ [_174511, _174513, _174515]))], (375 ^ _162905) ^ [] : [-(atocc(_174511, 367 ^ [_174511, _174513, _174515]))]]], (377 ^ _162905) ^ [_175161, _175163] : [root(_175161, _175163), 381 ^ _162905 : [(382 ^ _162905) ^ [] : [-(subactivity(380 ^ [_175161, _175163], _175163))], (384 ^ _162905) ^ [] : [-(atocc(_175161, 380 ^ [_175161, _175163]))]]], (386 ^ _162905) ^ [_175530, _175532, _175534] : [min_precedes(_175534, _175532, _175530), 390 ^ _162905 : [(391 ^ _162905) ^ [] : [-(root(389 ^ [_175530, _175532, _175534], _175530))], (393 ^ _162905) ^ [] : [-(min_precedes(389 ^ [_175530, _175532, _175534], _175532, _175530))]]], (395 ^ _162905) ^ [_175920, _175922, _175924] : [min_precedes(_175924, _175922, _175920), root(_175922, _175920)], (401 ^ _162905) ^ [_176153, _176155, _176157] : [min_precedes(_176157, _176155, _176153), -(precedes(_176157, _176155))], (407 ^ _162905) ^ [_176371, _176373] : [root(_176373, _176371), -(legal(_176373))], (413 ^ _162905) ^ [_176579, _176581] : [-(root(_176581, _176579)), atocc(_176581, _176579), legal(_176581)], (423 ^ _162905) ^ [_176904, _176906, _176908, _176910] : [-(min_precedes(_176908, _176906, _176904)), min_precedes(_176910, _176908, _176904), min_precedes(_176910, _176906, _176904), precedes(_176908, _176906)], (437 ^ _162905) ^ [_177340, _177342, _177344] : [min_precedes(_177344, _177342, _177340), atomic(_177340)], (443 ^ _162905) ^ [_177585, _177587, _177589, _177591] : [-(min_precedes(_177589, _177587, _177585)), min_precedes(_177589, _177591, _177585), min_precedes(_177587, _177591, _177585), precedes(_177589, _177587)], (457 ^ _162905) ^ [_178036, _178038] : [leaf(_178038, _178036), 460 ^ _162905 : [(468 ^ _162905) ^ [_178376] : [min_precedes(_178038, _178376, _178036)], (461 ^ _162905) ^ [] : [-(root(_178038, _178036)), -(min_precedes(464 ^ [_178036, _178038], _178038, _178036))]]], (470 ^ _162905) ^ [_178447, _178449] : [-(leaf(_178449, _178447)), 473 ^ _162905 : [(474 ^ _162905) ^ [] : [root(_178449, _178447)], (476 ^ _162905) ^ [_178637] : [min_precedes(_178637, _178449, _178447)]], -(min_precedes(_178449, 477 ^ [_178447, _178449], _178447))], (483 ^ _162905) ^ [_178951, _178953, _178955] : [next_subocc(_178955, _178953, _178951), 486 ^ _162905 : [(487 ^ _162905) ^ [] : [-(min_precedes(_178955, _178953, _178951))], (489 ^ _162905) ^ [_179174] : [min_precedes(_178955, _179174, _178951), min_precedes(_179174, _178953, _178951)]]], (495 ^ _162905) ^ [_179364, _179366, _179368] : [-(next_subocc(_179368, _179366, _179364)), min_precedes(_179368, _179366, _179364), 501 ^ _162905 : [(502 ^ _162905) ^ [] : [-(min_precedes(_179368, 500 ^ [_179364, _179366, _179368], _179364))], (504 ^ _162905) ^ [] : [-(min_precedes(500 ^ [_179364, _179366, _179368], _179366, _179364))]]], (508 ^ _162905) ^ [_179872, _179874] : [atocc(_179874, _179872), 512 ^ _162905 : [(513 ^ _162905) ^ [] : [-(subactivity(_179872, 511 ^ [_179872, _179874]))], (515 ^ _162905) ^ [] : [-(atomic(511 ^ [_179872, _179874]))], (517 ^ _162905) ^ [] : [-(occurrence_of(_179874, 511 ^ [_179872, _179874]))]]], (519 ^ _162905) ^ [_180263, _180265] : [-(atocc(_180265, _180263)), 520 ^ _162905 : [(521 ^ _162905) ^ [_180360] : [subactivity(_180263, _180360), atomic(_180360), occurrence_of(_180265, _180360)]]], (533 ^ _162905) ^ [_180723, _180725] : [subactivity_occurrence(_180725, _180723), 536 ^ _162905 : [(537 ^ _162905) ^ [] : [-(activity_occurrence(_180725))], (539 ^ _162905) ^ [] : [-(activity_occurrence(_180723))]]], (541 ^ _162905) ^ [_181018, _181020, _181022] : [min_precedes(_181020, _181018, _181022), 545 ^ _162905 : [(546 ^ _162905) ^ [] : [-(occurrence_of(544 ^ [_181018, _181020, _181022], _181022))], (548 ^ _162905) ^ [] : [-(subactivity_occurrence(_181020, 544 ^ [_181018, _181020, _181022]))], (550 ^ _162905) ^ [] : [-(subactivity_occurrence(_181018, 544 ^ [_181018, _181020, _181022]))]]], (552 ^ _162905) ^ [_181482, _181484] : [560 ^ _162905 : [(561 ^ _162905) ^ [] : [-(occurrence_of(559 ^ [_181482, _181484], _181484))], (563 ^ _162905) ^ [] : [-(subactivity_occurrence(_181482, 559 ^ [_181482, _181484]))]], root(_181482, _181484), -(atomic(_181484))], (565 ^ _162905) ^ [_181927, _181929] : [573 ^ _162905 : [(574 ^ _162905) ^ [] : [-(root(572 ^ [_181927, _181929], _181929))], (576 ^ _162905) ^ [] : [-(subactivity_occurrence(572 ^ [_181927, _181929], _181927))]], occurrence_of(_181927, _181929), -(atomic(_181929))], (578 ^ _162905) ^ [_182400, _182402, _182404, _182406] : [-(min_precedes(_182402, _182400, _182406)), -(min_precedes(_182400, _182402, _182406)), -(_182402 = _182400), occurrence_of(_182404, _182406), arboreal(_182402), arboreal(_182400), subactivity_occurrence(_182402, _182404), subactivity_occurrence(_182400, _182404)], (608 ^ _162905) ^ [_183238, _183240, _183242, _183244] : [-(subactivity_occurrence(_183244, _183238)), min_precedes(_183244, _183242, _183240), occurrence_of(_183238, _183240), subactivity_occurrence(_183242, _183238)], (622 ^ _162905) ^ [_183684, _183686, _183688, _183690] : [-(subactivity(_183690, _183688)), occurrence_of(_183686, _183690), occurrence_of(_183684, _183688), -(atomic(_183690)), subactivity_occurrence(_183686, _183684)], (640 ^ _162905) ^ [_184212, _184214, _184216] : [-(subactivity_occurrence(_184216, _184212)), subactivity_occurrence(_184216, _184214), subactivity_occurrence(_184214, _184212)], (650 ^ _162905) ^ [_184549, _184551, _184553, _184555] : [666 ^ _162905 : [(667 ^ _162905) ^ [] : [-(subactivity_occurrence(665 ^ [_184549, _184551, _184553, _184555], _184549))], (669 ^ _162905) ^ [] : [subactivity_occurrence(665 ^ [_184549, _184551, _184553, _184555], _184551)]], occurrence_of(_184551, _184555), occurrence_of(_184549, _184553), subactivity(_184555, _184553), -(subactivity_occurrence(_184551, _184549))], (671 ^ _162905) ^ [_185262, _185264] : [root_occ(_185264, _185262), 675 ^ _162905 : [(676 ^ _162905) ^ [] : [-(occurrence_of(_185262, 674 ^ [_185262, _185264]))], (678 ^ _162905) ^ [] : [-(subactivity_occurrence(_185264, _185262))], (680 ^ _162905) ^ [] : [-(root(_185264, 674 ^ [_185262, _185264]))]]], (682 ^ _162905) ^ [_185649, _185651] : [-(root_occ(_185651, _185649)), 683 ^ _162905 : [(684 ^ _162905) ^ [_185747] : [occurrence_of(_185649, _185747), subactivity_occurrence(_185651, _185649), root(_185651, _185747)]]], (696 ^ _162905) ^ [_186141, _186143] : [leaf_occ(_186143, _186141), 700 ^ _162905 : [(701 ^ _162905) ^ [] : [-(occurrence_of(_186141, 699 ^ [_186141, _186143]))], (703 ^ _162905) ^ [] : [-(subactivity_occurrence(_186143, _186141))], (705 ^ _162905) ^ [] : [-(leaf(_186143, 699 ^ [_186141, _186143]))]]], (707 ^ _162905) ^ [_186528, _186530] : [-(leaf_occ(_186530, _186528)), 708 ^ _162905 : [(709 ^ _162905) ^ [_186626] : [occurrence_of(_186528, _186626), subactivity_occurrence(_186530, _186528), leaf(_186530, _186626)]]], (721 ^ _162905) ^ [_187019, _187021, _187023, _187025] : [-(_187025 = _187023), occurrence_of(_187021, _187019), root_occ(_187025, _187021), root_occ(_187023, _187021)], (735 ^ _162905) ^ [_187463, _187465, _187467, _187469] : [-(_187469 = _187467), occurrence_of(_187465, _187463), -(atomic(_187463)), leaf_occ(_187469, _187465), leaf_occ(_187467, _187465)], (753 ^ _162905) ^ [_187991, _187993, _187995] : [760 ^ _162905 : [(761 ^ _162905) ^ [_188206] : [min_precedes(_187993, _188206, _187991)]], occurrence_of(_187995, _187991), leaf_occ(_187993, _187995)], (763 ^ _162905) ^ [_188339, _188341, _188343] : [770 ^ _162905 : [(771 ^ _162905) ^ [_188554] : [min_precedes(_188554, _188341, _188339)]], occurrence_of(_188343, _188339), root_occ(_188341, _188343)], (773 ^ _162905) ^ [_188715, _188717, _188719, _188721, _188723] : [-(_188721 = _188719), next_subocc(_188723, _188721, _188717), next_subocc(_188723, _188719, _188717), occurrence_of(_188715, _188717), subactivity_occurrence(_188719, _188715), subactivity_occurrence(_188721, _188715)], (795 ^ _162905) ^ [_189379, _189381, _189383, _189385] : [-(_189383 = _189381), next_subocc(_189383, _189385, _189379), next_subocc(_189381, _189385, _189379)], (805 ^ _162905) ^ [_189730, _189732, _189734, _189736] : [-(min_precedes(_189732, _189734, _189730)), occurrence_of(_189736, _189730), leaf_occ(_189734, _189736), root_occ(_189732, _189736), -(_189734 = _189732)], (823 ^ _162905) ^ [_190276, _190278, _190280, _190282] : [-(_190276 = _190278), occurrence_of(_190280, _190282), subactivity_occurrence(_190278, _190280), root_occ(_190276, _190280), arboreal(_190278), -(min_precedes(_190276, _190278, _190282))], (845 ^ _162905) ^ [_190917, _190919, _190921, _190923] : [-(_190917 = _190919), occurrence_of(_190921, _190923), subactivity_occurrence(_190919, _190921), leaf_occ(_190917, _190921), arboreal(_190919), -(min_precedes(_190919, _190917, _190923))], (867 ^ _162905) ^ [_191544, _191546, _191548] : [next_subocc(_191548, _191546, _191544), 870 ^ _162905 : [(871 ^ _162905) ^ [] : [-(arboreal(_191548))], (873 ^ _162905) ^ [] : [-(arboreal(_191546))]]], (875 ^ _162905) ^ [_191835, _191837] : [883 ^ _162905 : [(884 ^ _162905) ^ [] : [-(occurrence_of(882 ^ [_191835, _191837], _191835))], (886 ^ _162905) ^ [] : [-(leaf_occ(_191837, 882 ^ [_191835, _191837]))]], leaf(_191837, _191835), -(atomic(_191835))], (888 ^ _162905) ^ [_192294, _192296, _192298] : [min_precedes(_192298, _192296, _192294), -(arboreal(_192298))], (894 ^ _162905) ^ [_192552, _192554, _192556, _192558, _192560] : [-(min_precedes(_192554, _192556, _192560)), occurrence_of(_192558, _192560), root_occ(_192554, _192558), leaf_occ(_192552, _192558), subactivity_occurrence(_192556, _192558), min_precedes(_192556, _192552, _192560), -(_192556 = _192554)], (971 ^ _162905) ^ [] : [-(activity(tptp0))], (973 ^ _162905) ^ [] : [atomic(tptp0)], (975 ^ _162905) ^ [] : [-(atomic(tptp4))], (977 ^ _162905) ^ [] : [-(atomic(tptp2))], (979 ^ _162905) ^ [] : [-(atomic(tptp1))], (981 ^ _162905) ^ [] : [-(atomic(tptp3))], (983 ^ _162905) ^ [] : [tptp4 = tptp3], (985 ^ _162905) ^ [] : [tptp4 = tptp2], (987 ^ _162905) ^ [] : [tptp4 = tptp1], (989 ^ _162905) ^ [] : [tptp3 = tptp2], (991 ^ _162905) ^ [] : [tptp3 = tptp1], (993 ^ _162905) ^ [] : [tptp2 = tptp1], (946 ^ _162905) ^ [_194060] : [occurrence_of(_194060, tptp0), 952 ^ _162905 : [(953 ^ _162905) ^ [] : [-(occurrence_of(949 ^ [_194060], tptp3))], (955 ^ _162905) ^ [] : [-(root_occ(949 ^ [_194060], _194060))], (957 ^ _162905) ^ [] : [-(occurrence_of(950 ^ [_194060], tptp4))], (959 ^ _162905) ^ [] : [-(next_subocc(949 ^ [_194060], 950 ^ [_194060], tptp0))], (967 ^ _162905) ^ [] : [-(next_subocc(950 ^ [_194060], 951 ^ [_194060], tptp0))], (969 ^ _162905) ^ [] : [-(leaf_occ(951 ^ [_194060], _194060))], (961 ^ _162905) ^ [] : [-(occurrence_of(951 ^ [_194060], tptp2)), -(occurrence_of(951 ^ [_194060], tptp1))]]], (920 ^ _162905) ^ [_193334, _193336, _193338, _193340, _193342] : [-(min_precedes(_193338, _193334, _193342)), occurrence_of(_193340, _193342), root_occ(_193336, _193340), leaf_occ(_193334, _193340), subactivity_occurrence(_193338, _193340), min_precedes(_193336, _193338, _193342), -(_193338 = _193334)]], input).
% 14.99/14.81 ncf('1',plain,[occurrence_of(949 ^ [994 ^ []], tptp3), root_occ(949 ^ [994 ^ []], 994 ^ []), 1008 : occurrence_of(951 ^ [994 ^ []], tptp2), 1008 : min_precedes(949 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0), 1008 : leaf_occ(951 ^ [994 ^ []], 994 ^ [])],start(998 ^ 0,bind([[_196306, _196308], [951 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.1',plain,[-(occurrence_of(949 ^ [994 ^ []], tptp3)), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 1,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 2)).
% 14.99/14.81 ncf('1.2',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), root_occ(949 ^ [994 ^ []], 994 ^ []), 949 ^ [994 ^ []] = 949 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(186 ^ 1,bind([[_168873, _168875, _168877, _168879], [994 ^ [], 994 ^ [], 949 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), root_occ(949 ^ [994 ^ []], 994 ^ []), 949 ^ [994 ^ []] = 949 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(186 ^ 2,bind([[_168873, _168875, _168877, _168879], [994 ^ [], 994 ^ [], 949 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), root_occ(949 ^ [994 ^ []], 994 ^ []), 949 ^ [994 ^ []] = 949 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(186 ^ 3,bind([[_168873, _168875, _168877, _168879], [994 ^ [], 994 ^ [], 949 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1.1.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), root_occ(949 ^ [994 ^ []], 994 ^ []), 949 ^ [994 ^ []] = 949 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(186 ^ 4,bind([[_168873, _168875, _168877, _168879], [994 ^ [], 994 ^ [], 949 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1.1.1.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.2.1.1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.2.1.1.1.2',plain,[-(949 ^ [994 ^ []] = 949 ^ [994 ^ []])],extension(2 ^ 5,bind([[_163029], [949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1.1.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 5,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.2.1.1.2',plain,[-(949 ^ [994 ^ []] = 949 ^ [994 ^ []])],extension(2 ^ 4,bind([[_163029], [949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 4,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.2.1.2',plain,[-(949 ^ [994 ^ []] = 949 ^ [994 ^ []])],extension(2 ^ 3,bind([[_163029], [949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 3,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.2.2',plain,[-(949 ^ [994 ^ []] = 949 ^ [994 ^ []])],extension(2 ^ 2,bind([[_163029], [949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.2.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 2,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.3',plain,[-(occurrence_of(951 ^ [994 ^ []], tptp2)), 961 : -(occurrence_of(951 ^ [994 ^ []], tptp1)), 961 : occurrence_of(994 ^ [], tptp0)],extension(946 ^ 3,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.3.1',plain,[occurrence_of(951 ^ [994 ^ []], tptp1)],extension(1010 ^ 6)).
% 14.99/14.81 ncf('1.3.2',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 4)).
% 14.99/14.81 ncf('1.4',plain,[-(min_precedes(949 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)), -(min_precedes(951 ^ [994 ^ []], 949 ^ [994 ^ []], tptp0)), -(949 ^ [994 ^ []] = 951 ^ [994 ^ []]), occurrence_of(994 ^ [], tptp0), arboreal(949 ^ [994 ^ []]), arboreal(951 ^ [994 ^ []]), subactivity_occurrence(949 ^ [994 ^ []], 994 ^ []), subactivity_occurrence(951 ^ [994 ^ []], 994 ^ [])],extension(578 ^ 1,bind([[_182400, _182402, _182404, _182406], [951 ^ [994 ^ []], 949 ^ [994 ^ []], 994 ^ [], tptp0]]))).
% 14.99/14.81 ncf('1.4.1',plain,[min_precedes(951 ^ [994 ^ []], 949 ^ [994 ^ []], tptp0), -(min_precedes(949 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)), 951 ^ [994 ^ []] = 949 ^ [994 ^ []], 949 ^ [994 ^ []] = 951 ^ [994 ^ []], tptp0 = tptp0],extension(214 ^ 2,bind([[_169789, _169791, _169793, _169795, _169797, _169799], [tptp0, tptp0, 951 ^ [994 ^ []], 949 ^ [994 ^ []], 949 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.1.1',plain,[min_precedes(949 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)],reduction('1')).
% 14.99/14.81 ncf('1.4.1.2',plain,[-(951 ^ [994 ^ []] = 949 ^ [994 ^ []]), -(min_precedes(949 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)), occurrence_of(994 ^ [], tptp0), leaf_occ(951 ^ [994 ^ []], 994 ^ []), root_occ(949 ^ [994 ^ []], 994 ^ [])],extension(805 ^ 3,bind([[_189730, _189732, _189734, _189736], [tptp0, 949 ^ [994 ^ []], 951 ^ [994 ^ []], 994 ^ []]]))).
% 14.99/14.81 ncf('1.4.1.2.1',plain,[min_precedes(949 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)],reduction('1')).
% 14.99/14.81 ncf('1.4.1.2.2',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 4)).
% 14.99/14.81 ncf('1.4.1.2.3',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 4,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.1.2.3.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.1.2.3.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.4.1.2.3.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 5,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.1.2.3.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 5,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.1.2.4',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ []))],lemmata('x')).
% 14.99/14.81 ncf('1.4.1.3',plain,[-(949 ^ [994 ^ []] = 951 ^ [994 ^ []]), 951 ^ [994 ^ []] = 949 ^ [994 ^ []]],extension(4 ^ 3,bind([[_163136, _163138], [949 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.1.3.1',plain,[-(951 ^ [994 ^ []] = 949 ^ [994 ^ []])],lemmata('[4, 1].x')).
% 14.99/14.81 ncf('1.4.1.4',plain,[-(tptp0 = tptp0)],extension(2 ^ 3,bind([[_163029], [tptp0]]))).
% 14.99/14.81 ncf('1.4.2',plain,[949 ^ [994 ^ []] = 951 ^ [994 ^ []], -(root(951 ^ [994 ^ []], tptp0)), root(949 ^ [994 ^ []], 674 ^ [994 ^ [], 949 ^ [994 ^ []]]), 674 ^ [994 ^ [], 949 ^ [994 ^ []]] = tptp0],extension(96 ^ 2,bind([[_166047, _166049, _166051, _166053], [tptp0, 674 ^ [994 ^ [], 949 ^ [994 ^ []]], 951 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.1',plain,[root(951 ^ [994 ^ []], tptp0), min_precedes(950 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)],extension(395 ^ 3,bind([[_175920, _175922, _175924], [tptp0, 951 ^ [994 ^ []], 950 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.1.1',plain,[-(min_precedes(950 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)), next_subocc(950 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)],extension(483 ^ 4,bind([[_178951, _178953, _178955], [tptp0, 951 ^ [994 ^ []], 950 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.1.1.1',plain,[-(next_subocc(950 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.2.1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.4.2.2',plain,[-(root(949 ^ [994 ^ []], 674 ^ [994 ^ [], 949 ^ [994 ^ []]])), root_occ(949 ^ [994 ^ []], 994 ^ [])],extension(671 ^ 3,bind([[_185262, _185264], [994 ^ [], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.2.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), root_occ(949 ^ [994 ^ []], 994 ^ []), 949 ^ [994 ^ []] = 949 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(186 ^ 4,bind([[_168873, _168875, _168877, _168879], [994 ^ [], 994 ^ [], 949 ^ [994 ^ []], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.2.1.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.2.2.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.4.2.2.1.2',plain,[-(949 ^ [994 ^ []] = 949 ^ [994 ^ []])],extension(2 ^ 5,bind([[_163029], [949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.2.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 5,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.2.3',plain,[-(674 ^ [994 ^ [], 949 ^ [994 ^ []]] = tptp0), tptp0 = 674 ^ [994 ^ [], 949 ^ [994 ^ []]]],extension(4 ^ 3,bind([[_163136, _163138], [674 ^ [994 ^ [], 949 ^ [994 ^ []]], tptp0]]))).
% 14.99/14.81 ncf('1.4.2.3.1',plain,[-(tptp0 = 674 ^ [994 ^ [], 949 ^ [994 ^ []]]), occurrence_of(994 ^ [], tptp0), occurrence_of(994 ^ [], 674 ^ [994 ^ [], 949 ^ [994 ^ []]])],extension(263 ^ 4,bind([[_171455, _171457, _171459], [674 ^ [994 ^ [], 949 ^ [994 ^ []]], tptp0, 994 ^ []]]))).
% 14.99/14.81 ncf('1.4.2.3.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 5)).
% 14.99/14.81 ncf('1.4.2.3.1.2',plain,[-(occurrence_of(994 ^ [], 674 ^ [994 ^ [], 949 ^ [994 ^ []]])), root_occ(949 ^ [994 ^ []], 994 ^ [])],extension(671 ^ 5,bind([[_185262, _185264], [994 ^ [], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.2.3.1.2.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ []))],lemmata('x')).
% 14.99/14.81 ncf('1.4.3',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 2)).
% 14.99/14.81 ncf('1.4.4',plain,[-(arboreal(949 ^ [994 ^ []])), legal(949 ^ [994 ^ []])],extension(329 ^ 2,bind([[_173439], [949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.4.1',plain,[-(legal(949 ^ [994 ^ []])), root(949 ^ [994 ^ []], 674 ^ [994 ^ [], 949 ^ [994 ^ []]])],extension(407 ^ 3,bind([[_176371, _176373], [674 ^ [994 ^ [], 949 ^ [994 ^ []]], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.4.1.1',plain,[-(root(949 ^ [994 ^ []], 674 ^ [994 ^ [], 949 ^ [994 ^ []]])), root_occ(949 ^ [994 ^ []], 994 ^ [])],extension(671 ^ 4,bind([[_185262, _185264], [994 ^ [], 949 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.4.1.1.1',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.4.1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],lemmata('[1].x')).
% 14.99/14.81 ncf('1.4.5',plain,[-(arboreal(951 ^ [994 ^ []])), next_subocc(950 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)],extension(867 ^ 2,bind([[_191544, _191546, _191548], [tptp0, 951 ^ [994 ^ []], 950 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.5.1',plain,[-(next_subocc(950 ^ [994 ^ []], 951 ^ [994 ^ []], tptp0)), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 3,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.5.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],lemmata('[1].x')).
% 14.99/14.81 ncf('1.4.6',plain,[-(subactivity_occurrence(949 ^ [994 ^ []], 994 ^ [])), subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ []), 572 ^ [994 ^ [], tptp0] = 949 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(134 ^ 2,bind([[_167230, _167232, _167234, _167236], [994 ^ [], 994 ^ [], 949 ^ [994 ^ []], 572 ^ [994 ^ [], tptp0]]]))).
% 14.99/14.81 ncf('1.4.6.1',plain,[-(subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ [])), subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ []), 572 ^ [994 ^ [], tptp0] = 572 ^ [994 ^ [], tptp0], 994 ^ [] = 994 ^ []],extension(134 ^ 3,bind([[_167230, _167232, _167234, _167236], [994 ^ [], 994 ^ [], 572 ^ [994 ^ [], tptp0], 572 ^ [994 ^ [], tptp0]]]))).
% 14.99/14.81 ncf('1.4.6.1.1',plain,[-(subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ [])), subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ []), 572 ^ [994 ^ [], tptp0] = 572 ^ [994 ^ [], tptp0], 994 ^ [] = 994 ^ []],extension(134 ^ 4,bind([[_167230, _167232, _167234, _167236], [994 ^ [], 994 ^ [], 572 ^ [994 ^ [], tptp0], 572 ^ [994 ^ [], tptp0]]]))).
% 14.99/14.81 ncf('1.4.6.1.1.1',plain,[-(subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ [])), occurrence_of(994 ^ [], tptp0), -(atomic(tptp0))],extension(565 ^ 5,bind([[_181927, _181929], [994 ^ [], tptp0]]))).
% 14.99/14.81 ncf('1.4.6.1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.4.6.1.1.1.2',plain,[atomic(tptp0)],extension(973 ^ 6)).
% 14.99/14.81 ncf('1.4.6.1.1.2',plain,[-(572 ^ [994 ^ [], tptp0] = 572 ^ [994 ^ [], tptp0])],extension(2 ^ 5,bind([[_163029], [572 ^ [994 ^ [], tptp0]]]))).
% 14.99/14.81 ncf('1.4.6.1.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 5,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.6.1.2',plain,[-(572 ^ [994 ^ [], tptp0] = 572 ^ [994 ^ [], tptp0])],extension(2 ^ 4,bind([[_163029], [572 ^ [994 ^ [], tptp0]]]))).
% 14.99/14.81 ncf('1.4.6.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 4,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.6.2',plain,[-(572 ^ [994 ^ [], tptp0] = 949 ^ [994 ^ []]), occurrence_of(994 ^ [], tptp0), root_occ(572 ^ [994 ^ [], tptp0], 994 ^ []), root_occ(949 ^ [994 ^ []], 994 ^ [])],extension(721 ^ 3,bind([[_187019, _187021, _187023, _187025], [tptp0, 994 ^ [], 949 ^ [994 ^ []], 572 ^ [994 ^ [], tptp0]]]))).
% 14.99/14.81 ncf('1.4.6.2.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 4)).
% 14.99/14.81 ncf('1.4.6.2.2',plain,[-(root_occ(572 ^ [994 ^ [], tptp0], 994 ^ [])), 684 : occurrence_of(994 ^ [], tptp0), 684 : subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ []), 684 : root(572 ^ [994 ^ [], tptp0], tptp0)],extension(682 ^ 4,bind([[_185649, _185651, _185747], [994 ^ [], 572 ^ [994 ^ [], tptp0], tptp0]]))).
% 14.99/14.81 ncf('1.4.6.2.2.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 7)).
% 14.99/14.81 ncf('1.4.6.2.2.2',plain,[-(subactivity_occurrence(572 ^ [994 ^ [], tptp0], 994 ^ []))],lemmata('[4, 1].x')).
% 14.99/14.81 ncf('1.4.6.2.2.3',plain,[-(root(572 ^ [994 ^ [], tptp0], tptp0)), occurrence_of(994 ^ [], tptp0), -(atomic(tptp0))],extension(565 ^ 7,bind([[_181927, _181929], [994 ^ [], tptp0]]))).
% 14.99/14.81 ncf('1.4.6.2.2.3.1',plain,[-(occurrence_of(994 ^ [], tptp0))],lemmata('[2, 6, 4, 1].x')).
% 14.99/14.81 ncf('1.4.6.2.2.3.2',plain,[atomic(tptp0)],extension(973 ^ 8)).
% 14.99/14.81 ncf('1.4.6.2.3',plain,[-(root_occ(949 ^ [994 ^ []], 994 ^ []))],lemmata('x')).
% 14.99/14.81 ncf('1.4.6.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 3,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.7',plain,[-(subactivity_occurrence(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ [])],extension(696 ^ 2,bind([[_186141, _186143], [994 ^ [], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.7.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 3,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.7.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 4,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.7.1.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.7.1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.4.7.1.1.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 5,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.7.1.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 5,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.4.7.1.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 4,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.4.7.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 4,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.5',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 1,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 2,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 3,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(232 ^ 4,bind([[_170350, _170352, _170354, _170356], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1.1.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 5,bind([[_194060], [994 ^ []]]))).
% 14.99/14.81 ncf('1.5.1.1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 6)).
% 14.99/14.81 ncf('1.5.1.1.1.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 5,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1.1.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 5,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.5.1.1.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 4,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 4,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.5.1.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 3,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.1.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 3,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 ncf('1.5.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 2,bind([[_163029], [951 ^ [994 ^ []]]]))).
% 14.99/14.81 ncf('1.5.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 2,bind([[_163029], [994 ^ []]]))).
% 14.99/14.81 %-----------------------------------------------------
% 14.99/14.81 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------