%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR068+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:58:47 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.08/0.13 % Problem : CSR068+1 : TPTP v8.1.2. Released v3.4.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n004.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 : Fri May 19 00:33:39 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.34/1.41
% 0.34/1.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41 ncf(matrix, plain, [(324 ^ _47111) ^ [] : [-(mtvisible(c_tptp_member2356_mt))], (326 ^ _47111) ^ [] : [tptpofobject(c_theprototypicalfurpelt, f_tptpquantityfn_1(n_328))], (2 ^ _47111) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (4 ^ _47111) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (6 ^ _47111) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (8 ^ _47111) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (10 ^ _47111) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (12 ^ _47111) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (14 ^ _47111) ^ [] : [-(genlmt(c_tptp_member2356_mt, c_tptp_spindleheadmt))], (16 ^ _47111) ^ [] : [-(furpelt(c_theprototypicalfurpelt))], (18 ^ _47111) ^ [_47634] : [-(tptpofobject(_47634, f_tptpquantityfn_1(n_328))), mtvisible(c_tptp_spindleheadmt), furpelt(_47634)], (28 ^ _47111) ^ [] : [mtvisible(c_tptp_spindleheadmt), -(relationallinstance(c_tptpofobject, c_furpelt, f_tptpquantityfn_1(n_328)))], (34 ^ _47111) ^ [_48048, _48050, _48052] : [isa(_48052, _48050), isa(_48052, _48048), disjointwith(_48050, _48048)], (44 ^ _47111) ^ [_48370, _48372, _48374] : [-(genlpreds(_48374, _48370)), genlinverse(_48374, _48372), genlinverse(_48372, _48370)], (54 ^ _47111) ^ [_48679, _48681] : [genlpreds(_48681, _48679), -(predicate(_48679))], (60 ^ _47111) ^ [_48887, _48889] : [genlpreds(_48889, _48887), -(predicate(_48887))], (66 ^ _47111) ^ [_49095, _49097] : [genlpreds(_49097, _49095), -(predicate(_49097))], (72 ^ _47111) ^ [_49303, _49305] : [genlpreds(_49305, _49303), -(predicate(_49305))], (78 ^ _47111) ^ [_49525, _49527, _49529] : [-(genlpreds(_49529, _49525)), genlpreds(_49529, _49527), genlpreds(_49527, _49525)], (88 ^ _47111) ^ [_49820] : [predicate(_49820), -(genlpreds(_49820, _49820))], (94 ^ _47111) ^ [_50008] : [predicate(_50008), -(genlpreds(_50008, _50008))], (100 ^ _47111) ^ [_50210, _50212] : [genlinverse(_50212, _50210), -(binarypredicate(_50210))], (106 ^ _47111) ^ [_50418, _50420] : [genlinverse(_50420, _50418), -(binarypredicate(_50420))], (112 ^ _47111) ^ [_50640, _50642, _50644] : [-(genlinverse(_50640, _50642)), genlinverse(_50644, _50642), genlpreds(_50640, _50644)], (122 ^ _47111) ^ [_50963, _50965, _50967] : [-(genlinverse(_50967, _50963)), genlinverse(_50967, _50965), genlpreds(_50965, _50963)], (132 ^ _47111) ^ [_51272, _51274] : [disjointwith(_51274, _51272), -(collection(_51272))], (138 ^ _47111) ^ [_51480, _51482] : [disjointwith(_51482, _51480), -(collection(_51482))], (144 ^ _47111) ^ [_51688, _51690] : [disjointwith(_51690, _51688), -(disjointwith(_51688, _51690))], (150 ^ _47111) ^ [_51912, _51914, _51916] : [-(disjointwith(_51916, _51912)), disjointwith(_51916, _51914), genls(_51912, _51914)], (160 ^ _47111) ^ [_52235, _52237, _52239] : [-(disjointwith(_52235, _52237)), disjointwith(_52239, _52237), genls(_52235, _52239)], (170 ^ _47111) ^ [_52515] : [-(natfunction(f_tptpquantityfn_1(_52515), c_tptpquantityfn_1))], (172 ^ _47111) ^ [_52595] : [-(natargument(f_tptpquantityfn_1(_52595), n_1, _52595))], (174 ^ _47111) ^ [_52676] : [-(tptpquantity(f_tptpquantityfn_1(_52676)))], (176 ^ _47111) ^ [_52784, _52786] : [tptpofobject(_52786, _52784), -(tptpquantity(_52784))], (182 ^ _47111) ^ [_52992, _52994] : [tptpofobject(_52994, _52992), -(partiallytangible(_52994))], (188 ^ _47111) ^ [_53214, _53216, _53218] : [relationallinstance(_53218, _53216, _53214), -(thing(_53214))], (194 ^ _47111) ^ [_53444, _53446, _53448] : [relationallinstance(_53448, _53446, _53444), -(collection(_53446))], (200 ^ _47111) ^ [_53674, _53676, _53678] : [relationallinstance(_53678, _53676, _53674), -(binarypredicate(_53678))], (206 ^ _47111) ^ [_53876] : [isa(_53876, c_furpelt), -(furpelt(_53876))], (212 ^ _47111) ^ [_54064] : [furpelt(_54064), -(isa(_54064, c_furpelt))], (218 ^ _47111) ^ [] : [-(mtvisible(c_basekb))], (220 ^ _47111) ^ [_54305] : [isa(_54305, c_transitivebinarypredicate), -(transitivebinarypredicate(_54305))], (226 ^ _47111) ^ [_54493] : [transitivebinarypredicate(_54493), -(isa(_54493, c_transitivebinarypredicate))], (232 ^ _47111) ^ [_54695, _54697] : [isa(_54697, _54695), -(collection(_54695))], (238 ^ _47111) ^ [_54903, _54905] : [isa(_54905, _54903), -(collection(_54903))], (244 ^ _47111) ^ [_55111, _55113] : [isa(_55113, _55111), -(thing(_55113))], (250 ^ _47111) ^ [_55319, _55321] : [isa(_55321, _55319), -(thing(_55321))], (256 ^ _47111) ^ [_55541, _55543, _55545] : [-(isa(_55545, _55541)), isa(_55545, _55543), genls(_55543, _55541)], (266 ^ _47111) ^ [_55850, _55852] : [-(mtvisible(_55850)), mtvisible(_55852), genlmt(_55852, _55850)], (276 ^ _47111) ^ [_56145, _56147] : [genlmt(_56147, _56145), -(microtheory(_56145))], (282 ^ _47111) ^ [_56353, _56355] : [genlmt(_56355, _56353), -(microtheory(_56353))], (288 ^ _47111) ^ [_56561, _56563] : [genlmt(_56563, _56561), -(microtheory(_56563))], (294 ^ _47111) ^ [_56769, _56771] : [genlmt(_56771, _56769), -(microtheory(_56771))], (300 ^ _47111) ^ [_56991, _56993, _56995] : [-(genlmt(_56995, _56991)), genlmt(_56995, _56993), genlmt(_56993, _56991)], (310 ^ _47111) ^ [_57286] : [microtheory(_57286), -(genlmt(_57286, _57286))], (322 ^ _47111) ^ [] : [-(mtvisible(c_universalvocabularymt))], (316 ^ _47111) ^ [_57474] : [microtheory(_57474), -(genlmt(_57474, _57474))]], input).
% 0.34/1.41 ncf('1',plain,[tptpofobject(c_theprototypicalfurpelt, f_tptpquantityfn_1(n_328))],start(326 ^ 0)).
% 0.34/1.41 ncf('1.1',plain,[-(tptpofobject(c_theprototypicalfurpelt, f_tptpquantityfn_1(n_328))), mtvisible(c_tptp_spindleheadmt), furpelt(c_theprototypicalfurpelt)],extension(18 ^ 1,bind([[_47634], [c_theprototypicalfurpelt]]))).
% 0.34/1.41 ncf('1.1.1',plain,[-(mtvisible(c_tptp_spindleheadmt)), mtvisible(c_tptp_member2356_mt), genlmt(c_tptp_member2356_mt, c_tptp_spindleheadmt)],extension(266 ^ 2,bind([[_55850, _55852], [c_tptp_spindleheadmt, c_tptp_member2356_mt]]))).
% 0.34/1.41 ncf('1.1.1.1',plain,[-(mtvisible(c_tptp_member2356_mt))],extension(324 ^ 3)).
% 0.34/1.41 ncf('1.1.1.2',plain,[-(genlmt(c_tptp_member2356_mt, c_tptp_spindleheadmt))],extension(14 ^ 3)).
% 0.34/1.41 ncf('1.1.2',plain,[-(furpelt(c_theprototypicalfurpelt))],extension(16 ^ 2)).
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------