%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR050+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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:44:08 EDT 2023
% Result : Theorem 0.91s 1.38s
% Output : Proof 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR050+1 : TPTP v8.1.2. Released v3.4.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n014.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 00:47:27 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.91/1.38
% 0.91/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.91/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/1.38 %-----------------------------------------------------
% 0.91/1.38 ncf(matrix, plain, [(454 ^ _73499) ^ [] : [-(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32)))], (456 ^ _73499) ^ [] : [tptptypes_7_691(c_tptpcol_16_26939, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma))], (2 ^ _73499) ^ [] : [-(genlmt(c_ldscdemonstrationspindleheadmt, c_currentworlddatacollectormt_nonhomocentric))], (4 ^ _73499) ^ [] : [-(genlmt(c_cycorpproductsmt, c_basekb))], (6 ^ _73499) ^ [] : [-(genlmt(c_cycnounlearnermt, c_cycorpproductsmt))], (8 ^ _73499) ^ [] : [-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32), c_machinelearningspindleheadmt))], (10 ^ _73499) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_miptdatabase19681997_termsmt))], (12 ^ _73499) ^ [] : [-(genlmt(c_miptdatabase19681997_termsmt, c_ldscgeneralcollectormt))], (14 ^ _73499) ^ [] : [-(genlmt(c_ldscgeneralcollectormt, c_ldscdemonstrationspindleheadmt))], (16 ^ _73499) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (18 ^ _73499) ^ [] : [-(genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt))], (20 ^ _73499) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (22 ^ _73499) ^ [] : [-(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))], (24 ^ _73499) ^ [_74195, _74197] : [tptptypes_8_692(_74197, _74195), -(tptptypes_7_691(_74195, _74197))], (30 ^ _73499) ^ [] : [-(genlpreds(c_tptptypes_9_693, c_tptptypes_8_692))], (32 ^ _73499) ^ [_74458, _74460] : [tptptypes_9_693(_74460, _74458), -(tptptypes_8_692(_74460, _74458))], (38 ^ _73499) ^ [] : [mtvisible(c_currentworlddatacollectormt_nonhomocentric), -(tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma), c_tptpcol_16_26939))], (44 ^ _73499) ^ [_74801, _74803, _74805] : [isa(_74805, _74803), isa(_74805, _74801), disjointwith(_74803, _74801)], (54 ^ _73499) ^ [_75123, _75125, _75127] : [-(genlpreds(_75127, _75123)), genlinverse(_75127, _75125), genlinverse(_75125, _75123)], (64 ^ _73499) ^ [_75432, _75434] : [disjointwith(_75434, _75432), -(collection(_75432))], (70 ^ _73499) ^ [_75640, _75642] : [disjointwith(_75642, _75640), -(collection(_75642))], (76 ^ _73499) ^ [_75848, _75850] : [disjointwith(_75850, _75848), -(disjointwith(_75848, _75850))], (82 ^ _73499) ^ [_76072, _76074, _76076] : [-(disjointwith(_76076, _76072)), disjointwith(_76076, _76074), genls(_76072, _76074)], (92 ^ _73499) ^ [_76395, _76397, _76399] : [-(disjointwith(_76395, _76397)), disjointwith(_76399, _76397), genls(_76395, _76399)], (102 ^ _73499) ^ [_76690] : [isa(_76690, c_tptpcol_16_26939), -(tptpcol_16_26939(_76690))], (108 ^ _73499) ^ [_76878] : [tptpcol_16_26939(_76878), -(isa(_76878, c_tptpcol_16_26939))], (114 ^ _73499) ^ [_77080, _77082] : [objectfoundinlocation(_77082, _77080), -(spatialthing_nonsituational(_77080))], (120 ^ _73499) ^ [_77288, _77290] : [objectfoundinlocation(_77290, _77288), -(spatialthing_localized(_77288))], (126 ^ _73499) ^ [_77496, _77498] : [objectfoundinlocation(_77498, _77496), -(spatialthing_nonsituational(_77498))], (132 ^ _73499) ^ [_77704, _77706] : [objectfoundinlocation(_77706, _77704), -(spatialthing_localized(_77706))], (138 ^ _73499) ^ [_77926, _77928, _77930] : [-(objectfoundinlocation(_77930, _77926)), objectfoundinlocation(_77930, _77928), objectfoundinlocation(_77928, _77926)], (148 ^ _73499) ^ [_78205] : [objectfoundinlocation(_78205, _78205)], (150 ^ _73499) ^ [_78326, _78328, _78330] : [-(objectfoundinlocation(_78330, _78326)), objectfoundinlocation(_78330, _78328), geopoliticalsubdivision(_78326, _78328)], (160 ^ _73499) ^ [_78649, _78651, _78653] : [-(objectfoundinlocation(_78653, _78649)), objectfoundinlocation(_78653, _78651), geographicallysubsumes(_78649, _78651)], (170 ^ _73499) ^ [_78972, _78974, _78976] : [-(objectfoundinlocation(_78976, _78972)), objectfoundinlocation(_78976, _78974), subregions(_78972, _78974)], (180 ^ _73499) ^ [_79267] : [isa(_79267, c_ship), -(ship(_79267))], (186 ^ _73499) ^ [_79455] : [ship(_79455), -(isa(_79455, c_ship))], (192 ^ _73499) ^ [_79656, _79658, _79660] : [-(natfunction(f_subcollectionofwithrelationtofn(_79660, _79658, _79656), c_subcollectionofwithrelationtofn))], (194 ^ _73499) ^ [_79770, _79772, _79774] : [-(natargument(f_subcollectionofwithrelationtofn(_79774, _79772, _79770), n_1, _79774))], (196 ^ _73499) ^ [_79885, _79887, _79889] : [-(natargument(f_subcollectionofwithrelationtofn(_79889, _79887, _79885), n_2, _79887))], (198 ^ _73499) ^ [_80000, _80002, _80004] : [-(natargument(f_subcollectionofwithrelationtofn(_80004, _80002, _80000), n_3, _80000))], (200 ^ _73499) ^ [_80115, _80117, _80119] : [-(collection(f_subcollectionofwithrelationtofn(_80119, _80117, _80115)))], (202 ^ _73499) ^ [_80215] : [isa(_80215, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)), -(subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(_80215))], (208 ^ _73499) ^ [_80403] : [subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(_80403), -(isa(_80403, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)))], (214 ^ _73499) ^ [_80605, _80607] : [tptptypes_9_693(_80607, _80605), -(firstordercollection(_80605))], (220 ^ _73499) ^ [_80813, _80815] : [tptptypes_9_693(_80815, _80813), -(firstordercollection(_80815))], (226 ^ _73499) ^ [_81021, _81023] : [genlpreds(_81023, _81021), -(predicate(_81021))], (232 ^ _73499) ^ [_81229, _81231] : [genlpreds(_81231, _81229), -(predicate(_81229))], (238 ^ _73499) ^ [_81437, _81439] : [genlpreds(_81439, _81437), -(predicate(_81439))], (244 ^ _73499) ^ [_81645, _81647] : [genlpreds(_81647, _81645), -(predicate(_81647))], (250 ^ _73499) ^ [_81867, _81869, _81871] : [-(genlpreds(_81871, _81867)), genlpreds(_81871, _81869), genlpreds(_81869, _81867)], (260 ^ _73499) ^ [_82162] : [predicate(_82162), -(genlpreds(_82162, _82162))], (266 ^ _73499) ^ [_82350] : [predicate(_82350), -(genlpreds(_82350, _82350))], (272 ^ _73499) ^ [_82552, _82554] : [tptptypes_7_691(_82554, _82552), -(firstordercollection(_82552))], (278 ^ _73499) ^ [_82760, _82762] : [tptptypes_7_691(_82762, _82760), -(firstordercollection(_82762))], (284 ^ _73499) ^ [_82968, _82970] : [tptptypes_8_692(_82970, _82968), -(firstordercollection(_82968))], (290 ^ _73499) ^ [_83176, _83178] : [tptptypes_8_692(_83178, _83176), -(firstordercollection(_83178))], (296 ^ _73499) ^ [_83384, _83386] : [genlinverse(_83386, _83384), -(binarypredicate(_83384))], (302 ^ _73499) ^ [_83592, _83594] : [genlinverse(_83594, _83592), -(binarypredicate(_83594))], (308 ^ _73499) ^ [_83814, _83816, _83818] : [-(genlinverse(_83814, _83816)), genlinverse(_83818, _83816), genlpreds(_83814, _83818)], (318 ^ _73499) ^ [_84137, _84139, _84141] : [-(genlinverse(_84141, _84137)), genlinverse(_84141, _84139), genlpreds(_84139, _84137)], (328 ^ _73499) ^ [_84432] : [isa(_84432, c_transitivebinarypredicate), -(transitivebinarypredicate(_84432))], (334 ^ _73499) ^ [_84620] : [transitivebinarypredicate(_84620), -(isa(_84620, c_transitivebinarypredicate))], (340 ^ _73499) ^ [_84822, _84824] : [isa(_84824, _84822), -(collection(_84822))], (346 ^ _73499) ^ [_85030, _85032] : [isa(_85032, _85030), -(collection(_85030))], (352 ^ _73499) ^ [_85238, _85240] : [isa(_85240, _85238), -(thing(_85240))], (358 ^ _73499) ^ [_85446, _85448] : [isa(_85448, _85446), -(thing(_85448))], (364 ^ _73499) ^ [_85668, _85670, _85672] : [-(isa(_85672, _85668)), isa(_85672, _85670), genls(_85670, _85668)], (374 ^ _73499) ^ [_85948] : [-(natfunction(f_urlfn(_85948), c_urlfn))], (376 ^ _73499) ^ [_86028] : [-(natargument(f_urlfn(_86028), n_1, _86028))], (378 ^ _73499) ^ [_86109] : [-(uniformresourcelocator(f_urlfn(_86109)))], (380 ^ _73499) ^ [_86188] : [-(natfunction(f_urlreferentfn(_86188), c_urlreferentfn))], (382 ^ _73499) ^ [_86268] : [-(natargument(f_urlreferentfn(_86268), n_1, _86268))], (384 ^ _73499) ^ [_86349] : [-(computerdataartifact(f_urlreferentfn(_86349)))], (386 ^ _73499) ^ [_86442, _86444] : [-(natfunction(f_contentmtofcdafromeventfn(_86444, _86442), c_contentmtofcdafromeventfn))], (388 ^ _73499) ^ [_86539, _86541] : [-(natargument(f_contentmtofcdafromeventfn(_86541, _86539), n_1, _86541))], (390 ^ _73499) ^ [_86637, _86639] : [-(natargument(f_contentmtofcdafromeventfn(_86639, _86637), n_2, _86637))], (392 ^ _73499) ^ [_86735, _86737] : [-(microtheory(f_contentmtofcdafromeventfn(_86737, _86735)))], (394 ^ _73499) ^ [] : [-(mtvisible(c_basekb))], (396 ^ _73499) ^ [_86899, _86901] : [-(mtvisible(_86899)), mtvisible(_86901), genlmt(_86901, _86899)], (406 ^ _73499) ^ [_87194, _87196] : [genlmt(_87196, _87194), -(microtheory(_87194))], (412 ^ _73499) ^ [_87402, _87404] : [genlmt(_87404, _87402), -(microtheory(_87402))], (418 ^ _73499) ^ [_87610, _87612] : [genlmt(_87612, _87610), -(microtheory(_87612))], (424 ^ _73499) ^ [_87818, _87820] : [genlmt(_87820, _87818), -(microtheory(_87820))], (430 ^ _73499) ^ [_88040, _88042, _88044] : [-(genlmt(_88044, _88040)), genlmt(_88044, _88042), genlmt(_88042, _88040)], (440 ^ _73499) ^ [_88335] : [microtheory(_88335), -(genlmt(_88335, _88335))], (452 ^ _73499) ^ [] : [-(mtvisible(c_universalvocabularymt))], (446 ^ _73499) ^ [_88523] : [microtheory(_88523), -(genlmt(_88523, _88523))]], input).
% 0.91/1.38 ncf('1',plain,[tptptypes_7_691(c_tptpcol_16_26939, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma))],start(456 ^ 0)).
% 0.91/1.38 ncf('1.1',plain,[-(tptptypes_7_691(c_tptpcol_16_26939, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma))), tptptypes_8_692(f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma), c_tptpcol_16_26939)],extension(24 ^ 1,bind([[_74195, _74197], [c_tptpcol_16_26939, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)]]))).
% 0.91/1.38 ncf('1.1.1',plain,[-(tptptypes_8_692(f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma), c_tptpcol_16_26939)), tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma), c_tptpcol_16_26939)],extension(32 ^ 2,bind([[_74458, _74460], [c_tptpcol_16_26939, f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma)]]))).
% 0.91/1.38 ncf('1.1.1.1',plain,[-(tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, c_cityofbostonma), c_tptpcol_16_26939)), mtvisible(c_currentworlddatacollectormt_nonhomocentric)],extension(38 ^ 3)).
% 0.91/1.38 ncf('1.1.1.1.1',plain,[-(mtvisible(c_currentworlddatacollectormt_nonhomocentric)), mtvisible(c_machinelearningspindleheadmt), genlmt(c_machinelearningspindleheadmt, c_currentworlddatacollectormt_nonhomocentric)],extension(396 ^ 4,bind([[_86899, _86901], [c_currentworlddatacollectormt_nonhomocentric, c_machinelearningspindleheadmt]]))).
% 0.91/1.38 ncf('1.1.1.1.1.1',plain,[-(mtvisible(c_machinelearningspindleheadmt)), mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32)), genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32), c_machinelearningspindleheadmt)],extension(396 ^ 5,bind([[_86899, _86901], [c_machinelearningspindleheadmt, f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32)]]))).
% 0.91/1.38 ncf('1.1.1.1.1.1.1',plain,[-(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32)))],extension(454 ^ 6)).
% 0.91/1.38 ncf('1.1.1.1.1.1.2',plain,[-(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)), c_translation_32), c_machinelearningspindleheadmt))],extension(8 ^ 6)).
% 0.91/1.38 ncf('1.1.1.1.1.2',plain,[-(genlmt(c_machinelearningspindleheadmt, c_currentworlddatacollectormt_nonhomocentric)), genlmt(c_machinelearningspindleheadmt, c_ldscgeneralcollectormt), genlmt(c_ldscgeneralcollectormt, c_currentworlddatacollectormt_nonhomocentric)],extension(430 ^ 5,bind([[_88040, _88042, _88044], [c_currentworlddatacollectormt_nonhomocentric, c_ldscgeneralcollectormt, c_machinelearningspindleheadmt]]))).
% 0.91/1.38 ncf('1.1.1.1.1.2.1',plain,[-(genlmt(c_machinelearningspindleheadmt, c_ldscgeneralcollectormt)), genlmt(c_machinelearningspindleheadmt, c_miptdatabase19681997_termsmt), genlmt(c_miptdatabase19681997_termsmt, c_ldscgeneralcollectormt)],extension(430 ^ 6,bind([[_88040, _88042, _88044], [c_ldscgeneralcollectormt, c_miptdatabase19681997_termsmt, c_machinelearningspindleheadmt]]))).
% 0.91/1.38 ncf('1.1.1.1.1.2.1.1',plain,[-(genlmt(c_machinelearningspindleheadmt, c_miptdatabase19681997_termsmt))],extension(10 ^ 7)).
% 0.91/1.38 ncf('1.1.1.1.1.2.1.2',plain,[-(genlmt(c_miptdatabase19681997_termsmt, c_ldscgeneralcollectormt))],extension(12 ^ 7)).
% 0.91/1.38 ncf('1.1.1.1.1.2.2',plain,[-(genlmt(c_ldscgeneralcollectormt, c_currentworlddatacollectormt_nonhomocentric)), genlmt(c_ldscgeneralcollectormt, c_ldscdemonstrationspindleheadmt), genlmt(c_ldscdemonstrationspindleheadmt, c_currentworlddatacollectormt_nonhomocentric)],extension(430 ^ 6,bind([[_88040, _88042, _88044], [c_currentworlddatacollectormt_nonhomocentric, c_ldscdemonstrationspindleheadmt, c_ldscgeneralcollectormt]]))).
% 0.91/1.38 ncf('1.1.1.1.1.2.2.1',plain,[-(genlmt(c_ldscgeneralcollectormt, c_ldscdemonstrationspindleheadmt))],extension(14 ^ 7)).
% 0.91/1.38 ncf('1.1.1.1.1.2.2.2',plain,[-(genlmt(c_ldscdemonstrationspindleheadmt, c_currentworlddatacollectormt_nonhomocentric))],extension(2 ^ 7)).
% 0.91/1.38 %-----------------------------------------------------
% 0.91/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------