%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR072+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:01:54 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR072+1 : TPTP v8.1.2. Released v3.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n022.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 : Thu May 18 23:52:02 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(374 ^ _55172) ^ [] : [-(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)), c_translation_0_885)))], (376 ^ _55172) ^ [] : [genls(c_tptpcol_16_130924, c_tptpcol_15_130923)], (2 ^ _55172) ^ [] : [-(genlmt(c_cycorpproductsmt, c_basekb))], (4 ^ _55172) ^ [] : [-(genlmt(c_cycnounlearnermt, c_cycorpproductsmt))], (6 ^ _55172) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (8 ^ _55172) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)), c_translation_0_885), c_machinelearningspindleheadmt))], (10 ^ _55172) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt))], (12 ^ _55172) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (14 ^ _55172) ^ [] : [-(genls(c_tptpcol_16_130924, c_tptpcol_15_130923))], (16 ^ _55172) ^ [_55642] : [tptpcol_16_130924(_55642), -(tptpcol_15_130923(_55642))], (22 ^ _55172) ^ [_55856, _55858, _55860] : [isa(_55860, _55858), isa(_55860, _55856), disjointwith(_55858, _55856)], (32 ^ _55172) ^ [_56178, _56180, _56182] : [-(genlpreds(_56182, _56178)), genlinverse(_56182, _56180), genlinverse(_56180, _56178)], (42 ^ _55172) ^ [_56487, _56489] : [genlpreds(_56489, _56487), -(predicate(_56487))], (48 ^ _55172) ^ [_56695, _56697] : [genlpreds(_56697, _56695), -(predicate(_56695))], (54 ^ _55172) ^ [_56903, _56905] : [genlpreds(_56905, _56903), -(predicate(_56905))], (60 ^ _55172) ^ [_57111, _57113] : [genlpreds(_57113, _57111), -(predicate(_57113))], (66 ^ _55172) ^ [_57333, _57335, _57337] : [-(genlpreds(_57337, _57333)), genlpreds(_57337, _57335), genlpreds(_57335, _57333)], (76 ^ _55172) ^ [_57628] : [predicate(_57628), -(genlpreds(_57628, _57628))], (82 ^ _55172) ^ [_57816] : [predicate(_57816), -(genlpreds(_57816, _57816))], (88 ^ _55172) ^ [_58018, _58020] : [genlinverse(_58020, _58018), -(binarypredicate(_58018))], (94 ^ _55172) ^ [_58226, _58228] : [genlinverse(_58228, _58226), -(binarypredicate(_58228))], (100 ^ _55172) ^ [_58448, _58450, _58452] : [-(genlinverse(_58448, _58450)), genlinverse(_58452, _58450), genlpreds(_58448, _58452)], (110 ^ _55172) ^ [_58771, _58773, _58775] : [-(genlinverse(_58775, _58771)), genlinverse(_58775, _58773), genlpreds(_58773, _58771)], (120 ^ _55172) ^ [_59080, _59082] : [disjointwith(_59082, _59080), -(collection(_59080))], (126 ^ _55172) ^ [_59288, _59290] : [disjointwith(_59290, _59288), -(collection(_59290))], (132 ^ _55172) ^ [_59496, _59498] : [disjointwith(_59498, _59496), -(disjointwith(_59496, _59498))], (138 ^ _55172) ^ [_59720, _59722, _59724] : [-(disjointwith(_59724, _59720)), disjointwith(_59724, _59722), genls(_59720, _59722)], (148 ^ _55172) ^ [_60043, _60045, _60047] : [-(disjointwith(_60043, _60045)), disjointwith(_60047, _60045), genls(_60043, _60047)], (158 ^ _55172) ^ [_60338] : [isa(_60338, c_tptpcol_15_130923), -(tptpcol_15_130923(_60338))], (164 ^ _55172) ^ [_60526] : [tptpcol_15_130923(_60526), -(isa(_60526, c_tptpcol_15_130923))], (170 ^ _55172) ^ [_60714] : [isa(_60714, c_tptpcol_16_130924), -(tptpcol_16_130924(_60714))], (176 ^ _55172) ^ [_60902] : [tptpcol_16_130924(_60902), -(isa(_60902, c_tptpcol_16_130924))], (182 ^ _55172) ^ [_61104, _61106] : [genls(_61106, _61104), -(collection(_61104))], (188 ^ _55172) ^ [_61312, _61314] : [genls(_61314, _61312), -(collection(_61312))], (194 ^ _55172) ^ [_61520, _61522] : [genls(_61522, _61520), -(collection(_61522))], (200 ^ _55172) ^ [_61728, _61730] : [genls(_61730, _61728), -(collection(_61730))], (206 ^ _55172) ^ [_61950, _61952, _61954] : [-(genls(_61954, _61950)), genls(_61954, _61952), genls(_61952, _61950)], (216 ^ _55172) ^ [_62245] : [collection(_62245), -(genls(_62245, _62245))], (222 ^ _55172) ^ [_62433] : [collection(_62433), -(genls(_62433, _62433))], (228 ^ _55172) ^ [_62649, _62651, _62653] : [-(genls(_62649, _62651)), genls(_62653, _62651), genls(_62649, _62653)], (238 ^ _55172) ^ [_62972, _62974, _62976] : [-(genls(_62976, _62972)), genls(_62976, _62974), genls(_62974, _62972)], (248 ^ _55172) ^ [_63252] : [-(natfunction(f_urlfn(_63252), c_urlfn))], (250 ^ _55172) ^ [_63332] : [-(natargument(f_urlfn(_63332), n_1, _63332))], (252 ^ _55172) ^ [_63413] : [-(uniformresourcelocator(f_urlfn(_63413)))], (254 ^ _55172) ^ [_63492] : [-(natfunction(f_urlreferentfn(_63492), c_urlreferentfn))], (256 ^ _55172) ^ [_63572] : [-(natargument(f_urlreferentfn(_63572), n_1, _63572))], (258 ^ _55172) ^ [_63653] : [-(computerdataartifact(f_urlreferentfn(_63653)))], (260 ^ _55172) ^ [_63746, _63748] : [-(natfunction(f_contentmtofcdafromeventfn(_63748, _63746), c_contentmtofcdafromeventfn))], (262 ^ _55172) ^ [_63843, _63845] : [-(natargument(f_contentmtofcdafromeventfn(_63845, _63843), n_1, _63845))], (264 ^ _55172) ^ [_63941, _63943] : [-(natargument(f_contentmtofcdafromeventfn(_63943, _63941), n_2, _63941))], (266 ^ _55172) ^ [_64039, _64041] : [-(microtheory(f_contentmtofcdafromeventfn(_64041, _64039)))], (268 ^ _55172) ^ [_64136] : [isa(_64136, c_transitivebinarypredicate), -(transitivebinarypredicate(_64136))], (274 ^ _55172) ^ [_64324] : [transitivebinarypredicate(_64324), -(isa(_64324, c_transitivebinarypredicate))], (280 ^ _55172) ^ [_64526, _64528] : [isa(_64528, _64526), -(collection(_64526))], (286 ^ _55172) ^ [_64734, _64736] : [isa(_64736, _64734), -(collection(_64734))], (292 ^ _55172) ^ [_64942, _64944] : [isa(_64944, _64942), -(thing(_64944))], (298 ^ _55172) ^ [_65150, _65152] : [isa(_65152, _65150), -(thing(_65152))], (304 ^ _55172) ^ [_65372, _65374, _65376] : [-(isa(_65376, _65372)), isa(_65376, _65374), genls(_65374, _65372)], (314 ^ _55172) ^ [] : [-(mtvisible(c_universalvocabularymt))], (316 ^ _55172) ^ [_65734, _65736] : [-(mtvisible(_65734)), mtvisible(_65736), genlmt(_65736, _65734)], (326 ^ _55172) ^ [_66029, _66031] : [genlmt(_66031, _66029), -(microtheory(_66029))], (332 ^ _55172) ^ [_66237, _66239] : [genlmt(_66239, _66237), -(microtheory(_66237))], (338 ^ _55172) ^ [_66445, _66447] : [genlmt(_66447, _66445), -(microtheory(_66447))], (344 ^ _55172) ^ [_66653, _66655] : [genlmt(_66655, _66653), -(microtheory(_66655))], (350 ^ _55172) ^ [_66875, _66877, _66879] : [-(genlmt(_66879, _66875)), genlmt(_66879, _66877), genlmt(_66877, _66875)], (360 ^ _55172) ^ [_67170] : [microtheory(_67170), -(genlmt(_67170, _67170))], (372 ^ _55172) ^ [] : [-(mtvisible(c_basekb))], (366 ^ _55172) ^ [_67358] : [microtheory(_67358), -(genlmt(_67358, _67358))]], input).
% 0.33/1.38 ncf('1',plain,[genls(c_tptpcol_16_130924, c_tptpcol_15_130923)],start(376 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(genls(c_tptpcol_16_130924, c_tptpcol_15_130923))],extension(14 ^ 1)).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------