%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR056+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:49:04 EDT 2023
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR056+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n021.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 23:47:27 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.36/1.40
% 0.36/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 ncf(matrix, plain, [(414 ^ _59675) ^ [_73424] : [-(mtvisible(c_tptp_member3717_mt))], (416 ^ _59675) ^ [_73461] : [tptpofobject(c_tptpartsupplies, _73461)], (2 ^ _59675) ^ [] : [-(genls(c_artsupplies, c_supplies))], (4 ^ _59675) ^ [_59827] : [artsupplies(_59827), -(supplies(_59827))], (10 ^ _59675) ^ [] : [-(genlmt(c_calendarsmt, c_calendarsvocabularymt))], (12 ^ _59675) ^ [] : [-(transitivebinarypredicate(c_genlmt))], (14 ^ _59675) ^ [] : [-(genlmt(c_basekb, c_universalvocabularymt))], (16 ^ _59675) ^ [] : [-(genlmt(c_cyclistsmt, c_calendarsmt))], (18 ^ _59675) ^ [] : [-(genlmt(c_calendarsvocabularymt, c_basekb))], (20 ^ _59675) ^ [] : [-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))], (22 ^ _59675) ^ [] : [-(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt))], (24 ^ _59675) ^ [_60384] : [-(tptpofobject(_60384, f_tptpquantityfn_14(n_232))), mtvisible(c_tptp_spindleheadmt), supplies(_60384)], (34 ^ _59675) ^ [] : [mtvisible(c_tptp_spindleheadmt), -(relationallinstance(c_tptpofobject, c_supplies, f_tptpquantityfn_14(n_232)))], (40 ^ _59675) ^ [] : [mtvisible(c_cyclistsmt), -(artsupplies(c_tptpartsupplies))], (46 ^ _59675) ^ [_60917, _60919, _60921] : [isa(_60921, _60919), isa(_60921, _60917), disjointwith(_60919, _60917)], (56 ^ _59675) ^ [_61239, _61241, _61243] : [-(genlpreds(_61243, _61239)), genlinverse(_61243, _61241), genlinverse(_61241, _61239)], (66 ^ _59675) ^ [_61548, _61550] : [genlpreds(_61550, _61548), -(predicate(_61548))], (72 ^ _59675) ^ [_61756, _61758] : [genlpreds(_61758, _61756), -(predicate(_61756))], (78 ^ _59675) ^ [_61964, _61966] : [genlpreds(_61966, _61964), -(predicate(_61966))], (84 ^ _59675) ^ [_62172, _62174] : [genlpreds(_62174, _62172), -(predicate(_62174))], (90 ^ _59675) ^ [_62394, _62396, _62398] : [-(genlpreds(_62398, _62394)), genlpreds(_62398, _62396), genlpreds(_62396, _62394)], (100 ^ _59675) ^ [_62689] : [predicate(_62689), -(genlpreds(_62689, _62689))], (106 ^ _59675) ^ [_62877] : [predicate(_62877), -(genlpreds(_62877, _62877))], (112 ^ _59675) ^ [_63079, _63081] : [genlinverse(_63081, _63079), -(binarypredicate(_63079))], (118 ^ _59675) ^ [_63287, _63289] : [genlinverse(_63289, _63287), -(binarypredicate(_63289))], (124 ^ _59675) ^ [_63509, _63511, _63513] : [-(genlinverse(_63509, _63511)), genlinverse(_63513, _63511), genlpreds(_63509, _63513)], (134 ^ _59675) ^ [_63832, _63834, _63836] : [-(genlinverse(_63836, _63832)), genlinverse(_63836, _63834), genlpreds(_63834, _63832)], (144 ^ _59675) ^ [_64141, _64143] : [disjointwith(_64143, _64141), -(collection(_64141))], (150 ^ _59675) ^ [_64349, _64351] : [disjointwith(_64351, _64349), -(collection(_64351))], (156 ^ _59675) ^ [_64557, _64559] : [disjointwith(_64559, _64557), -(disjointwith(_64557, _64559))], (162 ^ _59675) ^ [_64781, _64783, _64785] : [-(disjointwith(_64785, _64781)), disjointwith(_64785, _64783), genls(_64781, _64783)], (172 ^ _59675) ^ [_65104, _65106, _65108] : [-(disjointwith(_65104, _65106)), disjointwith(_65108, _65106), genls(_65104, _65108)], (182 ^ _59675) ^ [_65384] : [-(natfunction(f_tptpquantityfn_14(_65384), c_tptpquantityfn_14))], (184 ^ _59675) ^ [_65464] : [-(natargument(f_tptpquantityfn_14(_65464), n_1, _65464))], (186 ^ _59675) ^ [_65545] : [-(tptpquantity(f_tptpquantityfn_14(_65545)))], (188 ^ _59675) ^ [_65653, _65655] : [tptpofobject(_65655, _65653), -(tptpquantity(_65653))], (194 ^ _59675) ^ [_65861, _65863] : [tptpofobject(_65863, _65861), -(partiallytangible(_65863))], (200 ^ _59675) ^ [_66083, _66085, _66087] : [relationallinstance(_66087, _66085, _66083), -(thing(_66083))], (206 ^ _59675) ^ [_66313, _66315, _66317] : [relationallinstance(_66317, _66315, _66313), -(collection(_66315))], (212 ^ _59675) ^ [_66543, _66545, _66547] : [relationallinstance(_66547, _66545, _66543), -(binarypredicate(_66547))], (218 ^ _59675) ^ [] : [-(mtvisible(c_basekb))], (220 ^ _59675) ^ [_66798] : [isa(_66798, c_transitivebinarypredicate), -(transitivebinarypredicate(_66798))], (226 ^ _59675) ^ [_66986] : [transitivebinarypredicate(_66986), -(isa(_66986, c_transitivebinarypredicate))], (232 ^ _59675) ^ [_67188, _67190] : [isa(_67190, _67188), -(collection(_67188))], (238 ^ _59675) ^ [_67396, _67398] : [isa(_67398, _67396), -(collection(_67396))], (244 ^ _59675) ^ [_67604, _67606] : [isa(_67606, _67604), -(thing(_67606))], (250 ^ _59675) ^ [_67812, _67814] : [isa(_67814, _67812), -(thing(_67814))], (256 ^ _59675) ^ [_68034, _68036, _68038] : [-(isa(_68038, _68034)), isa(_68038, _68036), genls(_68036, _68034)], (266 ^ _59675) ^ [_68343, _68345] : [-(mtvisible(_68343)), mtvisible(_68345), genlmt(_68345, _68343)], (276 ^ _59675) ^ [_68638, _68640] : [genlmt(_68640, _68638), -(microtheory(_68638))], (282 ^ _59675) ^ [_68846, _68848] : [genlmt(_68848, _68846), -(microtheory(_68846))], (288 ^ _59675) ^ [_69054, _69056] : [genlmt(_69056, _69054), -(microtheory(_69056))], (294 ^ _59675) ^ [_69262, _69264] : [genlmt(_69264, _69262), -(microtheory(_69264))], (300 ^ _59675) ^ [_69484, _69486, _69488] : [-(genlmt(_69488, _69484)), genlmt(_69488, _69486), genlmt(_69486, _69484)], (310 ^ _59675) ^ [_69779] : [microtheory(_69779), -(genlmt(_69779, _69779))], (316 ^ _59675) ^ [_69967] : [microtheory(_69967), -(genlmt(_69967, _69967))], (322 ^ _59675) ^ [_70155] : [isa(_70155, c_supplies), -(supplies(_70155))], (328 ^ _59675) ^ [_70343] : [supplies(_70343), -(isa(_70343, c_supplies))], (334 ^ _59675) ^ [_70531] : [isa(_70531, c_artsupplies), -(artsupplies(_70531))], (340 ^ _59675) ^ [_70719] : [artsupplies(_70719), -(isa(_70719, c_artsupplies))], (346 ^ _59675) ^ [_70921, _70923] : [genls(_70923, _70921), -(collection(_70921))], (352 ^ _59675) ^ [_71129, _71131] : [genls(_71131, _71129), -(collection(_71129))], (358 ^ _59675) ^ [_71337, _71339] : [genls(_71339, _71337), -(collection(_71339))], (364 ^ _59675) ^ [_71545, _71547] : [genls(_71547, _71545), -(collection(_71547))], (370 ^ _59675) ^ [_71767, _71769, _71771] : [-(genls(_71771, _71767)), genls(_71771, _71769), genls(_71769, _71767)], (380 ^ _59675) ^ [_72062] : [collection(_72062), -(genls(_72062, _72062))], (386 ^ _59675) ^ [_72250] : [collection(_72250), -(genls(_72250, _72250))], (392 ^ _59675) ^ [_72466, _72468, _72470] : [-(genls(_72466, _72468)), genls(_72470, _72468), genls(_72466, _72470)], (412 ^ _59675) ^ [] : [-(mtvisible(c_universalvocabularymt))], (402 ^ _59675) ^ [_72789, _72791, _72793] : [-(genls(_72793, _72789)), genls(_72793, _72791), genls(_72791, _72789)]], input).
% 0.36/1.40 ncf('1',plain,[tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232))],start(416 ^ 0,bind([[_73461], [f_tptpquantityfn_14(n_232)]]))).
% 0.36/1.40 ncf('1.1',plain,[-(tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232))), mtvisible(c_tptp_spindleheadmt), supplies(c_tptpartsupplies)],extension(24 ^ 1,bind([[_60384], [c_tptpartsupplies]]))).
% 0.36/1.40 ncf('1.1.1',plain,[-(mtvisible(c_tptp_spindleheadmt)), mtvisible(c_tptp_member3717_mt), genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt)],extension(266 ^ 2,bind([[_68343, _68345], [c_tptp_spindleheadmt, c_tptp_member3717_mt]]))).
% 0.36/1.40 ncf('1.1.1.1',plain,[-(mtvisible(c_tptp_member3717_mt))],extension(414 ^ 3,bind([[_73424], [_42867]]))).
% 0.36/1.40 ncf('1.1.1.2',plain,[-(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt))],extension(22 ^ 3)).
% 0.36/1.40 ncf('1.1.2',plain,[-(supplies(c_tptpartsupplies)), artsupplies(c_tptpartsupplies)],extension(4 ^ 2,bind([[_59827], [c_tptpartsupplies]]))).
% 0.36/1.40 ncf('1.1.2.1',plain,[-(artsupplies(c_tptpartsupplies)), mtvisible(c_cyclistsmt)],extension(40 ^ 3)).
% 0.36/1.40 ncf('1.1.2.1.1',plain,[-(mtvisible(c_cyclistsmt)), mtvisible(c_tptp_member3717_mt), genlmt(c_tptp_member3717_mt, c_cyclistsmt)],extension(266 ^ 4,bind([[_68343, _68345], [c_cyclistsmt, c_tptp_member3717_mt]]))).
% 0.36/1.40 ncf('1.1.2.1.1.1',plain,[-(mtvisible(c_tptp_member3717_mt))],extension(414 ^ 5,bind([[_73424], [_43578]]))).
% 0.36/1.40 ncf('1.1.2.1.1.2',plain,[-(genlmt(c_tptp_member3717_mt, c_cyclistsmt)), genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptp_spindleheadmt, c_cyclistsmt)],extension(300 ^ 5,bind([[_69484, _69486, _69488], [c_cyclistsmt, c_tptp_spindleheadmt, c_tptp_member3717_mt]]))).
% 0.36/1.40 ncf('1.1.2.1.1.2.1',plain,[-(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt))],extension(22 ^ 6)).
% 0.36/1.40 ncf('1.1.2.1.1.2.2',plain,[-(genlmt(c_tptp_spindleheadmt, c_cyclistsmt))],extension(20 ^ 6)).
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------