%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR045+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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:40:05 EDT 2023
% Result : Theorem 0.34s 1.38s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR045+1 : TPTP v8.1.2. Released v3.4.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n004.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:05:39 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.34/1.38
% 0.34/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 ncf(matrix, plain, [(514 ^ _69385) ^ [] : [-(genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088))], (2 ^ _69385) ^ [] : [-(applicationcontext(c_wamt_evalinitial_p14))], (4 ^ _69385) ^ [] : [-(genls(c_microtheory, c_aspatialinformationstore))], (6 ^ _69385) ^ [_69590] : [microtheory(_69590), -(aspatialinformationstore(_69590))], (12 ^ _69385) ^ [] : [-(genlmt(c_universalvocabularymt, c_corecyclmt))], (14 ^ _69385) ^ [] : [-(genls(c_intangibleindividual, c_partiallyintangibleindividual))], (16 ^ _69385) ^ [_69882] : [intangibleindividual(_69882), -(partiallyintangibleindividual(_69882))], (22 ^ _69385) ^ [] : [-(genls(c_aspatialinformationstore, c_intangibleindividual))], (24 ^ _69385) ^ [_70121] : [aspatialinformationstore(_70121), -(intangibleindividual(_70121))], (30 ^ _69385) ^ [] : [-(genls(c_partiallyintangibleindividual, c_individual))], (32 ^ _69385) ^ [_70360] : [partiallyintangibleindividual(_70360), -(individual(_70360))], (38 ^ _69385) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (40 ^ _69385) ^ [] : [-(genlmt(c_corecyclmt, c_logicaltruthmt))], (42 ^ _69385) ^ [] : [-(genls(c_applicationcontext, c_microtheory))], (44 ^ _69385) ^ [_70705] : [applicationcontext(_70705), -(microtheory(_70705))], (50 ^ _69385) ^ [_70891] : [collection(_70891), individual(_70891)], (56 ^ _69385) ^ [] : [-(disjointwith(c_collection, c_individual))], (58 ^ _69385) ^ [_71157, _71159, _71161] : [isa(_71161, _71159), isa(_71161, _71157), disjointwith(_71159, _71157)], (68 ^ _69385) ^ [_71479, _71481, _71483] : [-(genlpreds(_71483, _71479)), genlinverse(_71483, _71481), genlinverse(_71481, _71479)], (78 ^ _69385) ^ [] : [-(arg1isa(c_genls, c_collection))], (80 ^ _69385) ^ [_71841, _71843] : [genls(_71843, _71841), -(collection(_71843))], (86 ^ _69385) ^ [_72063, _72065, _72067] : [isa(_72067, _72065), isa(_72067, _72063), disjointwith(_72065, _72063)], (96 ^ _69385) ^ [_72385, _72387, _72389] : [-(genlpreds(_72389, _72385)), genlinverse(_72389, _72387), genlinverse(_72387, _72385)], (106 ^ _69385) ^ [_72694, _72696] : [arg1isa(_72696, _72694), -(collection(_72694))], (112 ^ _69385) ^ [_72902, _72904] : [arg1isa(_72904, _72902), -(relation(_72904))], (118 ^ _69385) ^ [_73124, _73126, _73128] : [-(arg1isa(_73128, _73124)), arg1isa(_73128, _73126), genls(_73126, _73124)], (128 ^ _69385) ^ [_73447, _73449, _73451] : [-(arg1isa(_73451, _73447)), arg1isa(_73451, _73449), genls(_73449, _73447)], (138 ^ _69385) ^ [_73756, _73758] : [genlpreds(_73758, _73756), -(predicate(_73756))], (144 ^ _69385) ^ [_73964, _73966] : [genlpreds(_73966, _73964), -(predicate(_73964))], (150 ^ _69385) ^ [_74172, _74174] : [genlpreds(_74174, _74172), -(predicate(_74174))], (156 ^ _69385) ^ [_74380, _74382] : [genlpreds(_74382, _74380), -(predicate(_74382))], (162 ^ _69385) ^ [_74602, _74604, _74606] : [-(genlpreds(_74606, _74602)), genlpreds(_74606, _74604), genlpreds(_74604, _74602)], (172 ^ _69385) ^ [_74897] : [predicate(_74897), -(genlpreds(_74897, _74897))], (178 ^ _69385) ^ [_75085] : [predicate(_75085), -(genlpreds(_75085, _75085))], (184 ^ _69385) ^ [_75287, _75289] : [genlinverse(_75289, _75287), -(binarypredicate(_75287))], (190 ^ _69385) ^ [_75495, _75497] : [genlinverse(_75497, _75495), -(binarypredicate(_75497))], (196 ^ _69385) ^ [_75717, _75719, _75721] : [-(genlinverse(_75717, _75719)), genlinverse(_75721, _75719), genlpreds(_75717, _75721)], (206 ^ _69385) ^ [_76040, _76042, _76044] : [-(genlinverse(_76044, _76040)), genlinverse(_76044, _76042), genlpreds(_76042, _76040)], (216 ^ _69385) ^ [] : [-(mtvisible(c_basekb))], (218 ^ _69385) ^ [_76388] : [isa(_76388, c_collection), -(collection(_76388))], (224 ^ _69385) ^ [_76576] : [collection(_76576), -(isa(_76576, c_collection))], (230 ^ _69385) ^ [_76778, _76780] : [disjointwith(_76780, _76778), -(collection(_76778))], (236 ^ _69385) ^ [_76986, _76988] : [disjointwith(_76988, _76986), -(collection(_76988))], (242 ^ _69385) ^ [_77194, _77196] : [disjointwith(_77196, _77194), -(disjointwith(_77194, _77196))], (248 ^ _69385) ^ [_77418, _77420, _77422] : [-(disjointwith(_77422, _77418)), disjointwith(_77422, _77420), genls(_77418, _77420)], (258 ^ _69385) ^ [_77741, _77743, _77745] : [-(disjointwith(_77741, _77743)), disjointwith(_77745, _77743), genls(_77741, _77745)], (268 ^ _69385) ^ [] : [-(mtvisible(c_logicaltruthmt))], (270 ^ _69385) ^ [_78089] : [isa(_78089, c_transitivebinarypredicate), -(transitivebinarypredicate(_78089))], (276 ^ _69385) ^ [_78277] : [transitivebinarypredicate(_78277), -(isa(_78277, c_transitivebinarypredicate))], (282 ^ _69385) ^ [_78465] : [isa(_78465, c_individual), -(individual(_78465))], (288 ^ _69385) ^ [_78653] : [individual(_78653), -(isa(_78653, c_individual))], (294 ^ _69385) ^ [_78841] : [isa(_78841, c_partiallyintangibleindividual), -(partiallyintangibleindividual(_78841))], (300 ^ _69385) ^ [_79029] : [partiallyintangibleindividual(_79029), -(isa(_79029, c_partiallyintangibleindividual))], (306 ^ _69385) ^ [_79217] : [isa(_79217, c_intangibleindividual), -(intangibleindividual(_79217))], (312 ^ _69385) ^ [_79405] : [intangibleindividual(_79405), -(isa(_79405, c_intangibleindividual))], (318 ^ _69385) ^ [] : [-(mtvisible(c_corecyclmt))], (320 ^ _69385) ^ [_79660, _79662] : [-(mtvisible(_79660)), mtvisible(_79662), genlmt(_79662, _79660)], (330 ^ _69385) ^ [_79955, _79957] : [genlmt(_79957, _79955), -(microtheory(_79955))], (336 ^ _69385) ^ [_80163, _80165] : [genlmt(_80165, _80163), -(microtheory(_80163))], (342 ^ _69385) ^ [_80371, _80373] : [genlmt(_80373, _80371), -(microtheory(_80373))], (348 ^ _69385) ^ [_80579, _80581] : [genlmt(_80581, _80579), -(microtheory(_80581))], (354 ^ _69385) ^ [_80801, _80803, _80805] : [-(genlmt(_80805, _80801)), genlmt(_80805, _80803), genlmt(_80803, _80801)], (364 ^ _69385) ^ [_81096] : [microtheory(_81096), -(genlmt(_81096, _81096))], (370 ^ _69385) ^ [_81284] : [microtheory(_81284), -(genlmt(_81284, _81284))], (376 ^ _69385) ^ [_81472] : [isa(_81472, c_aspatialinformationstore), -(aspatialinformationstore(_81472))], (382 ^ _69385) ^ [_81660] : [aspatialinformationstore(_81660), -(isa(_81660, c_aspatialinformationstore))], (388 ^ _69385) ^ [_81848] : [isa(_81848, c_microtheory), -(microtheory(_81848))], (394 ^ _69385) ^ [_82036] : [microtheory(_82036), -(isa(_82036, c_microtheory))], (400 ^ _69385) ^ [_82238, _82240] : [genls(_82240, _82238), -(collection(_82238))], (406 ^ _69385) ^ [_82446, _82448] : [genls(_82448, _82446), -(collection(_82446))], (412 ^ _69385) ^ [_82654, _82656] : [genls(_82656, _82654), -(collection(_82656))], (418 ^ _69385) ^ [_82862, _82864] : [genls(_82864, _82862), -(collection(_82864))], (424 ^ _69385) ^ [_83084, _83086, _83088] : [-(genls(_83088, _83084)), genls(_83088, _83086), genls(_83086, _83084)], (434 ^ _69385) ^ [_83379] : [collection(_83379), -(genls(_83379, _83379))], (440 ^ _69385) ^ [_83567] : [collection(_83567), -(genls(_83567, _83567))], (446 ^ _69385) ^ [_83783, _83785, _83787] : [-(genls(_83783, _83785)), genls(_83787, _83785), genls(_83783, _83787)], (456 ^ _69385) ^ [_84106, _84108, _84110] : [-(genls(_84110, _84106)), genls(_84110, _84108), genls(_84108, _84106)], (466 ^ _69385) ^ [_84401] : [isa(_84401, c_applicationcontext), -(applicationcontext(_84401))], (472 ^ _69385) ^ [_84589] : [applicationcontext(_84589), -(isa(_84589, c_applicationcontext))], (478 ^ _69385) ^ [_84791, _84793] : [isa(_84793, _84791), -(collection(_84791))], (484 ^ _69385) ^ [_84999, _85001] : [isa(_85001, _84999), -(collection(_84999))], (490 ^ _69385) ^ [_85207, _85209] : [isa(_85209, _85207), -(thing(_85209))], (496 ^ _69385) ^ [_85415, _85417] : [isa(_85417, _85415), -(thing(_85417))], (512 ^ _69385) ^ [] : [-(mtvisible(c_universalvocabularymt))], (502 ^ _69385) ^ [_85637, _85639, _85641] : [-(isa(_85641, _85637)), isa(_85641, _85639), genls(_85639, _85637)]], input).
% 0.34/1.38 ncf('1',plain,[collection(c_wamt_evalinitial_p14), individual(c_wamt_evalinitial_p14)],start(50 ^ 0,bind([[_70891], [c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.1',plain,[-(collection(c_wamt_evalinitial_p14)), genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088)],extension(80 ^ 1,bind([[_71841, _71843], [c_tptpcol_15_80088, c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.1.1',plain,[-(genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088))],extension(514 ^ 2)).
% 0.34/1.38 ncf('1.2',plain,[-(individual(c_wamt_evalinitial_p14)), partiallyintangibleindividual(c_wamt_evalinitial_p14)],extension(32 ^ 1,bind([[_70360], [c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.2.1',plain,[-(partiallyintangibleindividual(c_wamt_evalinitial_p14)), intangibleindividual(c_wamt_evalinitial_p14)],extension(16 ^ 2,bind([[_69882], [c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.2.1.1',plain,[-(intangibleindividual(c_wamt_evalinitial_p14)), aspatialinformationstore(c_wamt_evalinitial_p14)],extension(24 ^ 3,bind([[_70121], [c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.2.1.1.1',plain,[-(aspatialinformationstore(c_wamt_evalinitial_p14)), microtheory(c_wamt_evalinitial_p14)],extension(6 ^ 4,bind([[_69590], [c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.2.1.1.1.1',plain,[-(microtheory(c_wamt_evalinitial_p14)), applicationcontext(c_wamt_evalinitial_p14)],extension(44 ^ 5,bind([[_70705], [c_wamt_evalinitial_p14]]))).
% 0.34/1.38 ncf('1.2.1.1.1.1.1',plain,[-(applicationcontext(c_wamt_evalinitial_p14))],extension(2 ^ 6)).
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------