%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR026+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:24:41 EDT 2023
% Result : Theorem 0.37s 1.38s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : CSR026+1 : TPTP v8.1.2. Released v3.4.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 23:16:30 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.37/1.38
% 0.37/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 ncf(matrix, plain, [(330 ^ _48866) ^ [] : [-(mtvisible(c_tptp_spindlecollectormt))], (332 ^ _48866) ^ [] : [tptpofobject(c_tptprunningshorts, f_tptpquantityfn_2(n_756))], (2 ^ _48866) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (4 ^ _48866) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (6 ^ _48866) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (8 ^ _48866) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (10 ^ _48866) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (12 ^ _48866) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member2701_mt))], (14 ^ _48866) ^ [] : [-(genlmt(c_tptp_member3993_mt, c_tptp_spindleheadmt))], (16 ^ _48866) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member3993_mt))], (18 ^ _48866) ^ [_49389] : [-(tptpofobject(_49389, f_tptpquantityfn_2(n_756))), mtvisible(c_tptp_member2701_mt), runningshorts(_49389)], (28 ^ _48866) ^ [] : [mtvisible(c_tptp_member2701_mt), -(relationallinstance(c_tptpofobject, c_runningshorts, f_tptpquantityfn_2(n_756)))], (34 ^ _48866) ^ [] : [mtvisible(c_cyclistsmt), -(runningshorts(c_tptprunningshorts))], (40 ^ _48866) ^ [_49922, _49924, _49926] : [isa(_49926, _49924), isa(_49926, _49922), disjointwith(_49924, _49922)], (50 ^ _48866) ^ [_50244, _50246, _50248] : [-(genlpreds(_50248, _50244)), genlinverse(_50248, _50246), genlinverse(_50246, _50244)], (60 ^ _48866) ^ [_50553, _50555] : [genlpreds(_50555, _50553), -(predicate(_50553))], (66 ^ _48866) ^ [_50761, _50763] : [genlpreds(_50763, _50761), -(predicate(_50761))], (72 ^ _48866) ^ [_50969, _50971] : [genlpreds(_50971, _50969), -(predicate(_50971))], (78 ^ _48866) ^ [_51177, _51179] : [genlpreds(_51179, _51177), -(predicate(_51179))], (84 ^ _48866) ^ [_51399, _51401, _51403] : [-(genlpreds(_51403, _51399)), genlpreds(_51403, _51401), genlpreds(_51401, _51399)], (94 ^ _48866) ^ [_51694] : [predicate(_51694), -(genlpreds(_51694, _51694))], (100 ^ _48866) ^ [_51882] : [predicate(_51882), -(genlpreds(_51882, _51882))], (106 ^ _48866) ^ [_52084, _52086] : [genlinverse(_52086, _52084), -(binarypredicate(_52084))], (112 ^ _48866) ^ [_52292, _52294] : [genlinverse(_52294, _52292), -(binarypredicate(_52294))], (118 ^ _48866) ^ [_52514, _52516, _52518] : [-(genlinverse(_52514, _52516)), genlinverse(_52518, _52516), genlpreds(_52514, _52518)], (128 ^ _48866) ^ [_52837, _52839, _52841] : [-(genlinverse(_52841, _52837)), genlinverse(_52841, _52839), genlpreds(_52839, _52837)], (138 ^ _48866) ^ [_53146, _53148] : [disjointwith(_53148, _53146), -(collection(_53146))], (144 ^ _48866) ^ [_53354, _53356] : [disjointwith(_53356, _53354), -(collection(_53356))], (150 ^ _48866) ^ [_53562, _53564] : [disjointwith(_53564, _53562), -(disjointwith(_53562, _53564))], (156 ^ _48866) ^ [_53786, _53788, _53790] : [-(disjointwith(_53790, _53786)), disjointwith(_53790, _53788), genls(_53786, _53788)], (166 ^ _48866) ^ [_54109, _54111, _54113] : [-(disjointwith(_54109, _54111)), disjointwith(_54113, _54111), genls(_54109, _54113)], (176 ^ _48866) ^ [_54389] : [-(natfunction(f_tptpquantityfn_2(_54389), c_tptpquantityfn_2))], (178 ^ _48866) ^ [_54469] : [-(natargument(f_tptpquantityfn_2(_54469), n_1, _54469))], (180 ^ _48866) ^ [_54550] : [-(tptpquantity(f_tptpquantityfn_2(_54550)))], (182 ^ _48866) ^ [_54644] : [isa(_54644, c_runningshorts), -(runningshorts(_54644))], (188 ^ _48866) ^ [_54832] : [runningshorts(_54832), -(isa(_54832, c_runningshorts))], (194 ^ _48866) ^ [_55034, _55036] : [tptpofobject(_55036, _55034), -(tptpquantity(_55034))], (200 ^ _48866) ^ [_55242, _55244] : [tptpofobject(_55244, _55242), -(partiallytangible(_55244))], (206 ^ _48866) ^ [_55464, _55466, _55468] : [relationallinstance(_55468, _55466, _55464), -(thing(_55464))], (212 ^ _48866) ^ [_55694, _55696, _55698] : [relationallinstance(_55698, _55696, _55694), -(collection(_55696))], (218 ^ _48866) ^ [_55924, _55926, _55928] : [relationallinstance(_55928, _55926, _55924), -(binarypredicate(_55928))], (224 ^ _48866) ^ [] : [-(mtvisible(c_basekb))], (226 ^ _48866) ^ [_56179] : [isa(_56179, c_transitivebinarypredicate), -(transitivebinarypredicate(_56179))], (232 ^ _48866) ^ [_56367] : [transitivebinarypredicate(_56367), -(isa(_56367, c_transitivebinarypredicate))], (238 ^ _48866) ^ [_56569, _56571] : [isa(_56571, _56569), -(collection(_56569))], (244 ^ _48866) ^ [_56777, _56779] : [isa(_56779, _56777), -(collection(_56777))], (250 ^ _48866) ^ [_56985, _56987] : [isa(_56987, _56985), -(thing(_56987))], (256 ^ _48866) ^ [_57193, _57195] : [isa(_57195, _57193), -(thing(_57195))], (262 ^ _48866) ^ [_57415, _57417, _57419] : [-(isa(_57419, _57415)), isa(_57419, _57417), genls(_57417, _57415)], (272 ^ _48866) ^ [_57724, _57726] : [-(mtvisible(_57724)), mtvisible(_57726), genlmt(_57726, _57724)], (282 ^ _48866) ^ [_58019, _58021] : [genlmt(_58021, _58019), -(microtheory(_58019))], (288 ^ _48866) ^ [_58227, _58229] : [genlmt(_58229, _58227), -(microtheory(_58227))], (294 ^ _48866) ^ [_58435, _58437] : [genlmt(_58437, _58435), -(microtheory(_58437))], (300 ^ _48866) ^ [_58643, _58645] : [genlmt(_58645, _58643), -(microtheory(_58645))], (306 ^ _48866) ^ [_58865, _58867, _58869] : [-(genlmt(_58869, _58865)), genlmt(_58869, _58867), genlmt(_58867, _58865)], (316 ^ _48866) ^ [_59160] : [microtheory(_59160), -(genlmt(_59160, _59160))], (328 ^ _48866) ^ [] : [-(mtvisible(c_universalvocabularymt))], (322 ^ _48866) ^ [_59348] : [microtheory(_59348), -(genlmt(_59348, _59348))]], input).
% 0.37/1.38 ncf('1',plain,[tptpofobject(c_tptprunningshorts, f_tptpquantityfn_2(n_756))],start(332 ^ 0)).
% 0.37/1.38 ncf('1.1',plain,[-(tptpofobject(c_tptprunningshorts, f_tptpquantityfn_2(n_756))), mtvisible(c_tptp_member2701_mt), runningshorts(c_tptprunningshorts)],extension(18 ^ 1,bind([[_49389], [c_tptprunningshorts]]))).
% 0.37/1.38 ncf('1.1.1',plain,[-(mtvisible(c_tptp_member2701_mt)), mtvisible(c_tptp_spindlecollectormt), genlmt(c_tptp_spindlecollectormt, c_tptp_member2701_mt)],extension(272 ^ 2,bind([[_57724, _57726], [c_tptp_member2701_mt, c_tptp_spindlecollectormt]]))).
% 0.37/1.38 ncf('1.1.1.1',plain,[-(mtvisible(c_tptp_spindlecollectormt))],extension(330 ^ 3)).
% 0.37/1.38 ncf('1.1.1.2',plain,[-(genlmt(c_tptp_spindlecollectormt, c_tptp_member2701_mt))],extension(12 ^ 3)).
% 0.37/1.38 ncf('1.1.2',plain,[-(runningshorts(c_tptprunningshorts)), mtvisible(c_cyclistsmt)],extension(34 ^ 2)).
% 0.37/1.38 ncf('1.1.2.1',plain,[-(mtvisible(c_cyclistsmt)), mtvisible(c_tptp_member3993_mt), genlmt(c_tptp_member3993_mt, c_cyclistsmt)],extension(272 ^ 3,bind([[_57724, _57726], [c_cyclistsmt, c_tptp_member3993_mt]]))).
% 0.37/1.38 ncf('1.1.2.1.1',plain,[-(mtvisible(c_tptp_member3993_mt)), mtvisible(c_tptp_spindlecollectormt), genlmt(c_tptp_spindlecollectormt, c_tptp_member3993_mt)],extension(272 ^ 4,bind([[_57724, _57726], [c_tptp_member3993_mt, c_tptp_spindlecollectormt]]))).
% 0.37/1.38 ncf('1.1.2.1.1.1',plain,[-(mtvisible(c_tptp_spindlecollectormt))],extension(330 ^ 5)).
% 0.37/1.38 ncf('1.1.2.1.1.2',plain,[-(genlmt(c_tptp_spindlecollectormt, c_tptp_member3993_mt))],extension(16 ^ 5)).
% 0.37/1.38 ncf('1.1.2.1.2',plain,[-(genlmt(c_tptp_member3993_mt, c_cyclistsmt)), genlmt(c_tptp_member3993_mt, c_tptp_spindleheadmt), genlmt(c_tptp_spindleheadmt, c_cyclistsmt)],extension(306 ^ 4,bind([[_58865, _58867, _58869], [c_cyclistsmt, c_tptp_spindleheadmt, c_tptp_member3993_mt]]))).
% 0.37/1.38 ncf('1.1.2.1.2.1',plain,[-(genlmt(c_tptp_member3993_mt, c_tptp_spindleheadmt))],extension(14 ^ 5)).
% 0.37/1.38 ncf('1.1.2.1.2.2',plain,[-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))],extension(10 ^ 5)).
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------