%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO010+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 11:47:18 EDT 2023
% Result : Theorem 0.42s 1.37s
% Output : Proof 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO010+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n002.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:49:34 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.42/1.37
% 0.42/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.42/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/1.37 %-----------------------------------------------------
% 0.42/1.37 ncf(matrix, plain, [(996 ^ _145642) ^ [] : [-(occurrence_of(994 ^ [], tptp0))], (998 ^ _145642) ^ [_179064, _179066] : [leaf_occ(_179064, 994 ^ []), 1003 ^ _145642 : [(1004 ^ _145642) ^ [] : [-(occurrence_of(_179064, tptp1))], (1007 ^ _145642) ^ [] : [-(occurrence_of(1005 ^ [_179064, _179066], tptp2))], (1009 ^ _145642) ^ [] : [-(min_precedes(_179066, 1005 ^ [_179064, _179066], tptp0))]], 1010 ^ _145642 : [(1011 ^ _145642) ^ [] : [-(occurrence_of(_179064, tptp2))], (1014 ^ _145642) ^ [] : [-(occurrence_of(1012 ^ [_179064, _179066], tptp1))], (1016 ^ _145642) ^ [] : [-(min_precedes(_179066, 1012 ^ [_179064, _179066], tptp0))]]], (2 ^ _145642) ^ [_145766] : [-(_145766 = _145766)], (4 ^ _145642) ^ [_145873, _145875] : [_145875 = _145873, -(_145873 = _145875)], (10 ^ _145642) ^ [_146077, _146079, _146081] : [-(_146081 = _146077), _146081 = _146079, _146079 = _146077], (20 ^ _145642) ^ [_146418, _146420, _146422, _146424] : [-(earlier(_146422, _146418)), earlier(_146424, _146420), _146424 = _146422, _146420 = _146418], (34 ^ _145642) ^ [_146834, _146836] : [-(legal(_146834)), _146836 = _146834, legal(_146836)], (44 ^ _145642) ^ [_147157, _147159, _147161, _147163] : [-(precedes(_147161, _147157)), precedes(_147163, _147159), _147163 = _147161, _147159 = _147157], (58 ^ _145642) ^ [_147601, _147603, _147605, _147607] : [-(atocc(_147605, _147601)), atocc(_147607, _147603), _147607 = _147605, _147603 = _147601], (72 ^ _145642) ^ [_148017, _148019] : [-(activity_occurrence(_148017)), _148019 = _148017, activity_occurrence(_148019)], (82 ^ _145642) ^ [_148340, _148342, _148344, _148346] : [-(subactivity(_148344, _148340)), subactivity(_148346, _148342), _148346 = _148344, _148342 = _148340], (96 ^ _145642) ^ [_148784, _148786, _148788, _148790] : [-(root(_148788, _148784)), root(_148790, _148786), _148790 = _148788, _148786 = _148784], (110 ^ _145642) ^ [_149228, _149230, _149232, _149234] : [-(leaf(_149232, _149228)), leaf(_149234, _149230), _149234 = _149232, _149230 = _149228], (124 ^ _145642) ^ [_149644, _149646] : [-(arboreal(_149644)), _149646 = _149644, arboreal(_149646)], (134 ^ _145642) ^ [_149967, _149969, _149971, _149973] : [-(subactivity_occurrence(_149971, _149967)), subactivity_occurrence(_149973, _149969), _149973 = _149971, _149969 = _149967], (148 ^ _145642) ^ [_150411, _150413, _150415, _150417] : [-(root_occ(_150415, _150411)), root_occ(_150417, _150413), _150417 = _150415, _150413 = _150411], (162 ^ _145642) ^ [_150883, _150885, _150887, _150889, _150891, _150893] : [-(next_subocc(_150891, _150887, _150883)), next_subocc(_150893, _150889, _150885), _150893 = _150891, _150889 = _150887, _150885 = _150883], (180 ^ _145642) ^ [_151436, _151438] : [-(activity(_151436)), _151438 = _151436, activity(_151438)], (190 ^ _145642) ^ [_151731, _151733] : [-(atomic(_151731)), _151733 = _151731, atomic(_151733)], (200 ^ _145642) ^ [_152054, _152056, _152058, _152060] : [-(leaf_occ(_152058, _152054)), leaf_occ(_152060, _152056), _152060 = _152058, _152056 = _152054], (214 ^ _145642) ^ [_152498, _152500, _152502, _152504] : [-(occurrence_of(_152502, _152498)), occurrence_of(_152504, _152500), _152504 = _152502, _152500 = _152498], (228 ^ _145642) ^ [_152950, _152952, _152954, _152956, _152958, _152960] : [-(min_precedes(_152958, _152954, _152950)), min_precedes(_152960, _152956, _152952), _152960 = _152958, _152956 = _152954, _152952 = _152950], (246 ^ _145642) ^ [_153577, _153579] : [occurrence_of(_153577, _153579), 249 ^ _145642 : [(250 ^ _145642) ^ [] : [-(activity(_153579))], (252 ^ _145642) ^ [] : [-(activity_occurrence(_153577))]]], (254 ^ _145642) ^ [_153844] : [activity_occurrence(_153844), 258 ^ _145642 : [(259 ^ _145642) ^ [] : [-(activity(257 ^ [_153844]))], (261 ^ _145642) ^ [] : [-(occurrence_of(_153844, 257 ^ [_153844]))]]], (263 ^ _145642) ^ [_154192, _154194, _154196] : [-(_154194 = _154192), occurrence_of(_154196, _154194), occurrence_of(_154196, _154192)], (273 ^ _145642) ^ [_154487] : [activity(_154487), -(subactivity(_154487, _154487))], (279 ^ _145642) ^ [_154689, _154691] : [earlier(_154691, _154689), earlier(_154689, _154691)], (285 ^ _145642) ^ [_154914, _154916, _154918] : [-(earlier(_154918, _154914)), earlier(_154918, _154916), earlier(_154916, _154914)], (295 ^ _145642) ^ [_155237, _155239, _155241] : [earlier(_155241, _155239), earlier(_155237, _155239), -(earlier(_155237, _155241)), -(earlier(_155241, _155237)), -(_155241 = _155237)], (313 ^ _145642) ^ [_155736, _155738] : [occurrence_of(_155738, _155736), 316 ^ _145642 : [(317 ^ _145642) ^ [] : [arboreal(_155738), -(atomic(_155736))], (323 ^ _145642) ^ [] : [atomic(_155736), -(arboreal(_155738))]]], (329 ^ _145642) ^ [_156176] : [legal(_156176), -(arboreal(_156176))], (335 ^ _145642) ^ [_156376, _156378] : [-(legal(_156376)), legal(_156378), earlier(_156376, _156378)], (345 ^ _145642) ^ [_156700, _156702] : [precedes(_156702, _156700), 348 ^ _145642 : [(349 ^ _145642) ^ [] : [-(earlier(_156702, _156700))], (351 ^ _145642) ^ [] : [-(legal(_156700))]]], (353 ^ _145642) ^ [_156935, _156937] : [-(precedes(_156937, _156935)), earlier(_156937, _156935), legal(_156935)], (363 ^ _145642) ^ [_157248, _157250, _157252] : [min_precedes(_157250, _157248, _157252), 368 ^ _145642 : [(369 ^ _145642) ^ [] : [-(subactivity(366 ^ [_157248, _157250, _157252], _157252))], (371 ^ _145642) ^ [] : [-(subactivity(367 ^ [_157248, _157250, _157252], _157252))], (373 ^ _145642) ^ [] : [-(atocc(_157250, 366 ^ [_157248, _157250, _157252]))], (375 ^ _145642) ^ [] : [-(atocc(_157248, 367 ^ [_157248, _157250, _157252]))]]], (377 ^ _145642) ^ [_157898, _157900] : [root(_157898, _157900), 381 ^ _145642 : [(382 ^ _145642) ^ [] : [-(subactivity(380 ^ [_157898, _157900], _157900))], (384 ^ _145642) ^ [] : [-(atocc(_157898, 380 ^ [_157898, _157900]))]]], (386 ^ _145642) ^ [_158267, _158269, _158271] : [min_precedes(_158271, _158269, _158267), 390 ^ _145642 : [(391 ^ _145642) ^ [] : [-(root(389 ^ [_158267, _158269, _158271], _158267))], (393 ^ _145642) ^ [] : [-(min_precedes(389 ^ [_158267, _158269, _158271], _158269, _158267))]]], (395 ^ _145642) ^ [_158657, _158659, _158661] : [min_precedes(_158661, _158659, _158657), root(_158659, _158657)], (401 ^ _145642) ^ [_158890, _158892, _158894] : [min_precedes(_158894, _158892, _158890), -(precedes(_158894, _158892))], (407 ^ _145642) ^ [_159108, _159110] : [root(_159110, _159108), -(legal(_159110))], (413 ^ _145642) ^ [_159316, _159318] : [-(root(_159318, _159316)), atocc(_159318, _159316), legal(_159318)], (423 ^ _145642) ^ [_159641, _159643, _159645, _159647] : [-(min_precedes(_159645, _159643, _159641)), min_precedes(_159647, _159645, _159641), min_precedes(_159647, _159643, _159641), precedes(_159645, _159643)], (437 ^ _145642) ^ [_160077, _160079, _160081] : [min_precedes(_160081, _160079, _160077), atomic(_160077)], (443 ^ _145642) ^ [_160322, _160324, _160326, _160328] : [-(min_precedes(_160326, _160324, _160322)), min_precedes(_160326, _160328, _160322), min_precedes(_160324, _160328, _160322), precedes(_160326, _160324)], (457 ^ _145642) ^ [_160773, _160775] : [leaf(_160775, _160773), 460 ^ _145642 : [(468 ^ _145642) ^ [_161113] : [min_precedes(_160775, _161113, _160773)], (461 ^ _145642) ^ [] : [-(root(_160775, _160773)), -(min_precedes(464 ^ [_160773, _160775], _160775, _160773))]]], (470 ^ _145642) ^ [_161184, _161186] : [-(leaf(_161186, _161184)), 473 ^ _145642 : [(474 ^ _145642) ^ [] : [root(_161186, _161184)], (476 ^ _145642) ^ [_161374] : [min_precedes(_161374, _161186, _161184)]], -(min_precedes(_161186, 477 ^ [_161184, _161186], _161184))], (483 ^ _145642) ^ [_161688, _161690, _161692] : [next_subocc(_161692, _161690, _161688), 486 ^ _145642 : [(487 ^ _145642) ^ [] : [-(min_precedes(_161692, _161690, _161688))], (489 ^ _145642) ^ [_161911] : [min_precedes(_161692, _161911, _161688), min_precedes(_161911, _161690, _161688)]]], (495 ^ _145642) ^ [_162101, _162103, _162105] : [-(next_subocc(_162105, _162103, _162101)), min_precedes(_162105, _162103, _162101), 501 ^ _145642 : [(502 ^ _145642) ^ [] : [-(min_precedes(_162105, 500 ^ [_162101, _162103, _162105], _162101))], (504 ^ _145642) ^ [] : [-(min_precedes(500 ^ [_162101, _162103, _162105], _162103, _162101))]]], (508 ^ _145642) ^ [_162609, _162611] : [atocc(_162611, _162609), 512 ^ _145642 : [(513 ^ _145642) ^ [] : [-(subactivity(_162609, 511 ^ [_162609, _162611]))], (515 ^ _145642) ^ [] : [-(atomic(511 ^ [_162609, _162611]))], (517 ^ _145642) ^ [] : [-(occurrence_of(_162611, 511 ^ [_162609, _162611]))]]], (519 ^ _145642) ^ [_163000, _163002] : [-(atocc(_163002, _163000)), 520 ^ _145642 : [(521 ^ _145642) ^ [_163097] : [subactivity(_163000, _163097), atomic(_163097), occurrence_of(_163002, _163097)]]], (533 ^ _145642) ^ [_163460, _163462] : [subactivity_occurrence(_163462, _163460), 536 ^ _145642 : [(537 ^ _145642) ^ [] : [-(activity_occurrence(_163462))], (539 ^ _145642) ^ [] : [-(activity_occurrence(_163460))]]], (541 ^ _145642) ^ [_163755, _163757, _163759] : [min_precedes(_163757, _163755, _163759), 545 ^ _145642 : [(546 ^ _145642) ^ [] : [-(occurrence_of(544 ^ [_163755, _163757, _163759], _163759))], (548 ^ _145642) ^ [] : [-(subactivity_occurrence(_163757, 544 ^ [_163755, _163757, _163759]))], (550 ^ _145642) ^ [] : [-(subactivity_occurrence(_163755, 544 ^ [_163755, _163757, _163759]))]]], (552 ^ _145642) ^ [_164219, _164221] : [560 ^ _145642 : [(561 ^ _145642) ^ [] : [-(occurrence_of(559 ^ [_164219, _164221], _164221))], (563 ^ _145642) ^ [] : [-(subactivity_occurrence(_164219, 559 ^ [_164219, _164221]))]], root(_164219, _164221), -(atomic(_164221))], (565 ^ _145642) ^ [_164664, _164666] : [573 ^ _145642 : [(574 ^ _145642) ^ [] : [-(root(572 ^ [_164664, _164666], _164666))], (576 ^ _145642) ^ [] : [-(subactivity_occurrence(572 ^ [_164664, _164666], _164664))]], occurrence_of(_164664, _164666), -(atomic(_164666))], (578 ^ _145642) ^ [_165137, _165139, _165141, _165143] : [-(min_precedes(_165139, _165137, _165143)), -(min_precedes(_165137, _165139, _165143)), -(_165139 = _165137), occurrence_of(_165141, _165143), arboreal(_165139), arboreal(_165137), subactivity_occurrence(_165139, _165141), subactivity_occurrence(_165137, _165141)], (608 ^ _145642) ^ [_165975, _165977, _165979, _165981] : [-(subactivity_occurrence(_165981, _165975)), min_precedes(_165981, _165979, _165977), occurrence_of(_165975, _165977), subactivity_occurrence(_165979, _165975)], (622 ^ _145642) ^ [_166421, _166423, _166425, _166427] : [-(subactivity(_166427, _166425)), occurrence_of(_166423, _166427), occurrence_of(_166421, _166425), -(atomic(_166427)), subactivity_occurrence(_166423, _166421)], (640 ^ _145642) ^ [_166949, _166951, _166953] : [-(subactivity_occurrence(_166953, _166949)), subactivity_occurrence(_166953, _166951), subactivity_occurrence(_166951, _166949)], (650 ^ _145642) ^ [_167286, _167288, _167290, _167292] : [666 ^ _145642 : [(667 ^ _145642) ^ [] : [-(subactivity_occurrence(665 ^ [_167286, _167288, _167290, _167292], _167286))], (669 ^ _145642) ^ [] : [subactivity_occurrence(665 ^ [_167286, _167288, _167290, _167292], _167288)]], occurrence_of(_167288, _167292), occurrence_of(_167286, _167290), subactivity(_167292, _167290), -(subactivity_occurrence(_167288, _167286))], (671 ^ _145642) ^ [_167999, _168001] : [root_occ(_168001, _167999), 675 ^ _145642 : [(676 ^ _145642) ^ [] : [-(occurrence_of(_167999, 674 ^ [_167999, _168001]))], (678 ^ _145642) ^ [] : [-(subactivity_occurrence(_168001, _167999))], (680 ^ _145642) ^ [] : [-(root(_168001, 674 ^ [_167999, _168001]))]]], (682 ^ _145642) ^ [_168386, _168388] : [-(root_occ(_168388, _168386)), 683 ^ _145642 : [(684 ^ _145642) ^ [_168484] : [occurrence_of(_168386, _168484), subactivity_occurrence(_168388, _168386), root(_168388, _168484)]]], (696 ^ _145642) ^ [_168878, _168880] : [leaf_occ(_168880, _168878), 700 ^ _145642 : [(701 ^ _145642) ^ [] : [-(occurrence_of(_168878, 699 ^ [_168878, _168880]))], (703 ^ _145642) ^ [] : [-(subactivity_occurrence(_168880, _168878))], (705 ^ _145642) ^ [] : [-(leaf(_168880, 699 ^ [_168878, _168880]))]]], (707 ^ _145642) ^ [_169265, _169267] : [-(leaf_occ(_169267, _169265)), 708 ^ _145642 : [(709 ^ _145642) ^ [_169363] : [occurrence_of(_169265, _169363), subactivity_occurrence(_169267, _169265), leaf(_169267, _169363)]]], (721 ^ _145642) ^ [_169756, _169758, _169760, _169762] : [-(_169762 = _169760), occurrence_of(_169758, _169756), root_occ(_169762, _169758), root_occ(_169760, _169758)], (735 ^ _145642) ^ [_170200, _170202, _170204, _170206] : [-(_170206 = _170204), occurrence_of(_170202, _170200), -(atomic(_170200)), leaf_occ(_170206, _170202), leaf_occ(_170204, _170202)], (753 ^ _145642) ^ [_170728, _170730, _170732] : [760 ^ _145642 : [(761 ^ _145642) ^ [_170943] : [min_precedes(_170730, _170943, _170728)]], occurrence_of(_170732, _170728), leaf_occ(_170730, _170732)], (763 ^ _145642) ^ [_171076, _171078, _171080] : [770 ^ _145642 : [(771 ^ _145642) ^ [_171291] : [min_precedes(_171291, _171078, _171076)]], occurrence_of(_171080, _171076), root_occ(_171078, _171080)], (773 ^ _145642) ^ [_171452, _171454, _171456, _171458, _171460] : [-(_171458 = _171456), next_subocc(_171460, _171458, _171454), next_subocc(_171460, _171456, _171454), occurrence_of(_171452, _171454), subactivity_occurrence(_171456, _171452), subactivity_occurrence(_171458, _171452)], (795 ^ _145642) ^ [_172116, _172118, _172120, _172122] : [-(_172120 = _172118), next_subocc(_172120, _172122, _172116), next_subocc(_172118, _172122, _172116)], (805 ^ _145642) ^ [_172467, _172469, _172471, _172473] : [-(min_precedes(_172469, _172471, _172467)), occurrence_of(_172473, _172467), leaf_occ(_172471, _172473), root_occ(_172469, _172473), -(_172471 = _172469)], (823 ^ _145642) ^ [_173013, _173015, _173017, _173019] : [-(_173013 = _173015), occurrence_of(_173017, _173019), subactivity_occurrence(_173015, _173017), root_occ(_173013, _173017), arboreal(_173015), -(min_precedes(_173013, _173015, _173019))], (845 ^ _145642) ^ [_173654, _173656, _173658, _173660] : [-(_173654 = _173656), occurrence_of(_173658, _173660), subactivity_occurrence(_173656, _173658), leaf_occ(_173654, _173658), arboreal(_173656), -(min_precedes(_173656, _173654, _173660))], (867 ^ _145642) ^ [_174281, _174283, _174285] : [next_subocc(_174285, _174283, _174281), 870 ^ _145642 : [(871 ^ _145642) ^ [] : [-(arboreal(_174285))], (873 ^ _145642) ^ [] : [-(arboreal(_174283))]]], (875 ^ _145642) ^ [_174572, _174574] : [883 ^ _145642 : [(884 ^ _145642) ^ [] : [-(occurrence_of(882 ^ [_174572, _174574], _174572))], (886 ^ _145642) ^ [] : [-(leaf_occ(_174574, 882 ^ [_174572, _174574]))]], leaf(_174574, _174572), -(atomic(_174572))], (888 ^ _145642) ^ [_175031, _175033, _175035] : [min_precedes(_175035, _175033, _175031), -(arboreal(_175035))], (894 ^ _145642) ^ [_175289, _175291, _175293, _175295, _175297] : [-(min_precedes(_175291, _175293, _175297)), occurrence_of(_175295, _175297), root_occ(_175291, _175295), leaf_occ(_175289, _175295), subactivity_occurrence(_175293, _175295), min_precedes(_175293, _175289, _175297), -(_175293 = _175291)], (971 ^ _145642) ^ [] : [-(activity(tptp0))], (973 ^ _145642) ^ [] : [atomic(tptp0)], (975 ^ _145642) ^ [] : [-(atomic(tptp4))], (977 ^ _145642) ^ [] : [-(atomic(tptp1))], (979 ^ _145642) ^ [] : [-(atomic(tptp2))], (981 ^ _145642) ^ [] : [-(atomic(tptp3))], (983 ^ _145642) ^ [] : [tptp4 = tptp3], (985 ^ _145642) ^ [] : [tptp4 = tptp1], (987 ^ _145642) ^ [] : [tptp4 = tptp2], (989 ^ _145642) ^ [] : [tptp3 = tptp1], (991 ^ _145642) ^ [] : [tptp3 = tptp2], (993 ^ _145642) ^ [] : [tptp1 = tptp2], (946 ^ _145642) ^ [_176797] : [occurrence_of(_176797, tptp0), 952 ^ _145642 : [(953 ^ _145642) ^ [] : [-(occurrence_of(949 ^ [_176797], tptp3))], (955 ^ _145642) ^ [] : [-(root_occ(949 ^ [_176797], _176797))], (957 ^ _145642) ^ [] : [-(occurrence_of(950 ^ [_176797], tptp4))], (959 ^ _145642) ^ [] : [-(next_subocc(949 ^ [_176797], 950 ^ [_176797], tptp0))], (967 ^ _145642) ^ [] : [-(next_subocc(950 ^ [_176797], 951 ^ [_176797], tptp0))], (969 ^ _145642) ^ [] : [-(leaf_occ(951 ^ [_176797], _176797))], (961 ^ _145642) ^ [] : [-(occurrence_of(951 ^ [_176797], tptp1)), -(occurrence_of(951 ^ [_176797], tptp2))]]], (920 ^ _145642) ^ [_176071, _176073, _176075, _176077, _176079] : [-(min_precedes(_176075, _176071, _176079)), occurrence_of(_176077, _176079), root_occ(_176073, _176077), leaf_occ(_176071, _176077), subactivity_occurrence(_176075, _176077), min_precedes(_176073, _176075, _176079), -(_176075 = _176071)]], input).
% 0.42/1.37 ncf('1',plain,[761 : min_precedes(951 ^ [994 ^ []], 1005 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0), 761 : occurrence_of(994 ^ [], tptp0), 761 : leaf_occ(951 ^ [994 ^ []], 994 ^ [])],start(753 ^ 0,bind([[_170728, _170730, _170732, _170943], [tptp0, 951 ^ [994 ^ []], 994 ^ [], 1005 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]]]]))).
% 0.42/1.37 ncf('1.1',plain,[-(min_precedes(951 ^ [994 ^ []], 1005 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0)), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 1016 : -(min_precedes(951 ^ [994 ^ []], 1012 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0))],extension(998 ^ 3,bind([[_179064, _179066], [951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 0.42/1.37 ncf('1.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 4,bind([[_176797], [994 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 5)).
% 0.42/1.37 ncf('1.1.2',plain,[min_precedes(951 ^ [994 ^ []], 1012 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0)],extension(761 ^ 6,bind([[_170943], [1012 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]]]]))).
% 0.42/1.37 ncf('1.2',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 1)).
% 0.42/1.37 ncf('1.3',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(200 ^ 1,bind([[_152054, _152056, _152058, _152060], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 0.42/1.37 ncf('1.3.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 2,bind([[_176797], [994 ^ []]]))).
% 0.42/1.37 ncf('1.3.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 3)).
% 0.42/1.37 ncf('1.3.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 2,bind([[_145766], [951 ^ [994 ^ []]]]))).
% 0.42/1.37 ncf('1.3.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 2,bind([[_145766], [994 ^ []]]))).
% 0.42/1.37 %-----------------------------------------------------
% 0.42/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------