%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR062+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:53:58 EDT 2023
% Result : Theorem 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR062+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n001.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 : Fri May 19 00:15:50 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(360 ^ _51913) ^ [_63921] : [-(mtvisible(c_tptp_member3205_mt))], (362 ^ _51913) ^ [_63958] : [tptptypes_5_387(_63958, c_pushingwithfingers)], (2 ^ _51913) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (4 ^ _51913) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (6 ^ _51913) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (8 ^ _51913) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (10 ^ _51913) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (12 ^ _51913) ^ [] : [-(genlpreds(c_tptptypes_6_388, c_tptptypes_5_387))], (14 ^ _51913) ^ [_52344, _52346] : [tptptypes_6_388(_52346, _52344), -(tptptypes_5_387(_52346, _52344))], (20 ^ _51913) ^ [] : [-(genlinverse(c_tptptypes_7_389, c_tptptypes_6_388))], (22 ^ _51913) ^ [_52607, _52609] : [tptptypes_7_389(_52609, _52607), -(tptptypes_6_388(_52607, _52609))], (28 ^ _51913) ^ [] : [-(genlpreds(c_tptptypes_8_390, c_tptptypes_7_389))], (30 ^ _51913) ^ [_52870, _52872] : [tptptypes_8_390(_52872, _52870), -(tptptypes_7_389(_52872, _52870))], (36 ^ _51913) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (38 ^ _51913) ^ [] : [-(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))], (40 ^ _51913) ^ [] : [mtvisible(c_cyclistsmt), -(tptptypes_8_390(c_pushingwithfingers, c_tptpcol_15_4027))], (46 ^ _51913) ^ [_53319, _53321, _53323] : [isa(_53323, _53321), isa(_53323, _53319), disjointwith(_53321, _53319)], (56 ^ _51913) ^ [_53641, _53643, _53645] : [-(genlpreds(_53645, _53641)), genlinverse(_53645, _53643), genlinverse(_53643, _53641)], (66 ^ _51913) ^ [_53950, _53952] : [disjointwith(_53952, _53950), -(collection(_53950))], (72 ^ _51913) ^ [_54158, _54160] : [disjointwith(_54160, _54158), -(collection(_54160))], (78 ^ _51913) ^ [_54366, _54368] : [disjointwith(_54368, _54366), -(disjointwith(_54366, _54368))], (84 ^ _51913) ^ [_54590, _54592, _54594] : [-(disjointwith(_54594, _54590)), disjointwith(_54594, _54592), genls(_54590, _54592)], (94 ^ _51913) ^ [_54913, _54915, _54917] : [-(disjointwith(_54913, _54915)), disjointwith(_54917, _54915), genls(_54913, _54917)], (104 ^ _51913) ^ [_55208] : [isa(_55208, c_tptpcol_15_4027), -(tptpcol_15_4027(_55208))], (110 ^ _51913) ^ [_55396] : [tptpcol_15_4027(_55396), -(isa(_55396, c_tptpcol_15_4027))], (116 ^ _51913) ^ [_55584] : [isa(_55584, c_pushingwithfingers), -(pushingwithfingers(_55584))], (122 ^ _51913) ^ [_55772] : [pushingwithfingers(_55772), -(isa(_55772, c_pushingwithfingers))], (128 ^ _51913) ^ [_55974, _55976] : [tptptypes_8_390(_55976, _55974), -(firstordercollection(_55974))], (134 ^ _51913) ^ [_56182, _56184] : [tptptypes_8_390(_56184, _56182), -(firstordercollection(_56184))], (140 ^ _51913) ^ [_56390, _56392] : [tptptypes_7_389(_56392, _56390), -(firstordercollection(_56390))], (146 ^ _51913) ^ [_56598, _56600] : [tptptypes_7_389(_56600, _56598), -(firstordercollection(_56600))], (152 ^ _51913) ^ [_56806, _56808] : [genlinverse(_56808, _56806), -(binarypredicate(_56806))], (158 ^ _51913) ^ [_57014, _57016] : [genlinverse(_57016, _57014), -(binarypredicate(_57016))], (164 ^ _51913) ^ [_57236, _57238, _57240] : [-(genlinverse(_57236, _57238)), genlinverse(_57240, _57238), genlpreds(_57236, _57240)], (174 ^ _51913) ^ [_57559, _57561, _57563] : [-(genlinverse(_57563, _57559)), genlinverse(_57563, _57561), genlpreds(_57561, _57559)], (184 ^ _51913) ^ [_57868, _57870] : [tptptypes_5_387(_57870, _57868), -(firstordercollection(_57868))], (190 ^ _51913) ^ [_58076, _58078] : [tptptypes_5_387(_58078, _58076), -(firstordercollection(_58078))], (196 ^ _51913) ^ [_58284, _58286] : [tptptypes_6_388(_58286, _58284), -(firstordercollection(_58284))], (202 ^ _51913) ^ [_58492, _58494] : [tptptypes_6_388(_58494, _58492), -(firstordercollection(_58494))], (208 ^ _51913) ^ [_58700, _58702] : [genlpreds(_58702, _58700), -(predicate(_58700))], (214 ^ _51913) ^ [_58908, _58910] : [genlpreds(_58910, _58908), -(predicate(_58908))], (220 ^ _51913) ^ [_59116, _59118] : [genlpreds(_59118, _59116), -(predicate(_59118))], (226 ^ _51913) ^ [_59324, _59326] : [genlpreds(_59326, _59324), -(predicate(_59326))], (232 ^ _51913) ^ [_59546, _59548, _59550] : [-(genlpreds(_59550, _59546)), genlpreds(_59550, _59548), genlpreds(_59548, _59546)], (242 ^ _51913) ^ [_59841] : [predicate(_59841), -(genlpreds(_59841, _59841))], (248 ^ _51913) ^ [_60029] : [predicate(_60029), -(genlpreds(_60029, _60029))], (254 ^ _51913) ^ [] : [-(mtvisible(c_basekb))], (256 ^ _51913) ^ [_60270] : [isa(_60270, c_transitivebinarypredicate), -(transitivebinarypredicate(_60270))], (262 ^ _51913) ^ [_60458] : [transitivebinarypredicate(_60458), -(isa(_60458, c_transitivebinarypredicate))], (268 ^ _51913) ^ [_60660, _60662] : [isa(_60662, _60660), -(collection(_60660))], (274 ^ _51913) ^ [_60868, _60870] : [isa(_60870, _60868), -(collection(_60868))], (280 ^ _51913) ^ [_61076, _61078] : [isa(_61078, _61076), -(thing(_61078))], (286 ^ _51913) ^ [_61284, _61286] : [isa(_61286, _61284), -(thing(_61286))], (292 ^ _51913) ^ [_61506, _61508, _61510] : [-(isa(_61510, _61506)), isa(_61510, _61508), genls(_61508, _61506)], (302 ^ _51913) ^ [_61815, _61817] : [-(mtvisible(_61815)), mtvisible(_61817), genlmt(_61817, _61815)], (312 ^ _51913) ^ [_62110, _62112] : [genlmt(_62112, _62110), -(microtheory(_62110))], (318 ^ _51913) ^ [_62318, _62320] : [genlmt(_62320, _62318), -(microtheory(_62318))], (324 ^ _51913) ^ [_62526, _62528] : [genlmt(_62528, _62526), -(microtheory(_62528))], (330 ^ _51913) ^ [_62734, _62736] : [genlmt(_62736, _62734), -(microtheory(_62736))], (336 ^ _51913) ^ [_62956, _62958, _62960] : [-(genlmt(_62960, _62956)), genlmt(_62960, _62958), genlmt(_62958, _62956)], (346 ^ _51913) ^ [_63251] : [microtheory(_63251), -(genlmt(_63251, _63251))], (358 ^ _51913) ^ [] : [-(mtvisible(c_universalvocabularymt))], (352 ^ _51913) ^ [_63439] : [microtheory(_63439), -(genlmt(_63439, _63439))]], input).
% 0.35/1.37 ncf('1',plain,[tptptypes_5_387(c_tptpcol_15_4027, c_pushingwithfingers)],start(362 ^ 0,bind([[_63958], [c_tptpcol_15_4027]]))).
% 0.35/1.37 ncf('1.1',plain,[-(tptptypes_5_387(c_tptpcol_15_4027, c_pushingwithfingers)), tptptypes_6_388(c_tptpcol_15_4027, c_pushingwithfingers)],extension(14 ^ 1,bind([[_52344, _52346], [c_pushingwithfingers, c_tptpcol_15_4027]]))).
% 0.35/1.37 ncf('1.1.1',plain,[-(tptptypes_6_388(c_tptpcol_15_4027, c_pushingwithfingers)), tptptypes_7_389(c_pushingwithfingers, c_tptpcol_15_4027)],extension(22 ^ 2,bind([[_52607, _52609], [c_tptpcol_15_4027, c_pushingwithfingers]]))).
% 0.35/1.37 ncf('1.1.1.1',plain,[-(tptptypes_7_389(c_pushingwithfingers, c_tptpcol_15_4027)), tptptypes_8_390(c_pushingwithfingers, c_tptpcol_15_4027)],extension(30 ^ 3,bind([[_52870, _52872], [c_tptpcol_15_4027, c_pushingwithfingers]]))).
% 0.35/1.37 ncf('1.1.1.1.1',plain,[-(tptptypes_8_390(c_pushingwithfingers, c_tptpcol_15_4027)), mtvisible(c_cyclistsmt)],extension(40 ^ 4)).
% 0.35/1.37 ncf('1.1.1.1.1.1',plain,[-(mtvisible(c_cyclistsmt)), mtvisible(c_tptp_member3205_mt), genlmt(c_tptp_member3205_mt, c_cyclistsmt)],extension(302 ^ 5,bind([[_61815, _61817], [c_cyclistsmt, c_tptp_member3205_mt]]))).
% 0.35/1.37 ncf('1.1.1.1.1.1.1',plain,[-(mtvisible(c_tptp_member3205_mt))],extension(360 ^ 6,bind([[_63921], [_37950]]))).
% 0.35/1.37 ncf('1.1.1.1.1.1.2',plain,[-(genlmt(c_tptp_member3205_mt, c_cyclistsmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), genlmt(c_tptp_spindleheadmt, c_cyclistsmt)],extension(336 ^ 6,bind([[_62956, _62958, _62960], [c_cyclistsmt, c_tptp_spindleheadmt, c_tptp_member3205_mt]]))).
% 0.35/1.37 ncf('1.1.1.1.1.1.2.1',plain,[-(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))],extension(38 ^ 7)).
% 0.35/1.37 ncf('1.1.1.1.1.1.2.2',plain,[-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))],extension(36 ^ 7)).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------