%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR066+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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 10:57:14 EDT 2023
% Result : Theorem 0.34s 1.41s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : CSR066+1 : TPTP v8.1.2. Released v3.4.0.
% 0.11/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n011.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 23:52:03 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.34/1.41
% 0.34/1.41 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.41 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41 ncf(matrix, plain, [(376 ^ _64870) ^ [_78153] : [-(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)), c_translation_21)))], (378 ^ _64870) ^ [_78206] : [tptp_8_271(_78206, c_theprototypicalshavingrazor_manual), tptpcol_16_25972(_78206)], (2 ^ _64870) ^ [] : [-(genlmt(c_cycorpproductsmt, c_basekb))], (4 ^ _64870) ^ [] : [-(genlmt(c_cycnounlearnermt, c_cycorpproductsmt))], (6 ^ _64870) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)), c_translation_21), c_machinelearningspindleheadmt))], (8 ^ _64870) ^ [_65170, _65172, _65174, _65176] : [-(isa(f_relationexistsallfn(_65176, _65172, _65170, _65174), _65170)), isa(_65176, _65174), relationexistsall(_65172, _65170, _65174)], (18 ^ _64870) ^ [] : [-(resultisaarg(c_relationexistsallfn, n_3))], (20 ^ _64870) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (22 ^ _64870) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt))], (24 ^ _64870) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (26 ^ _64870) ^ [_65699] : [shavingrazor_manual(_65699), -(tptp_8_271(f_relationexistsallfn(_65699, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual), _65699))], (32 ^ _64870) ^ [] : [-(relationexistsall(c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual))], (34 ^ _64870) ^ [] : [-(shavingrazor_manual(c_theprototypicalshavingrazor_manual))], (36 ^ _64870) ^ [_66031, _66033, _66035] : [isa(_66035, _66033), isa(_66035, _66031), disjointwith(_66033, _66031)], (46 ^ _64870) ^ [_66353, _66355, _66357] : [-(genlpreds(_66357, _66353)), genlinverse(_66357, _66355), genlinverse(_66355, _66353)], (56 ^ _64870) ^ [_66662, _66664] : [genlpreds(_66664, _66662), -(predicate(_66662))], (62 ^ _64870) ^ [_66870, _66872] : [genlpreds(_66872, _66870), -(predicate(_66870))], (68 ^ _64870) ^ [_67078, _67080] : [genlpreds(_67080, _67078), -(predicate(_67080))], (74 ^ _64870) ^ [_67286, _67288] : [genlpreds(_67288, _67286), -(predicate(_67288))], (80 ^ _64870) ^ [_67508, _67510, _67512] : [-(genlpreds(_67512, _67508)), genlpreds(_67512, _67510), genlpreds(_67510, _67508)], (90 ^ _64870) ^ [_67803] : [predicate(_67803), -(genlpreds(_67803, _67803))], (96 ^ _64870) ^ [_67991] : [predicate(_67991), -(genlpreds(_67991, _67991))], (102 ^ _64870) ^ [_68193, _68195] : [genlinverse(_68195, _68193), -(binarypredicate(_68193))], (108 ^ _64870) ^ [_68401, _68403] : [genlinverse(_68403, _68401), -(binarypredicate(_68403))], (114 ^ _64870) ^ [_68623, _68625, _68627] : [-(genlinverse(_68623, _68625)), genlinverse(_68627, _68625), genlpreds(_68623, _68627)], (124 ^ _64870) ^ [_68946, _68948, _68950] : [-(genlinverse(_68950, _68946)), genlinverse(_68950, _68948), genlpreds(_68948, _68946)], (134 ^ _64870) ^ [_69255, _69257] : [disjointwith(_69257, _69255), -(collection(_69255))], (140 ^ _64870) ^ [_69463, _69465] : [disjointwith(_69465, _69463), -(collection(_69465))], (146 ^ _64870) ^ [_69671, _69673] : [disjointwith(_69673, _69671), -(disjointwith(_69671, _69673))], (152 ^ _64870) ^ [_69895, _69897, _69899] : [-(disjointwith(_69899, _69895)), disjointwith(_69899, _69897), genls(_69895, _69897)], (162 ^ _64870) ^ [_70218, _70220, _70222] : [-(disjointwith(_70218, _70220)), disjointwith(_70222, _70220), genls(_70218, _70222)], (172 ^ _64870) ^ [_70513] : [isa(_70513, c_shavingrazor_manual), -(shavingrazor_manual(_70513))], (178 ^ _64870) ^ [_70701] : [shavingrazor_manual(_70701), -(isa(_70701, c_shavingrazor_manual))], (184 ^ _64870) ^ [_70889] : [isa(_70889, c_tptpcol_16_25972), -(tptpcol_16_25972(_70889))], (190 ^ _64870) ^ [_71077] : [tptpcol_16_25972(_71077), -(isa(_71077, c_tptpcol_16_25972))], (196 ^ _64870) ^ [_71279, _71281] : [tptp_8_271(_71281, _71279), -(razor(_71279))], (202 ^ _64870) ^ [_71487, _71489] : [tptp_8_271(_71489, _71487), -(tptpcol_5_24579(_71489))], (208 ^ _64870) ^ [_71709, _71711, _71713] : [relationexistsall(_71713, _71711, _71709), -(collection(_71709))], (214 ^ _64870) ^ [_71939, _71941, _71943] : [relationexistsall(_71943, _71941, _71939), -(collection(_71941))], (220 ^ _64870) ^ [_72169, _72171, _72173] : [relationexistsall(_72173, _72171, _72169), -(binarypredicate(_72173))], (226 ^ _64870) ^ [_72371] : [isa(_72371, c_transitivebinarypredicate), -(transitivebinarypredicate(_72371))], (232 ^ _64870) ^ [_72559] : [transitivebinarypredicate(_72559), -(isa(_72559, c_transitivebinarypredicate))], (238 ^ _64870) ^ [_72761, _72763] : [isa(_72763, _72761), -(collection(_72761))], (244 ^ _64870) ^ [_72969, _72971] : [isa(_72971, _72969), -(collection(_72969))], (250 ^ _64870) ^ [_73177, _73179] : [isa(_73179, _73177), -(thing(_73179))], (256 ^ _64870) ^ [_73385, _73387] : [isa(_73387, _73385), -(thing(_73387))], (262 ^ _64870) ^ [_73607, _73609, _73611] : [-(isa(_73611, _73607)), isa(_73611, _73609), genls(_73609, _73607)], (272 ^ _64870) ^ [_73929, _73931, _73933, _73935] : [-(natfunction(f_relationexistsallfn(_73935, _73933, _73931, _73929), c_relationexistsallfn))], (274 ^ _64870) ^ [_74060, _74062, _74064, _74066] : [-(natargument(f_relationexistsallfn(_74066, _74064, _74062, _74060), n_1, _74066))], (276 ^ _64870) ^ [_74192, _74194, _74196, _74198] : [-(natargument(f_relationexistsallfn(_74198, _74196, _74194, _74192), n_2, _74196))], (278 ^ _64870) ^ [_74324, _74326, _74328, _74330] : [-(natargument(f_relationexistsallfn(_74330, _74328, _74326, _74324), n_3, _74326))], (280 ^ _64870) ^ [_74456, _74458, _74460, _74462] : [-(natargument(f_relationexistsallfn(_74462, _74460, _74458, _74456), n_4, _74456))], (282 ^ _64870) ^ [_74588, _74590, _74592, _74594] : [-(thing(f_relationexistsallfn(_74594, _74592, _74590, _74588)))], (284 ^ _64870) ^ [_74705, _74707] : [resultisaarg(_74707, _74705), -(positiveinteger(_74705))], (290 ^ _64870) ^ [_74913, _74915] : [resultisaarg(_74915, _74913), -(function_denotational(_74915))], (296 ^ _64870) ^ [_75092] : [-(natfunction(f_urlfn(_75092), c_urlfn))], (298 ^ _64870) ^ [_75172] : [-(natargument(f_urlfn(_75172), n_1, _75172))], (300 ^ _64870) ^ [_75253] : [-(uniformresourcelocator(f_urlfn(_75253)))], (302 ^ _64870) ^ [_75332] : [-(natfunction(f_urlreferentfn(_75332), c_urlreferentfn))], (304 ^ _64870) ^ [_75412] : [-(natargument(f_urlreferentfn(_75412), n_1, _75412))], (306 ^ _64870) ^ [_75493] : [-(computerdataartifact(f_urlreferentfn(_75493)))], (308 ^ _64870) ^ [_75586, _75588] : [-(natfunction(f_contentmtofcdafromeventfn(_75588, _75586), c_contentmtofcdafromeventfn))], (310 ^ _64870) ^ [_75683, _75685] : [-(natargument(f_contentmtofcdafromeventfn(_75685, _75683), n_1, _75685))], (312 ^ _64870) ^ [_75781, _75783] : [-(natargument(f_contentmtofcdafromeventfn(_75783, _75781), n_2, _75781))], (314 ^ _64870) ^ [_75879, _75881] : [-(microtheory(f_contentmtofcdafromeventfn(_75881, _75879)))], (316 ^ _64870) ^ [] : [-(mtvisible(c_universalvocabularymt))], (318 ^ _64870) ^ [_76043, _76045] : [-(mtvisible(_76043)), mtvisible(_76045), genlmt(_76045, _76043)], (328 ^ _64870) ^ [_76338, _76340] : [genlmt(_76340, _76338), -(microtheory(_76338))], (334 ^ _64870) ^ [_76546, _76548] : [genlmt(_76548, _76546), -(microtheory(_76546))], (340 ^ _64870) ^ [_76754, _76756] : [genlmt(_76756, _76754), -(microtheory(_76756))], (346 ^ _64870) ^ [_76962, _76964] : [genlmt(_76964, _76962), -(microtheory(_76964))], (352 ^ _64870) ^ [_77184, _77186, _77188] : [-(genlmt(_77188, _77184)), genlmt(_77188, _77186), genlmt(_77186, _77184)], (362 ^ _64870) ^ [_77479] : [microtheory(_77479), -(genlmt(_77479, _77479))], (374 ^ _64870) ^ [] : [-(mtvisible(c_basekb))], (368 ^ _64870) ^ [_77667] : [microtheory(_77667), -(genlmt(_77667, _77667))]], input).
% 0.34/1.41 ncf('1',plain,[tptp_8_271(f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual), c_theprototypicalshavingrazor_manual), tptpcol_16_25972(f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual))],start(378 ^ 0,bind([[_78206], [f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual)]]))).
% 0.34/1.41 ncf('1.1',plain,[-(tptp_8_271(f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual), c_theprototypicalshavingrazor_manual)), shavingrazor_manual(c_theprototypicalshavingrazor_manual)],extension(26 ^ 1,bind([[_65699], [c_theprototypicalshavingrazor_manual]]))).
% 0.34/1.41 ncf('1.1.1',plain,[-(shavingrazor_manual(c_theprototypicalshavingrazor_manual))],extension(34 ^ 2)).
% 0.34/1.41 ncf('1.2',plain,[-(tptpcol_16_25972(f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual))), isa(f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual), c_tptpcol_16_25972)],extension(184 ^ 1,bind([[_70889], [f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual)]]))).
% 0.34/1.41 ncf('1.2.1',plain,[-(isa(f_relationexistsallfn(c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual), c_tptpcol_16_25972)), isa(c_theprototypicalshavingrazor_manual, c_shavingrazor_manual), relationexistsall(c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual)],extension(8 ^ 2,bind([[_65170, _65172, _65174, _65176], [c_tptpcol_16_25972, c_tptp_8_271, c_shavingrazor_manual, c_theprototypicalshavingrazor_manual]]))).
% 0.34/1.41 ncf('1.2.1.1',plain,[-(isa(c_theprototypicalshavingrazor_manual, c_shavingrazor_manual)), shavingrazor_manual(c_theprototypicalshavingrazor_manual)],extension(178 ^ 3,bind([[_70701], [c_theprototypicalshavingrazor_manual]]))).
% 0.34/1.41 ncf('1.2.1.1.1',plain,[-(shavingrazor_manual(c_theprototypicalshavingrazor_manual))],extension(34 ^ 4)).
% 0.34/1.41 ncf('1.2.1.2',plain,[-(relationexistsall(c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual))],extension(32 ^ 3)).
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------