%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR071+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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 11:01:07 EDT 2023
% Result : Theorem 0.36s 1.39s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR071+1 : TPTP v8.1.2. Released v3.4.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n024.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:12:21 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.36/1.39
% 0.36/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 ncf(matrix, plain, [(420 ^ _59864) ^ [] : [-(mtvisible(c_tptp_spindlecollectormt))], (422 ^ _59864) ^ [] : [tptpofobject(c_tptpnavypersonnel_3, f_tptpquantityfn_6(n_414))], (2 ^ _59864) ^ [] : [-(genls(c_navypersonnel, c_militaryperson))], (4 ^ _59864) ^ [_60016] : [navypersonnel(_60016), -(militaryperson(_60016))], (10 ^ _59864) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (12 ^ _59864) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (14 ^ _59864) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (16 ^ _59864) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (18 ^ _59864) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (20 ^ _59864) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (22 ^ _59864) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member698_mt))], (24 ^ _59864) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member1672_mt))], (26 ^ _59864) ^ [] : [-(genlmt(c_tptp_member3993_mt, c_tptp_spindleheadmt))], (28 ^ _59864) ^ [] : [-(genlmt(c_tptp_spindlecollectormt, c_tptp_member3993_mt))], (30 ^ _59864) ^ [_60732] : [-(tptpofobject(_60732, f_tptpquantityfn_6(n_414))), mtvisible(c_tptp_member698_mt), militaryperson(_60732)], (40 ^ _59864) ^ [] : [mtvisible(c_tptp_member698_mt), -(relationallinstance(c_tptpofobject, c_militaryperson, f_tptpquantityfn_6(n_414)))], (46 ^ _59864) ^ [] : [mtvisible(c_tptp_member1672_mt), -(navypersonnel(c_tptpnavypersonnel_3))], (52 ^ _59864) ^ [_61265, _61267, _61269] : [isa(_61269, _61267), isa(_61269, _61265), disjointwith(_61267, _61265)], (62 ^ _59864) ^ [_61587, _61589, _61591] : [-(genlpreds(_61591, _61587)), genlinverse(_61591, _61589), genlinverse(_61589, _61587)], (72 ^ _59864) ^ [_61896, _61898] : [genlpreds(_61898, _61896), -(predicate(_61896))], (78 ^ _59864) ^ [_62104, _62106] : [genlpreds(_62106, _62104), -(predicate(_62104))], (84 ^ _59864) ^ [_62312, _62314] : [genlpreds(_62314, _62312), -(predicate(_62314))], (90 ^ _59864) ^ [_62520, _62522] : [genlpreds(_62522, _62520), -(predicate(_62522))], (96 ^ _59864) ^ [_62742, _62744, _62746] : [-(genlpreds(_62746, _62742)), genlpreds(_62746, _62744), genlpreds(_62744, _62742)], (106 ^ _59864) ^ [_63037] : [predicate(_63037), -(genlpreds(_63037, _63037))], (112 ^ _59864) ^ [_63225] : [predicate(_63225), -(genlpreds(_63225, _63225))], (118 ^ _59864) ^ [_63427, _63429] : [genlinverse(_63429, _63427), -(binarypredicate(_63427))], (124 ^ _59864) ^ [_63635, _63637] : [genlinverse(_63637, _63635), -(binarypredicate(_63637))], (130 ^ _59864) ^ [_63857, _63859, _63861] : [-(genlinverse(_63857, _63859)), genlinverse(_63861, _63859), genlpreds(_63857, _63861)], (140 ^ _59864) ^ [_64180, _64182, _64184] : [-(genlinverse(_64184, _64180)), genlinverse(_64184, _64182), genlpreds(_64182, _64180)], (150 ^ _59864) ^ [_64489, _64491] : [disjointwith(_64491, _64489), -(collection(_64489))], (156 ^ _59864) ^ [_64697, _64699] : [disjointwith(_64699, _64697), -(collection(_64699))], (162 ^ _59864) ^ [_64905, _64907] : [disjointwith(_64907, _64905), -(disjointwith(_64905, _64907))], (168 ^ _59864) ^ [_65129, _65131, _65133] : [-(disjointwith(_65133, _65129)), disjointwith(_65133, _65131), genls(_65129, _65131)], (178 ^ _59864) ^ [_65452, _65454, _65456] : [-(disjointwith(_65452, _65454)), disjointwith(_65456, _65454), genls(_65452, _65456)], (188 ^ _59864) ^ [_65732] : [-(natfunction(f_tptpquantityfn_6(_65732), c_tptpquantityfn_6))], (190 ^ _59864) ^ [_65812] : [-(natargument(f_tptpquantityfn_6(_65812), n_1, _65812))], (192 ^ _59864) ^ [_65893] : [-(tptpquantity(f_tptpquantityfn_6(_65893)))], (194 ^ _59864) ^ [_66001, _66003] : [tptpofobject(_66003, _66001), -(tptpquantity(_66001))], (200 ^ _59864) ^ [_66209, _66211] : [tptpofobject(_66211, _66209), -(partiallytangible(_66211))], (206 ^ _59864) ^ [_66431, _66433, _66435] : [relationallinstance(_66435, _66433, _66431), -(thing(_66431))], (212 ^ _59864) ^ [_66661, _66663, _66665] : [relationallinstance(_66665, _66663, _66661), -(collection(_66663))], (218 ^ _59864) ^ [_66891, _66893, _66895] : [relationallinstance(_66895, _66893, _66891), -(binarypredicate(_66895))], (224 ^ _59864) ^ [] : [-(mtvisible(c_basekb))], (226 ^ _59864) ^ [_67146] : [isa(_67146, c_transitivebinarypredicate), -(transitivebinarypredicate(_67146))], (232 ^ _59864) ^ [_67334] : [transitivebinarypredicate(_67334), -(isa(_67334, c_transitivebinarypredicate))], (238 ^ _59864) ^ [_67536, _67538] : [isa(_67538, _67536), -(collection(_67536))], (244 ^ _59864) ^ [_67744, _67746] : [isa(_67746, _67744), -(collection(_67744))], (250 ^ _59864) ^ [_67952, _67954] : [isa(_67954, _67952), -(thing(_67954))], (256 ^ _59864) ^ [_68160, _68162] : [isa(_68162, _68160), -(thing(_68162))], (262 ^ _59864) ^ [_68382, _68384, _68386] : [-(isa(_68386, _68382)), isa(_68386, _68384), genls(_68384, _68382)], (272 ^ _59864) ^ [_68691, _68693] : [-(mtvisible(_68691)), mtvisible(_68693), genlmt(_68693, _68691)], (282 ^ _59864) ^ [_68986, _68988] : [genlmt(_68988, _68986), -(microtheory(_68986))], (288 ^ _59864) ^ [_69194, _69196] : [genlmt(_69196, _69194), -(microtheory(_69194))], (294 ^ _59864) ^ [_69402, _69404] : [genlmt(_69404, _69402), -(microtheory(_69404))], (300 ^ _59864) ^ [_69610, _69612] : [genlmt(_69612, _69610), -(microtheory(_69612))], (306 ^ _59864) ^ [_69832, _69834, _69836] : [-(genlmt(_69836, _69832)), genlmt(_69836, _69834), genlmt(_69834, _69832)], (316 ^ _59864) ^ [_70127] : [microtheory(_70127), -(genlmt(_70127, _70127))], (322 ^ _59864) ^ [_70315] : [microtheory(_70315), -(genlmt(_70315, _70315))], (328 ^ _59864) ^ [_70503] : [isa(_70503, c_militaryperson), -(militaryperson(_70503))], (334 ^ _59864) ^ [_70691] : [militaryperson(_70691), -(isa(_70691, c_militaryperson))], (340 ^ _59864) ^ [_70879] : [isa(_70879, c_navypersonnel), -(navypersonnel(_70879))], (346 ^ _59864) ^ [_71067] : [navypersonnel(_71067), -(isa(_71067, c_navypersonnel))], (352 ^ _59864) ^ [_71269, _71271] : [genls(_71271, _71269), -(collection(_71269))], (358 ^ _59864) ^ [_71477, _71479] : [genls(_71479, _71477), -(collection(_71477))], (364 ^ _59864) ^ [_71685, _71687] : [genls(_71687, _71685), -(collection(_71687))], (370 ^ _59864) ^ [_71893, _71895] : [genls(_71895, _71893), -(collection(_71895))], (376 ^ _59864) ^ [_72115, _72117, _72119] : [-(genls(_72119, _72115)), genls(_72119, _72117), genls(_72117, _72115)], (386 ^ _59864) ^ [_72410] : [collection(_72410), -(genls(_72410, _72410))], (392 ^ _59864) ^ [_72598] : [collection(_72598), -(genls(_72598, _72598))], (398 ^ _59864) ^ [_72814, _72816, _72818] : [-(genls(_72814, _72816)), genls(_72818, _72816), genls(_72814, _72818)], (418 ^ _59864) ^ [] : [-(mtvisible(c_universalvocabularymt))], (408 ^ _59864) ^ [_73137, _73139, _73141] : [-(genls(_73141, _73137)), genls(_73141, _73139), genls(_73139, _73137)]], input).
% 0.36/1.39 ncf('1',plain,[tptpofobject(c_tptpnavypersonnel_3, f_tptpquantityfn_6(n_414))],start(422 ^ 0)).
% 0.36/1.39 ncf('1.1',plain,[-(tptpofobject(c_tptpnavypersonnel_3, f_tptpquantityfn_6(n_414))), mtvisible(c_tptp_member698_mt), militaryperson(c_tptpnavypersonnel_3)],extension(30 ^ 1,bind([[_60732], [c_tptpnavypersonnel_3]]))).
% 0.36/1.39 ncf('1.1.1',plain,[-(mtvisible(c_tptp_member698_mt)), mtvisible(c_tptp_spindlecollectormt), genlmt(c_tptp_spindlecollectormt, c_tptp_member698_mt)],extension(272 ^ 2,bind([[_68691, _68693], [c_tptp_member698_mt, c_tptp_spindlecollectormt]]))).
% 0.36/1.39 ncf('1.1.1.1',plain,[-(mtvisible(c_tptp_spindlecollectormt))],extension(420 ^ 3)).
% 0.36/1.39 ncf('1.1.1.2',plain,[-(genlmt(c_tptp_spindlecollectormt, c_tptp_member698_mt))],extension(22 ^ 3)).
% 0.36/1.39 ncf('1.1.2',plain,[-(militaryperson(c_tptpnavypersonnel_3)), navypersonnel(c_tptpnavypersonnel_3)],extension(4 ^ 2,bind([[_60016], [c_tptpnavypersonnel_3]]))).
% 0.36/1.39 ncf('1.1.2.1',plain,[-(navypersonnel(c_tptpnavypersonnel_3)), mtvisible(c_tptp_member1672_mt)],extension(46 ^ 3)).
% 0.36/1.39 ncf('1.1.2.1.1',plain,[-(mtvisible(c_tptp_member1672_mt)), mtvisible(c_tptp_spindlecollectormt), genlmt(c_tptp_spindlecollectormt, c_tptp_member1672_mt)],extension(272 ^ 4,bind([[_68691, _68693], [c_tptp_member1672_mt, c_tptp_spindlecollectormt]]))).
% 0.36/1.39 ncf('1.1.2.1.1.1',plain,[-(mtvisible(c_tptp_spindlecollectormt))],extension(420 ^ 5)).
% 0.36/1.39 ncf('1.1.2.1.1.2',plain,[-(genlmt(c_tptp_spindlecollectormt, c_tptp_member1672_mt))],extension(24 ^ 5)).
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------