%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR028+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:26:15 EDT 2023
% Result : Theorem 0.31s 1.38s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR028+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n006.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 00:29:36 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.31/1.38
% 0.31/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.31/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.38 %-----------------------------------------------------
% 0.31/1.38 ncf(matrix, plain, [(272 ^ _38492) ^ [] : [-(mtvisible(c_tptp_member2089_mt))], (274 ^ _38492) ^ [] : [individual(c_tptptptpcol_16_25985)], (2 ^ _38492) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (4 ^ _38492) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (6 ^ _38492) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (8 ^ _38492) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (10 ^ _38492) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (12 ^ _38492) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (14 ^ _38492) ^ [] : [-(genlmt(c_tptp_member2089_mt, c_tptp_spindleheadmt))], (16 ^ _38492) ^ [] : [-(individual(c_tptptptpcol_16_25985))], (18 ^ _38492) ^ [_39043, _39045, _39047] : [isa(_39047, _39045), isa(_39047, _39043), disjointwith(_39045, _39043)], (28 ^ _38492) ^ [_39365, _39367, _39369] : [-(genlpreds(_39369, _39365)), genlinverse(_39369, _39367), genlinverse(_39367, _39365)], (38 ^ _38492) ^ [_39674, _39676] : [genlpreds(_39676, _39674), -(predicate(_39674))], (44 ^ _38492) ^ [_39882, _39884] : [genlpreds(_39884, _39882), -(predicate(_39882))], (50 ^ _38492) ^ [_40090, _40092] : [genlpreds(_40092, _40090), -(predicate(_40092))], (56 ^ _38492) ^ [_40298, _40300] : [genlpreds(_40300, _40298), -(predicate(_40300))], (62 ^ _38492) ^ [_40520, _40522, _40524] : [-(genlpreds(_40524, _40520)), genlpreds(_40524, _40522), genlpreds(_40522, _40520)], (72 ^ _38492) ^ [_40815] : [predicate(_40815), -(genlpreds(_40815, _40815))], (78 ^ _38492) ^ [_41003] : [predicate(_41003), -(genlpreds(_41003, _41003))], (84 ^ _38492) ^ [_41205, _41207] : [genlinverse(_41207, _41205), -(binarypredicate(_41205))], (90 ^ _38492) ^ [_41413, _41415] : [genlinverse(_41415, _41413), -(binarypredicate(_41415))], (96 ^ _38492) ^ [_41635, _41637, _41639] : [-(genlinverse(_41635, _41637)), genlinverse(_41639, _41637), genlpreds(_41635, _41639)], (106 ^ _38492) ^ [_41958, _41960, _41962] : [-(genlinverse(_41962, _41958)), genlinverse(_41962, _41960), genlpreds(_41960, _41958)], (116 ^ _38492) ^ [_42267, _42269] : [disjointwith(_42269, _42267), -(collection(_42267))], (122 ^ _38492) ^ [_42475, _42477] : [disjointwith(_42477, _42475), -(collection(_42477))], (128 ^ _38492) ^ [_42683, _42685] : [disjointwith(_42685, _42683), -(disjointwith(_42683, _42685))], (134 ^ _38492) ^ [_42907, _42909, _42911] : [-(disjointwith(_42911, _42907)), disjointwith(_42911, _42909), genls(_42907, _42909)], (144 ^ _38492) ^ [_43230, _43232, _43234] : [-(disjointwith(_43230, _43232)), disjointwith(_43234, _43232), genls(_43230, _43234)], (154 ^ _38492) ^ [_43525] : [isa(_43525, c_individual), -(individual(_43525))], (160 ^ _38492) ^ [_43713] : [individual(_43713), -(isa(_43713, c_individual))], (166 ^ _38492) ^ [] : [-(mtvisible(c_basekb))], (168 ^ _38492) ^ [_43954] : [isa(_43954, c_transitivebinarypredicate), -(transitivebinarypredicate(_43954))], (174 ^ _38492) ^ [_44142] : [transitivebinarypredicate(_44142), -(isa(_44142, c_transitivebinarypredicate))], (180 ^ _38492) ^ [_44344, _44346] : [isa(_44346, _44344), -(collection(_44344))], (186 ^ _38492) ^ [_44552, _44554] : [isa(_44554, _44552), -(collection(_44552))], (192 ^ _38492) ^ [_44760, _44762] : [isa(_44762, _44760), -(thing(_44762))], (198 ^ _38492) ^ [_44968, _44970] : [isa(_44970, _44968), -(thing(_44970))], (204 ^ _38492) ^ [_45190, _45192, _45194] : [-(isa(_45194, _45190)), isa(_45194, _45192), genls(_45192, _45190)], (214 ^ _38492) ^ [_45499, _45501] : [-(mtvisible(_45499)), mtvisible(_45501), genlmt(_45501, _45499)], (224 ^ _38492) ^ [_45794, _45796] : [genlmt(_45796, _45794), -(microtheory(_45794))], (230 ^ _38492) ^ [_46002, _46004] : [genlmt(_46004, _46002), -(microtheory(_46002))], (236 ^ _38492) ^ [_46210, _46212] : [genlmt(_46212, _46210), -(microtheory(_46212))], (242 ^ _38492) ^ [_46418, _46420] : [genlmt(_46420, _46418), -(microtheory(_46420))], (248 ^ _38492) ^ [_46640, _46642, _46644] : [-(genlmt(_46644, _46640)), genlmt(_46644, _46642), genlmt(_46642, _46640)], (258 ^ _38492) ^ [_46935] : [microtheory(_46935), -(genlmt(_46935, _46935))], (270 ^ _38492) ^ [] : [-(mtvisible(c_universalvocabularymt))], (264 ^ _38492) ^ [_47123] : [microtheory(_47123), -(genlmt(_47123, _47123))]], input).
% 0.31/1.38 ncf('1',plain,[individual(c_tptptptpcol_16_25985)],start(274 ^ 0)).
% 0.31/1.38 ncf('1.1',plain,[-(individual(c_tptptptpcol_16_25985))],extension(16 ^ 1)).
% 0.31/1.38 %-----------------------------------------------------
% 0.31/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------