%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR064+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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:55:36 EDT 2023
% Result : Theorem 0.38s 1.39s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR064+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n004.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 18 23:43:39 EDT 2023
% 0.14/0.34 % CPUTime :
% 0.38/1.39
% 0.38/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.38/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/1.39 %-----------------------------------------------------
% 0.38/1.39 ncf(matrix, plain, [(506 ^ _71803) ^ [] : [-(genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)), c_tptpcol_15_74743))], (2 ^ _71803) ^ [] : [-(disjointwith(c_individual, c_setorcollection))], (4 ^ _71803) ^ [_71955] : [individual(_71955), setorcollection(_71955)], (10 ^ _71803) ^ [] : [-(individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))], (12 ^ _71803) ^ [_72221, _72223, _72225] : [isa(_72225, _72223), isa(_72225, _72221), disjointwith(_72223, _72221)], (22 ^ _71803) ^ [_72543, _72545, _72547] : [-(genlpreds(_72547, _72543)), genlinverse(_72547, _72545), genlinverse(_72545, _72543)], (32 ^ _71803) ^ [] : [-(genlpreds(c_subsetof, c_most))], (34 ^ _71803) ^ [_72905, _72907] : [subsetof(_72907, _72905), -(most(_72907, _72905))], (40 ^ _71803) ^ [] : [-(transitivebinarypredicate(c_genlpreds))], (42 ^ _71803) ^ [] : [-(genlpreds(c_genls, c_subsetof))], (44 ^ _71803) ^ [_73221, _73223] : [genls(_73223, _73221), -(subsetof(_73223, _73221))], (50 ^ _71803) ^ [_73445, _73447, _73449] : [isa(_73449, _73447), isa(_73449, _73445), disjointwith(_73447, _73445)], (60 ^ _71803) ^ [_73767, _73769, _73771] : [-(genlpreds(_73771, _73767)), genlinverse(_73771, _73769), genlinverse(_73769, _73767)], (70 ^ _71803) ^ [] : [-(arg1isa(c_most, c_setorcollection))], (72 ^ _71803) ^ [_74129, _74131] : [most(_74131, _74129), -(setorcollection(_74131))], (78 ^ _71803) ^ [_74351, _74353, _74355] : [isa(_74355, _74353), isa(_74355, _74351), disjointwith(_74353, _74351)], (88 ^ _71803) ^ [_74673, _74675, _74677] : [-(genlpreds(_74677, _74673)), genlinverse(_74677, _74675), genlinverse(_74675, _74673)], (98 ^ _71803) ^ [_74982, _74984] : [arg1isa(_74984, _74982), -(collection(_74982))], (104 ^ _71803) ^ [_75190, _75192] : [arg1isa(_75192, _75190), -(relation(_75192))], (110 ^ _71803) ^ [_75412, _75414, _75416] : [-(arg1isa(_75416, _75412)), arg1isa(_75416, _75414), genls(_75414, _75412)], (120 ^ _71803) ^ [_75735, _75737, _75739] : [-(arg1isa(_75739, _75735)), arg1isa(_75739, _75737), genls(_75737, _75735)], (130 ^ _71803) ^ [_76044, _76046] : [genls(_76046, _76044), -(collection(_76044))], (136 ^ _71803) ^ [_76252, _76254] : [genls(_76254, _76252), -(collection(_76252))], (142 ^ _71803) ^ [_76460, _76462] : [genls(_76462, _76460), -(collection(_76462))], (148 ^ _71803) ^ [_76668, _76670] : [genls(_76670, _76668), -(collection(_76670))], (154 ^ _71803) ^ [_76890, _76892, _76894] : [-(genls(_76894, _76890)), genls(_76894, _76892), genls(_76892, _76890)], (164 ^ _71803) ^ [_77185] : [collection(_77185), -(genls(_77185, _77185))], (170 ^ _71803) ^ [_77373] : [collection(_77373), -(genls(_77373, _77373))], (176 ^ _71803) ^ [_77589, _77591, _77593] : [-(genls(_77589, _77591)), genls(_77593, _77591), genls(_77589, _77593)], (186 ^ _71803) ^ [_77912, _77914, _77916] : [-(genls(_77916, _77912)), genls(_77916, _77914), genls(_77914, _77912)], (196 ^ _71803) ^ [_78207] : [isa(_78207, c_transitivebinarypredicate), -(transitivebinarypredicate(_78207))], (202 ^ _71803) ^ [_78395] : [transitivebinarypredicate(_78395), -(isa(_78395, c_transitivebinarypredicate))], (208 ^ _71803) ^ [_78597, _78599] : [most(_78599, _78597), -(setorcollection(_78597))], (214 ^ _71803) ^ [_78805, _78807] : [most(_78807, _78805), -(setorcollection(_78805))], (220 ^ _71803) ^ [_79013, _79015] : [most(_79015, _79013), -(setorcollection(_79015))], (226 ^ _71803) ^ [_79221, _79223] : [most(_79223, _79221), -(setorcollection(_79223))], (232 ^ _71803) ^ [_79415] : [setorcollection(_79415), -(most(_79415, _79415))], (238 ^ _71803) ^ [_79603] : [setorcollection(_79603), -(most(_79603, _79603))], (244 ^ _71803) ^ [_79819, _79821, _79823] : [-(most(_79823, _79819)), most(_79823, _79821), subsetof(_79821, _79819)], (254 ^ _71803) ^ [_80142, _80144, _80146] : [-(most(_80146, _80142)), most(_80146, _80144), subsetof(_80144, _80142)], (264 ^ _71803) ^ [_80451, _80453] : [subsetof(_80453, _80451), -(setorcollection(_80451))], (270 ^ _71803) ^ [_80659, _80661] : [subsetof(_80661, _80659), -(setorcollection(_80661))], (276 ^ _71803) ^ [_80881, _80883, _80885] : [-(subsetof(_80885, _80881)), subsetof(_80885, _80883), subsetof(_80883, _80881)], (286 ^ _71803) ^ [_81176] : [setorcollection(_81176), -(subsetof(_81176, _81176))], (292 ^ _71803) ^ [_81392, _81394, _81396] : [-(subsetof(_81392, _81394)), subsetof(_81396, _81394), subsetof(_81392, _81396)], (302 ^ _71803) ^ [_81715, _81717, _81719] : [-(subsetof(_81719, _81715)), subsetof(_81719, _81717), subsetof(_81717, _81715)], (312 ^ _71803) ^ [_82038, _82040, _82042] : [-(subsetof(_82042, _82038)), subsetof(_82042, _82040), subsetof(_82040, _82038)], (322 ^ _71803) ^ [_82347, _82349] : [genlpreds(_82349, _82347), -(predicate(_82347))], (328 ^ _71803) ^ [_82555, _82557] : [genlpreds(_82557, _82555), -(predicate(_82555))], (334 ^ _71803) ^ [_82763, _82765] : [genlpreds(_82765, _82763), -(predicate(_82765))], (340 ^ _71803) ^ [_82971, _82973] : [genlpreds(_82973, _82971), -(predicate(_82973))], (346 ^ _71803) ^ [_83193, _83195, _83197] : [-(genlpreds(_83197, _83193)), genlpreds(_83197, _83195), genlpreds(_83195, _83193)], (356 ^ _71803) ^ [_83488] : [predicate(_83488), -(genlpreds(_83488, _83488))], (362 ^ _71803) ^ [_83676] : [predicate(_83676), -(genlpreds(_83676, _83676))], (368 ^ _71803) ^ [_83878, _83880] : [genlinverse(_83880, _83878), -(binarypredicate(_83878))], (374 ^ _71803) ^ [_84086, _84088] : [genlinverse(_84088, _84086), -(binarypredicate(_84088))], (380 ^ _71803) ^ [_84308, _84310, _84312] : [-(genlinverse(_84308, _84310)), genlinverse(_84312, _84310), genlpreds(_84308, _84312)], (390 ^ _71803) ^ [_84631, _84633, _84635] : [-(genlinverse(_84635, _84631)), genlinverse(_84635, _84633), genlpreds(_84633, _84631)], (400 ^ _71803) ^ [] : [-(mtvisible(c_basekb))], (402 ^ _71803) ^ [_84964] : [-(natfunction(f_urlfn(_84964), c_urlfn))], (404 ^ _71803) ^ [_85044] : [-(natargument(f_urlfn(_85044), n_1, _85044))], (406 ^ _71803) ^ [_85125] : [-(uniformresourcelocator(f_urlfn(_85125)))], (408 ^ _71803) ^ [_85233, _85235] : [isa(_85235, _85233), -(collection(_85233))], (414 ^ _71803) ^ [_85441, _85443] : [isa(_85443, _85441), -(collection(_85441))], (420 ^ _71803) ^ [_85649, _85651] : [isa(_85651, _85649), -(thing(_85651))], (426 ^ _71803) ^ [_85857, _85859] : [isa(_85859, _85857), -(thing(_85859))], (432 ^ _71803) ^ [_86079, _86081, _86083] : [-(isa(_86083, _86079)), isa(_86083, _86081), genls(_86081, _86079)], (442 ^ _71803) ^ [_86374] : [isa(_86374, c_setorcollection), -(setorcollection(_86374))], (448 ^ _71803) ^ [_86562] : [setorcollection(_86562), -(isa(_86562, c_setorcollection))], (454 ^ _71803) ^ [_86750] : [isa(_86750, c_individual), -(individual(_86750))], (460 ^ _71803) ^ [_86938] : [individual(_86938), -(isa(_86938, c_individual))], (466 ^ _71803) ^ [_87140, _87142] : [disjointwith(_87142, _87140), -(collection(_87140))], (472 ^ _71803) ^ [_87348, _87350] : [disjointwith(_87350, _87348), -(collection(_87350))], (478 ^ _71803) ^ [_87556, _87558] : [disjointwith(_87558, _87556), -(disjointwith(_87556, _87558))], (484 ^ _71803) ^ [_87780, _87782, _87784] : [-(disjointwith(_87784, _87780)), disjointwith(_87784, _87782), genls(_87780, _87782)], (504 ^ _71803) ^ [] : [-(mtvisible(c_universalvocabularymt))], (494 ^ _71803) ^ [_88103, _88105, _88107] : [-(disjointwith(_88103, _88105)), disjointwith(_88107, _88105), genls(_88103, _88107)]], input).
% 0.38/1.39 ncf('1',plain,[individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))), setorcollection(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))],start(4 ^ 0,bind([[_71955], [f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))]]))).
% 0.38/1.39 ncf('1.1',plain,[-(individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))))],extension(10 ^ 1)).
% 0.38/1.39 ncf('1.2',plain,[-(setorcollection(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))), subsetof(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)), c_tptpcol_15_74743)],extension(270 ^ 1,bind([[_80659, _80661], [c_tptpcol_15_74743, f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))]]))).
% 0.38/1.39 ncf('1.2.1',plain,[-(subsetof(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)), c_tptpcol_15_74743)), genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)), c_tptpcol_15_74743)],extension(44 ^ 2,bind([[_73221, _73223], [c_tptpcol_15_74743, f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))]]))).
% 0.38/1.39 ncf('1.2.1.1',plain,[-(genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)), c_tptpcol_15_74743))],extension(506 ^ 3)).
% 0.38/1.39 %-----------------------------------------------------
% 0.38/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------