%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PRO011+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:19 EDT 2023
% Result : Theorem 0.39s 1.37s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : PRO011+3 : TPTP v8.1.2. Released v4.0.0.
% 0.10/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:29:53 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.39/1.37
% 0.39/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.39/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/1.37 %-----------------------------------------------------
% 0.39/1.37 ncf(matrix, plain, [(996 ^ _146436) ^ [] : [-(occurrence_of(994 ^ [], tptp0))], (998 ^ _146436) ^ [_179870, _179872] : [leaf_occ(_179870, 994 ^ []), 1003 ^ _146436 : [(1004 ^ _146436) ^ [] : [-(occurrence_of(_179870, tptp1))], (1007 ^ _146436) ^ [] : [-(occurrence_of(1005 ^ [_179870, _179872], tptp2))], (1009 ^ _146436) ^ [] : [-(subactivity_occurrence(1005 ^ [_179870, _179872], 994 ^ []))], (1011 ^ _146436) ^ [] : [-(min_precedes(_179872, 1005 ^ [_179870, _179872], tptp0))]], 1012 ^ _146436 : [(1013 ^ _146436) ^ [] : [-(occurrence_of(_179870, tptp2))], (1016 ^ _146436) ^ [] : [-(occurrence_of(1014 ^ [_179870, _179872], tptp1))], (1018 ^ _146436) ^ [] : [-(subactivity_occurrence(1014 ^ [_179870, _179872], 994 ^ []))], (1020 ^ _146436) ^ [] : [-(min_precedes(_179872, 1014 ^ [_179870, _179872], tptp0))]]], (2 ^ _146436) ^ [_146560] : [-(_146560 = _146560)], (4 ^ _146436) ^ [_146667, _146669] : [_146669 = _146667, -(_146667 = _146669)], (10 ^ _146436) ^ [_146871, _146873, _146875] : [-(_146875 = _146871), _146875 = _146873, _146873 = _146871], (20 ^ _146436) ^ [_147212, _147214, _147216, _147218] : [-(earlier(_147216, _147212)), earlier(_147218, _147214), _147218 = _147216, _147214 = _147212], (34 ^ _146436) ^ [_147628, _147630] : [-(legal(_147628)), _147630 = _147628, legal(_147630)], (44 ^ _146436) ^ [_147951, _147953, _147955, _147957] : [-(precedes(_147955, _147951)), precedes(_147957, _147953), _147957 = _147955, _147953 = _147951], (58 ^ _146436) ^ [_148395, _148397, _148399, _148401] : [-(atocc(_148399, _148395)), atocc(_148401, _148397), _148401 = _148399, _148397 = _148395], (72 ^ _146436) ^ [_148811, _148813] : [-(activity_occurrence(_148811)), _148813 = _148811, activity_occurrence(_148813)], (82 ^ _146436) ^ [_149134, _149136, _149138, _149140] : [-(subactivity(_149138, _149134)), subactivity(_149140, _149136), _149140 = _149138, _149136 = _149134], (96 ^ _146436) ^ [_149578, _149580, _149582, _149584] : [-(root(_149582, _149578)), root(_149584, _149580), _149584 = _149582, _149580 = _149578], (110 ^ _146436) ^ [_150022, _150024, _150026, _150028] : [-(leaf(_150026, _150022)), leaf(_150028, _150024), _150028 = _150026, _150024 = _150022], (124 ^ _146436) ^ [_150438, _150440] : [-(arboreal(_150438)), _150440 = _150438, arboreal(_150440)], (134 ^ _146436) ^ [_150761, _150763, _150765, _150767] : [-(root_occ(_150765, _150761)), root_occ(_150767, _150763), _150767 = _150765, _150763 = _150761], (148 ^ _146436) ^ [_151233, _151235, _151237, _151239, _151241, _151243] : [-(next_subocc(_151241, _151237, _151233)), next_subocc(_151243, _151239, _151235), _151243 = _151241, _151239 = _151237, _151235 = _151233], (166 ^ _146436) ^ [_151786, _151788] : [-(activity(_151786)), _151788 = _151786, activity(_151788)], (176 ^ _146436) ^ [_152081, _152083] : [-(atomic(_152081)), _152083 = _152081, atomic(_152083)], (186 ^ _146436) ^ [_152404, _152406, _152408, _152410] : [-(leaf_occ(_152408, _152404)), leaf_occ(_152410, _152406), _152410 = _152408, _152406 = _152404], (200 ^ _146436) ^ [_152848, _152850, _152852, _152854] : [-(occurrence_of(_152852, _152848)), occurrence_of(_152854, _152850), _152854 = _152852, _152850 = _152848], (214 ^ _146436) ^ [_153292, _153294, _153296, _153298] : [-(subactivity_occurrence(_153296, _153292)), subactivity_occurrence(_153298, _153294), _153298 = _153296, _153294 = _153292], (228 ^ _146436) ^ [_153744, _153746, _153748, _153750, _153752, _153754] : [-(min_precedes(_153752, _153748, _153744)), min_precedes(_153754, _153750, _153746), _153754 = _153752, _153750 = _153748, _153746 = _153744], (246 ^ _146436) ^ [_154371, _154373] : [occurrence_of(_154371, _154373), 249 ^ _146436 : [(250 ^ _146436) ^ [] : [-(activity(_154373))], (252 ^ _146436) ^ [] : [-(activity_occurrence(_154371))]]], (254 ^ _146436) ^ [_154638] : [activity_occurrence(_154638), 258 ^ _146436 : [(259 ^ _146436) ^ [] : [-(activity(257 ^ [_154638]))], (261 ^ _146436) ^ [] : [-(occurrence_of(_154638, 257 ^ [_154638]))]]], (263 ^ _146436) ^ [_154986, _154988, _154990] : [-(_154988 = _154986), occurrence_of(_154990, _154988), occurrence_of(_154990, _154986)], (273 ^ _146436) ^ [_155281] : [activity(_155281), -(subactivity(_155281, _155281))], (279 ^ _146436) ^ [_155483, _155485] : [earlier(_155485, _155483), earlier(_155483, _155485)], (285 ^ _146436) ^ [_155708, _155710, _155712] : [-(earlier(_155712, _155708)), earlier(_155712, _155710), earlier(_155710, _155708)], (295 ^ _146436) ^ [_156031, _156033, _156035] : [earlier(_156035, _156033), earlier(_156031, _156033), -(earlier(_156031, _156035)), -(earlier(_156035, _156031)), -(_156035 = _156031)], (313 ^ _146436) ^ [_156530, _156532] : [occurrence_of(_156532, _156530), 316 ^ _146436 : [(317 ^ _146436) ^ [] : [arboreal(_156532), -(atomic(_156530))], (323 ^ _146436) ^ [] : [atomic(_156530), -(arboreal(_156532))]]], (329 ^ _146436) ^ [_156970] : [legal(_156970), -(arboreal(_156970))], (335 ^ _146436) ^ [_157170, _157172] : [-(legal(_157170)), legal(_157172), earlier(_157170, _157172)], (345 ^ _146436) ^ [_157494, _157496] : [precedes(_157496, _157494), 348 ^ _146436 : [(349 ^ _146436) ^ [] : [-(earlier(_157496, _157494))], (351 ^ _146436) ^ [] : [-(legal(_157494))]]], (353 ^ _146436) ^ [_157729, _157731] : [-(precedes(_157731, _157729)), earlier(_157731, _157729), legal(_157729)], (363 ^ _146436) ^ [_158042, _158044, _158046] : [min_precedes(_158044, _158042, _158046), 368 ^ _146436 : [(369 ^ _146436) ^ [] : [-(subactivity(366 ^ [_158042, _158044, _158046], _158046))], (371 ^ _146436) ^ [] : [-(subactivity(367 ^ [_158042, _158044, _158046], _158046))], (373 ^ _146436) ^ [] : [-(atocc(_158044, 366 ^ [_158042, _158044, _158046]))], (375 ^ _146436) ^ [] : [-(atocc(_158042, 367 ^ [_158042, _158044, _158046]))]]], (377 ^ _146436) ^ [_158692, _158694] : [root(_158692, _158694), 381 ^ _146436 : [(382 ^ _146436) ^ [] : [-(subactivity(380 ^ [_158692, _158694], _158694))], (384 ^ _146436) ^ [] : [-(atocc(_158692, 380 ^ [_158692, _158694]))]]], (386 ^ _146436) ^ [_159061, _159063, _159065] : [min_precedes(_159065, _159063, _159061), 390 ^ _146436 : [(391 ^ _146436) ^ [] : [-(root(389 ^ [_159061, _159063, _159065], _159061))], (393 ^ _146436) ^ [] : [-(min_precedes(389 ^ [_159061, _159063, _159065], _159063, _159061))]]], (395 ^ _146436) ^ [_159451, _159453, _159455] : [min_precedes(_159455, _159453, _159451), root(_159453, _159451)], (401 ^ _146436) ^ [_159684, _159686, _159688] : [min_precedes(_159688, _159686, _159684), -(precedes(_159688, _159686))], (407 ^ _146436) ^ [_159902, _159904] : [root(_159904, _159902), -(legal(_159904))], (413 ^ _146436) ^ [_160110, _160112] : [-(root(_160112, _160110)), atocc(_160112, _160110), legal(_160112)], (423 ^ _146436) ^ [_160435, _160437, _160439, _160441] : [-(min_precedes(_160439, _160437, _160435)), min_precedes(_160441, _160439, _160435), min_precedes(_160441, _160437, _160435), precedes(_160439, _160437)], (437 ^ _146436) ^ [_160871, _160873, _160875] : [min_precedes(_160875, _160873, _160871), atomic(_160871)], (443 ^ _146436) ^ [_161116, _161118, _161120, _161122] : [-(min_precedes(_161120, _161118, _161116)), min_precedes(_161120, _161122, _161116), min_precedes(_161118, _161122, _161116), precedes(_161120, _161118)], (457 ^ _146436) ^ [_161567, _161569] : [leaf(_161569, _161567), 460 ^ _146436 : [(468 ^ _146436) ^ [_161907] : [min_precedes(_161569, _161907, _161567)], (461 ^ _146436) ^ [] : [-(root(_161569, _161567)), -(min_precedes(464 ^ [_161567, _161569], _161569, _161567))]]], (470 ^ _146436) ^ [_161978, _161980] : [-(leaf(_161980, _161978)), 473 ^ _146436 : [(474 ^ _146436) ^ [] : [root(_161980, _161978)], (476 ^ _146436) ^ [_162168] : [min_precedes(_162168, _161980, _161978)]], -(min_precedes(_161980, 477 ^ [_161978, _161980], _161978))], (483 ^ _146436) ^ [_162482, _162484, _162486] : [next_subocc(_162486, _162484, _162482), 486 ^ _146436 : [(487 ^ _146436) ^ [] : [-(min_precedes(_162486, _162484, _162482))], (489 ^ _146436) ^ [_162705] : [min_precedes(_162486, _162705, _162482), min_precedes(_162705, _162484, _162482)]]], (495 ^ _146436) ^ [_162895, _162897, _162899] : [-(next_subocc(_162899, _162897, _162895)), min_precedes(_162899, _162897, _162895), 501 ^ _146436 : [(502 ^ _146436) ^ [] : [-(min_precedes(_162899, 500 ^ [_162895, _162897, _162899], _162895))], (504 ^ _146436) ^ [] : [-(min_precedes(500 ^ [_162895, _162897, _162899], _162897, _162895))]]], (508 ^ _146436) ^ [_163403, _163405] : [atocc(_163405, _163403), 512 ^ _146436 : [(513 ^ _146436) ^ [] : [-(subactivity(_163403, 511 ^ [_163403, _163405]))], (515 ^ _146436) ^ [] : [-(atomic(511 ^ [_163403, _163405]))], (517 ^ _146436) ^ [] : [-(occurrence_of(_163405, 511 ^ [_163403, _163405]))]]], (519 ^ _146436) ^ [_163794, _163796] : [-(atocc(_163796, _163794)), 520 ^ _146436 : [(521 ^ _146436) ^ [_163891] : [subactivity(_163794, _163891), atomic(_163891), occurrence_of(_163796, _163891)]]], (533 ^ _146436) ^ [_164254, _164256] : [subactivity_occurrence(_164256, _164254), 536 ^ _146436 : [(537 ^ _146436) ^ [] : [-(activity_occurrence(_164256))], (539 ^ _146436) ^ [] : [-(activity_occurrence(_164254))]]], (541 ^ _146436) ^ [_164549, _164551, _164553] : [min_precedes(_164551, _164549, _164553), 545 ^ _146436 : [(546 ^ _146436) ^ [] : [-(occurrence_of(544 ^ [_164549, _164551, _164553], _164553))], (548 ^ _146436) ^ [] : [-(subactivity_occurrence(_164551, 544 ^ [_164549, _164551, _164553]))], (550 ^ _146436) ^ [] : [-(subactivity_occurrence(_164549, 544 ^ [_164549, _164551, _164553]))]]], (552 ^ _146436) ^ [_165013, _165015] : [560 ^ _146436 : [(561 ^ _146436) ^ [] : [-(occurrence_of(559 ^ [_165013, _165015], _165015))], (563 ^ _146436) ^ [] : [-(subactivity_occurrence(_165013, 559 ^ [_165013, _165015]))]], root(_165013, _165015), -(atomic(_165015))], (565 ^ _146436) ^ [_165458, _165460] : [573 ^ _146436 : [(574 ^ _146436) ^ [] : [-(root(572 ^ [_165458, _165460], _165460))], (576 ^ _146436) ^ [] : [-(subactivity_occurrence(572 ^ [_165458, _165460], _165458))]], occurrence_of(_165458, _165460), -(atomic(_165460))], (578 ^ _146436) ^ [_165931, _165933, _165935, _165937] : [-(min_precedes(_165933, _165931, _165937)), -(min_precedes(_165931, _165933, _165937)), -(_165933 = _165931), occurrence_of(_165935, _165937), arboreal(_165933), arboreal(_165931), subactivity_occurrence(_165933, _165935), subactivity_occurrence(_165931, _165935)], (608 ^ _146436) ^ [_166769, _166771, _166773, _166775] : [-(subactivity_occurrence(_166775, _166769)), min_precedes(_166775, _166773, _166771), occurrence_of(_166769, _166771), subactivity_occurrence(_166773, _166769)], (622 ^ _146436) ^ [_167215, _167217, _167219, _167221] : [-(subactivity(_167221, _167219)), occurrence_of(_167217, _167221), occurrence_of(_167215, _167219), -(atomic(_167221)), subactivity_occurrence(_167217, _167215)], (640 ^ _146436) ^ [_167743, _167745, _167747] : [-(subactivity_occurrence(_167747, _167743)), subactivity_occurrence(_167747, _167745), subactivity_occurrence(_167745, _167743)], (650 ^ _146436) ^ [_168080, _168082, _168084, _168086] : [666 ^ _146436 : [(667 ^ _146436) ^ [] : [-(subactivity_occurrence(665 ^ [_168080, _168082, _168084, _168086], _168080))], (669 ^ _146436) ^ [] : [subactivity_occurrence(665 ^ [_168080, _168082, _168084, _168086], _168082)]], occurrence_of(_168082, _168086), occurrence_of(_168080, _168084), subactivity(_168086, _168084), -(subactivity_occurrence(_168082, _168080))], (671 ^ _146436) ^ [_168793, _168795] : [root_occ(_168795, _168793), 675 ^ _146436 : [(676 ^ _146436) ^ [] : [-(occurrence_of(_168793, 674 ^ [_168793, _168795]))], (678 ^ _146436) ^ [] : [-(subactivity_occurrence(_168795, _168793))], (680 ^ _146436) ^ [] : [-(root(_168795, 674 ^ [_168793, _168795]))]]], (682 ^ _146436) ^ [_169180, _169182] : [-(root_occ(_169182, _169180)), 683 ^ _146436 : [(684 ^ _146436) ^ [_169278] : [occurrence_of(_169180, _169278), subactivity_occurrence(_169182, _169180), root(_169182, _169278)]]], (696 ^ _146436) ^ [_169672, _169674] : [leaf_occ(_169674, _169672), 700 ^ _146436 : [(701 ^ _146436) ^ [] : [-(occurrence_of(_169672, 699 ^ [_169672, _169674]))], (703 ^ _146436) ^ [] : [-(subactivity_occurrence(_169674, _169672))], (705 ^ _146436) ^ [] : [-(leaf(_169674, 699 ^ [_169672, _169674]))]]], (707 ^ _146436) ^ [_170059, _170061] : [-(leaf_occ(_170061, _170059)), 708 ^ _146436 : [(709 ^ _146436) ^ [_170157] : [occurrence_of(_170059, _170157), subactivity_occurrence(_170061, _170059), leaf(_170061, _170157)]]], (721 ^ _146436) ^ [_170550, _170552, _170554, _170556] : [-(_170556 = _170554), occurrence_of(_170552, _170550), root_occ(_170556, _170552), root_occ(_170554, _170552)], (735 ^ _146436) ^ [_170994, _170996, _170998, _171000] : [-(_171000 = _170998), occurrence_of(_170996, _170994), -(atomic(_170994)), leaf_occ(_171000, _170996), leaf_occ(_170998, _170996)], (753 ^ _146436) ^ [_171522, _171524, _171526] : [760 ^ _146436 : [(761 ^ _146436) ^ [_171737] : [min_precedes(_171524, _171737, _171522)]], occurrence_of(_171526, _171522), leaf_occ(_171524, _171526)], (763 ^ _146436) ^ [_171870, _171872, _171874] : [770 ^ _146436 : [(771 ^ _146436) ^ [_172085] : [min_precedes(_172085, _171872, _171870)]], occurrence_of(_171874, _171870), root_occ(_171872, _171874)], (773 ^ _146436) ^ [_172246, _172248, _172250, _172252, _172254] : [-(_172252 = _172250), next_subocc(_172254, _172252, _172248), next_subocc(_172254, _172250, _172248), occurrence_of(_172246, _172248), subactivity_occurrence(_172250, _172246), subactivity_occurrence(_172252, _172246)], (795 ^ _146436) ^ [_172910, _172912, _172914, _172916] : [-(_172914 = _172912), next_subocc(_172914, _172916, _172910), next_subocc(_172912, _172916, _172910)], (805 ^ _146436) ^ [_173261, _173263, _173265, _173267] : [-(min_precedes(_173263, _173265, _173261)), occurrence_of(_173267, _173261), leaf_occ(_173265, _173267), root_occ(_173263, _173267), -(_173265 = _173263)], (823 ^ _146436) ^ [_173807, _173809, _173811, _173813] : [-(_173807 = _173809), occurrence_of(_173811, _173813), subactivity_occurrence(_173809, _173811), root_occ(_173807, _173811), arboreal(_173809), -(min_precedes(_173807, _173809, _173813))], (845 ^ _146436) ^ [_174448, _174450, _174452, _174454] : [-(_174448 = _174450), occurrence_of(_174452, _174454), subactivity_occurrence(_174450, _174452), leaf_occ(_174448, _174452), arboreal(_174450), -(min_precedes(_174450, _174448, _174454))], (867 ^ _146436) ^ [_175075, _175077, _175079] : [next_subocc(_175079, _175077, _175075), 870 ^ _146436 : [(871 ^ _146436) ^ [] : [-(arboreal(_175079))], (873 ^ _146436) ^ [] : [-(arboreal(_175077))]]], (875 ^ _146436) ^ [_175366, _175368] : [883 ^ _146436 : [(884 ^ _146436) ^ [] : [-(occurrence_of(882 ^ [_175366, _175368], _175366))], (886 ^ _146436) ^ [] : [-(leaf_occ(_175368, 882 ^ [_175366, _175368]))]], leaf(_175368, _175366), -(atomic(_175366))], (888 ^ _146436) ^ [_175825, _175827, _175829] : [min_precedes(_175829, _175827, _175825), -(arboreal(_175829))], (894 ^ _146436) ^ [_176083, _176085, _176087, _176089, _176091] : [-(min_precedes(_176085, _176087, _176091)), occurrence_of(_176089, _176091), root_occ(_176085, _176089), leaf_occ(_176083, _176089), subactivity_occurrence(_176087, _176089), min_precedes(_176087, _176083, _176091), -(_176087 = _176085)], (971 ^ _146436) ^ [] : [-(activity(tptp0))], (973 ^ _146436) ^ [] : [atomic(tptp0)], (975 ^ _146436) ^ [] : [-(atomic(tptp4))], (977 ^ _146436) ^ [] : [-(atomic(tptp1))], (979 ^ _146436) ^ [] : [-(atomic(tptp2))], (981 ^ _146436) ^ [] : [-(atomic(tptp3))], (983 ^ _146436) ^ [] : [tptp4 = tptp3], (985 ^ _146436) ^ [] : [tptp4 = tptp1], (987 ^ _146436) ^ [] : [tptp4 = tptp2], (989 ^ _146436) ^ [] : [tptp3 = tptp1], (991 ^ _146436) ^ [] : [tptp3 = tptp2], (993 ^ _146436) ^ [] : [tptp1 = tptp2], (946 ^ _146436) ^ [_177591] : [occurrence_of(_177591, tptp0), 952 ^ _146436 : [(953 ^ _146436) ^ [] : [-(occurrence_of(949 ^ [_177591], tptp3))], (955 ^ _146436) ^ [] : [-(root_occ(949 ^ [_177591], _177591))], (957 ^ _146436) ^ [] : [-(occurrence_of(950 ^ [_177591], tptp4))], (959 ^ _146436) ^ [] : [-(next_subocc(949 ^ [_177591], 950 ^ [_177591], tptp0))], (967 ^ _146436) ^ [] : [-(next_subocc(950 ^ [_177591], 951 ^ [_177591], tptp0))], (969 ^ _146436) ^ [] : [-(leaf_occ(951 ^ [_177591], _177591))], (961 ^ _146436) ^ [] : [-(occurrence_of(951 ^ [_177591], tptp1)), -(occurrence_of(951 ^ [_177591], tptp2))]]], (920 ^ _146436) ^ [_176865, _176867, _176869, _176871, _176873] : [-(min_precedes(_176869, _176865, _176873)), occurrence_of(_176871, _176873), root_occ(_176867, _176871), leaf_occ(_176865, _176871), subactivity_occurrence(_176869, _176871), min_precedes(_176867, _176869, _176873), -(_176869 = _176865)]], input).
% 0.39/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([[_171522, _171524, _171526, _171737], [tptp0, 951 ^ [994 ^ []], 994 ^ [], 1005 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]]]]))).
% 0.39/1.37 ncf('1.1',plain,[-(min_precedes(951 ^ [994 ^ []], 1005 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0)), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 1020 : -(min_precedes(951 ^ [994 ^ []], 1014 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0))],extension(998 ^ 3,bind([[_179870, _179872], [951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 0.39/1.37 ncf('1.1.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 4,bind([[_177591], [994 ^ []]]))).
% 0.39/1.37 ncf('1.1.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 5)).
% 0.39/1.37 ncf('1.1.2',plain,[min_precedes(951 ^ [994 ^ []], 1014 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]], tptp0)],extension(761 ^ 6,bind([[_171737], [1014 ^ [951 ^ [994 ^ []], 951 ^ [994 ^ []]]]]))).
% 0.39/1.37 ncf('1.2',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 1)).
% 0.39/1.37 ncf('1.3',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), leaf_occ(951 ^ [994 ^ []], 994 ^ []), 951 ^ [994 ^ []] = 951 ^ [994 ^ []], 994 ^ [] = 994 ^ []],extension(186 ^ 1,bind([[_152404, _152406, _152408, _152410], [994 ^ [], 994 ^ [], 951 ^ [994 ^ []], 951 ^ [994 ^ []]]]))).
% 0.39/1.37 ncf('1.3.1',plain,[-(leaf_occ(951 ^ [994 ^ []], 994 ^ [])), occurrence_of(994 ^ [], tptp0)],extension(946 ^ 2,bind([[_177591], [994 ^ []]]))).
% 0.39/1.37 ncf('1.3.1.1',plain,[-(occurrence_of(994 ^ [], tptp0))],extension(996 ^ 3)).
% 0.39/1.37 ncf('1.3.2',plain,[-(951 ^ [994 ^ []] = 951 ^ [994 ^ []])],extension(2 ^ 2,bind([[_146560], [951 ^ [994 ^ []]]]))).
% 0.39/1.37 ncf('1.3.3',plain,[-(994 ^ [] = 994 ^ [])],extension(2 ^ 2,bind([[_146560], [994 ^ []]]))).
% 0.39/1.37 %-----------------------------------------------------
% 0.39/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------