%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR031+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:28:41 EDT 2023
% Result : Theorem 0.35s 1.41s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : CSR031+1 : TPTP v8.1.2. Released v3.4.0.
% 0.13/0.14 % Command : nanocop.sh %s %d
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri May 19 00:19:12 EDT 2023
% 0.14/0.36 % CPUTime :
% 0.35/1.41
% 0.35/1.41 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.41 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.41 %-----------------------------------------------------
% 0.35/1.41 ncf(matrix, plain, [(348 ^ _48768) ^ [] : [-(disjointwith(c_tptptptpcol_16_8398, c_tptpcol_16_18488))], (2 ^ _48768) ^ [] : [-(genlmt(c_universalvocabularymt, c_corecyclmt))], (4 ^ _48768) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (6 ^ _48768) ^ [] : [-(genlmt(c_corecyclmt, c_logicaltruthmt))], (8 ^ _48768) ^ [_49026] : [collection(_49026), individual(_49026)], (14 ^ _48768) ^ [] : [-(disjointwith(c_collection, c_individual))], (16 ^ _48768) ^ [] : [-(individual(c_tptptptpcol_16_8398))], (18 ^ _48768) ^ [_49345, _49347, _49349] : [isa(_49349, _49347), isa(_49349, _49345), disjointwith(_49347, _49345)], (28 ^ _48768) ^ [_49667, _49669, _49671] : [-(genlpreds(_49671, _49667)), genlinverse(_49671, _49669), genlinverse(_49669, _49667)], (38 ^ _48768) ^ [] : [-(arg2isa(c_disjointwith, c_collection))], (40 ^ _48768) ^ [_50029, _50031] : [disjointwith(_50031, _50029), -(collection(_50029))], (46 ^ _48768) ^ [_50251, _50253, _50255] : [isa(_50255, _50253), isa(_50255, _50251), disjointwith(_50253, _50251)], (56 ^ _48768) ^ [_50573, _50575, _50577] : [-(genlpreds(_50577, _50573)), genlinverse(_50577, _50575), genlinverse(_50575, _50573)], (66 ^ _48768) ^ [_50882, _50884] : [arg2isa(_50884, _50882), -(collection(_50882))], (72 ^ _48768) ^ [_51090, _51092] : [arg2isa(_51092, _51090), -(relation(_51092))], (78 ^ _48768) ^ [_51312, _51314, _51316] : [-(arg2isa(_51316, _51312)), arg2isa(_51316, _51314), genls(_51314, _51312)], (88 ^ _48768) ^ [_51635, _51637, _51639] : [-(arg2isa(_51639, _51635)), arg2isa(_51639, _51637), genls(_51637, _51635)], (98 ^ _48768) ^ [_51944, _51946] : [genlpreds(_51946, _51944), -(predicate(_51944))], (104 ^ _48768) ^ [_52152, _52154] : [genlpreds(_52154, _52152), -(predicate(_52152))], (110 ^ _48768) ^ [_52360, _52362] : [genlpreds(_52362, _52360), -(predicate(_52362))], (116 ^ _48768) ^ [_52568, _52570] : [genlpreds(_52570, _52568), -(predicate(_52570))], (122 ^ _48768) ^ [_52790, _52792, _52794] : [-(genlpreds(_52794, _52790)), genlpreds(_52794, _52792), genlpreds(_52792, _52790)], (132 ^ _48768) ^ [_53085] : [predicate(_53085), -(genlpreds(_53085, _53085))], (138 ^ _48768) ^ [_53273] : [predicate(_53273), -(genlpreds(_53273, _53273))], (144 ^ _48768) ^ [_53475, _53477] : [genlinverse(_53477, _53475), -(binarypredicate(_53475))], (150 ^ _48768) ^ [_53683, _53685] : [genlinverse(_53685, _53683), -(binarypredicate(_53685))], (156 ^ _48768) ^ [_53905, _53907, _53909] : [-(genlinverse(_53905, _53907)), genlinverse(_53909, _53907), genlpreds(_53905, _53909)], (166 ^ _48768) ^ [_54228, _54230, _54232] : [-(genlinverse(_54232, _54228)), genlinverse(_54232, _54230), genlpreds(_54230, _54228)], (176 ^ _48768) ^ [] : [-(mtvisible(c_basekb))], (178 ^ _48768) ^ [_54576] : [isa(_54576, c_individual), -(individual(_54576))], (184 ^ _48768) ^ [_54764] : [individual(_54764), -(isa(_54764, c_individual))], (190 ^ _48768) ^ [_54952] : [isa(_54952, c_collection), -(collection(_54952))], (196 ^ _48768) ^ [_55140] : [collection(_55140), -(isa(_55140, c_collection))], (202 ^ _48768) ^ [_55342, _55344] : [disjointwith(_55344, _55342), -(collection(_55342))], (208 ^ _48768) ^ [_55550, _55552] : [disjointwith(_55552, _55550), -(collection(_55552))], (214 ^ _48768) ^ [_55758, _55760] : [disjointwith(_55760, _55758), -(disjointwith(_55758, _55760))], (220 ^ _48768) ^ [_55982, _55984, _55986] : [-(disjointwith(_55986, _55982)), disjointwith(_55986, _55984), genls(_55982, _55984)], (230 ^ _48768) ^ [_56305, _56307, _56309] : [-(disjointwith(_56305, _56307)), disjointwith(_56309, _56307), genls(_56305, _56309)], (240 ^ _48768) ^ [] : [-(mtvisible(c_logicaltruthmt))], (242 ^ _48768) ^ [_56653] : [isa(_56653, c_transitivebinarypredicate), -(transitivebinarypredicate(_56653))], (248 ^ _48768) ^ [_56841] : [transitivebinarypredicate(_56841), -(isa(_56841, c_transitivebinarypredicate))], (254 ^ _48768) ^ [_57043, _57045] : [isa(_57045, _57043), -(collection(_57043))], (260 ^ _48768) ^ [_57251, _57253] : [isa(_57253, _57251), -(collection(_57251))], (266 ^ _48768) ^ [_57459, _57461] : [isa(_57461, _57459), -(thing(_57461))], (272 ^ _48768) ^ [_57667, _57669] : [isa(_57669, _57667), -(thing(_57669))], (278 ^ _48768) ^ [_57889, _57891, _57893] : [-(isa(_57893, _57889)), isa(_57893, _57891), genls(_57891, _57889)], (288 ^ _48768) ^ [] : [-(mtvisible(c_corecyclmt))], (290 ^ _48768) ^ [_58251, _58253] : [-(mtvisible(_58251)), mtvisible(_58253), genlmt(_58253, _58251)], (300 ^ _48768) ^ [_58546, _58548] : [genlmt(_58548, _58546), -(microtheory(_58546))], (306 ^ _48768) ^ [_58754, _58756] : [genlmt(_58756, _58754), -(microtheory(_58754))], (312 ^ _48768) ^ [_58962, _58964] : [genlmt(_58964, _58962), -(microtheory(_58964))], (318 ^ _48768) ^ [_59170, _59172] : [genlmt(_59172, _59170), -(microtheory(_59172))], (324 ^ _48768) ^ [_59392, _59394, _59396] : [-(genlmt(_59396, _59392)), genlmt(_59396, _59394), genlmt(_59394, _59392)], (334 ^ _48768) ^ [_59687] : [microtheory(_59687), -(genlmt(_59687, _59687))], (346 ^ _48768) ^ [] : [-(mtvisible(c_universalvocabularymt))], (340 ^ _48768) ^ [_59875] : [microtheory(_59875), -(genlmt(_59875, _59875))]], input).
% 0.35/1.41 ncf('1',plain,[collection(c_tptptptpcol_16_8398), individual(c_tptptptpcol_16_8398)],start(8 ^ 0,bind([[_49026], [c_tptptptpcol_16_8398]]))).
% 0.35/1.41 ncf('1.1',plain,[-(collection(c_tptptptpcol_16_8398)), disjointwith(c_tptptptpcol_16_8398, c_tptpcol_16_18488)],extension(208 ^ 1,bind([[_55550, _55552], [c_tptpcol_16_18488, c_tptptptpcol_16_8398]]))).
% 0.35/1.41 ncf('1.1.1',plain,[-(disjointwith(c_tptptptpcol_16_8398, c_tptpcol_16_18488))],extension(348 ^ 2)).
% 0.35/1.41 ncf('1.2',plain,[-(individual(c_tptptptpcol_16_8398))],extension(16 ^ 1)).
% 0.35/1.41 %-----------------------------------------------------
% 0.35/1.41 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------