%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR055+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:48:13 EDT 2023
% Result : Theorem 0.31s 1.39s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR055+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n001.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 : Fri May 19 00:18:20 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.31/1.39
% 0.31/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.31/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.39 %-----------------------------------------------------
% 0.31/1.39 ncf(matrix, plain, [(348 ^ _48712) ^ [] : [-(disjointwith(c_xskijump_thegame, c_tptpcol_16_35301))], (2 ^ _48712) ^ [] : [-(individual(c_xskijump_thegame))], (4 ^ _48712) ^ [] : [-(genlmt(c_universalvocabularymt, c_corecyclmt))], (6 ^ _48712) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (8 ^ _48712) ^ [] : [-(genlmt(c_corecyclmt, c_logicaltruthmt))], (10 ^ _48712) ^ [_49023] : [collection(_49023), individual(_49023)], (16 ^ _48712) ^ [] : [-(disjointwith(c_collection, c_individual))], (18 ^ _48712) ^ [_49289, _49291, _49293] : [isa(_49293, _49291), isa(_49293, _49289), disjointwith(_49291, _49289)], (28 ^ _48712) ^ [_49611, _49613, _49615] : [-(genlpreds(_49615, _49611)), genlinverse(_49615, _49613), genlinverse(_49613, _49611)], (38 ^ _48712) ^ [] : [-(arg2isa(c_disjointwith, c_collection))], (40 ^ _48712) ^ [_49973, _49975] : [disjointwith(_49975, _49973), -(collection(_49973))], (46 ^ _48712) ^ [_50195, _50197, _50199] : [isa(_50199, _50197), isa(_50199, _50195), disjointwith(_50197, _50195)], (56 ^ _48712) ^ [_50517, _50519, _50521] : [-(genlpreds(_50521, _50517)), genlinverse(_50521, _50519), genlinverse(_50519, _50517)], (66 ^ _48712) ^ [_50826, _50828] : [arg2isa(_50828, _50826), -(collection(_50826))], (72 ^ _48712) ^ [_51034, _51036] : [arg2isa(_51036, _51034), -(relation(_51036))], (78 ^ _48712) ^ [_51256, _51258, _51260] : [-(arg2isa(_51260, _51256)), arg2isa(_51260, _51258), genls(_51258, _51256)], (88 ^ _48712) ^ [_51579, _51581, _51583] : [-(arg2isa(_51583, _51579)), arg2isa(_51583, _51581), genls(_51581, _51579)], (98 ^ _48712) ^ [_51888, _51890] : [genlpreds(_51890, _51888), -(predicate(_51888))], (104 ^ _48712) ^ [_52096, _52098] : [genlpreds(_52098, _52096), -(predicate(_52096))], (110 ^ _48712) ^ [_52304, _52306] : [genlpreds(_52306, _52304), -(predicate(_52306))], (116 ^ _48712) ^ [_52512, _52514] : [genlpreds(_52514, _52512), -(predicate(_52514))], (122 ^ _48712) ^ [_52734, _52736, _52738] : [-(genlpreds(_52738, _52734)), genlpreds(_52738, _52736), genlpreds(_52736, _52734)], (132 ^ _48712) ^ [_53029] : [predicate(_53029), -(genlpreds(_53029, _53029))], (138 ^ _48712) ^ [_53217] : [predicate(_53217), -(genlpreds(_53217, _53217))], (144 ^ _48712) ^ [_53419, _53421] : [genlinverse(_53421, _53419), -(binarypredicate(_53419))], (150 ^ _48712) ^ [_53627, _53629] : [genlinverse(_53629, _53627), -(binarypredicate(_53629))], (156 ^ _48712) ^ [_53849, _53851, _53853] : [-(genlinverse(_53849, _53851)), genlinverse(_53853, _53851), genlpreds(_53849, _53853)], (166 ^ _48712) ^ [_54172, _54174, _54176] : [-(genlinverse(_54176, _54172)), genlinverse(_54176, _54174), genlpreds(_54174, _54172)], (176 ^ _48712) ^ [] : [-(mtvisible(c_basekb))], (178 ^ _48712) ^ [_54520] : [isa(_54520, c_collection), -(collection(_54520))], (184 ^ _48712) ^ [_54708] : [collection(_54708), -(isa(_54708, c_collection))], (190 ^ _48712) ^ [_54910, _54912] : [disjointwith(_54912, _54910), -(collection(_54910))], (196 ^ _48712) ^ [_55118, _55120] : [disjointwith(_55120, _55118), -(collection(_55120))], (202 ^ _48712) ^ [_55326, _55328] : [disjointwith(_55328, _55326), -(disjointwith(_55326, _55328))], (208 ^ _48712) ^ [_55550, _55552, _55554] : [-(disjointwith(_55554, _55550)), disjointwith(_55554, _55552), genls(_55550, _55552)], (218 ^ _48712) ^ [_55873, _55875, _55877] : [-(disjointwith(_55873, _55875)), disjointwith(_55877, _55875), genls(_55873, _55877)], (228 ^ _48712) ^ [] : [-(mtvisible(c_logicaltruthmt))], (230 ^ _48712) ^ [_56221] : [isa(_56221, c_transitivebinarypredicate), -(transitivebinarypredicate(_56221))], (236 ^ _48712) ^ [_56409] : [transitivebinarypredicate(_56409), -(isa(_56409, c_transitivebinarypredicate))], (242 ^ _48712) ^ [] : [-(mtvisible(c_corecyclmt))], (244 ^ _48712) ^ [_56664, _56666] : [-(mtvisible(_56664)), mtvisible(_56666), genlmt(_56666, _56664)], (254 ^ _48712) ^ [_56959, _56961] : [genlmt(_56961, _56959), -(microtheory(_56959))], (260 ^ _48712) ^ [_57167, _57169] : [genlmt(_57169, _57167), -(microtheory(_57167))], (266 ^ _48712) ^ [_57375, _57377] : [genlmt(_57377, _57375), -(microtheory(_57377))], (272 ^ _48712) ^ [_57583, _57585] : [genlmt(_57585, _57583), -(microtheory(_57585))], (278 ^ _48712) ^ [_57805, _57807, _57809] : [-(genlmt(_57809, _57805)), genlmt(_57809, _57807), genlmt(_57807, _57805)], (288 ^ _48712) ^ [_58100] : [microtheory(_58100), -(genlmt(_58100, _58100))], (294 ^ _48712) ^ [_58288] : [microtheory(_58288), -(genlmt(_58288, _58288))], (300 ^ _48712) ^ [_58476] : [isa(_58476, c_individual), -(individual(_58476))], (306 ^ _48712) ^ [_58664] : [individual(_58664), -(isa(_58664, c_individual))], (312 ^ _48712) ^ [_58866, _58868] : [isa(_58868, _58866), -(collection(_58866))], (318 ^ _48712) ^ [_59074, _59076] : [isa(_59076, _59074), -(collection(_59074))], (324 ^ _48712) ^ [_59282, _59284] : [isa(_59284, _59282), -(thing(_59284))], (330 ^ _48712) ^ [_59490, _59492] : [isa(_59492, _59490), -(thing(_59492))], (346 ^ _48712) ^ [] : [-(mtvisible(c_universalvocabularymt))], (336 ^ _48712) ^ [_59712, _59714, _59716] : [-(isa(_59716, _59712)), isa(_59716, _59714), genls(_59714, _59712)]], input).
% 0.31/1.39 ncf('1',plain,[collection(c_xskijump_thegame), individual(c_xskijump_thegame)],start(10 ^ 0,bind([[_49023], [c_xskijump_thegame]]))).
% 0.31/1.39 ncf('1.1',plain,[-(collection(c_xskijump_thegame)), disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)],extension(196 ^ 1,bind([[_55118, _55120], [c_tptpcol_16_35301, c_xskijump_thegame]]))).
% 0.31/1.39 ncf('1.1.1',plain,[-(disjointwith(c_xskijump_thegame, c_tptpcol_16_35301))],extension(348 ^ 2)).
% 0.31/1.39 ncf('1.2',plain,[-(individual(c_xskijump_thegame))],extension(2 ^ 1)).
% 0.31/1.39 %-----------------------------------------------------
% 0.31/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------