%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR053+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:46:36 EDT 2023
% Result : Theorem 0.28s 1.38s
% Output : Proof 0.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR053+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n012.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:36:31 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.28/1.38
% 0.28/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.28/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.28/1.38 %-----------------------------------------------------
% 0.28/1.38 ncf(matrix, plain, [(208 ^ _30804) ^ [] : [-(mtvisible(c_tptpgeo_member1_mt))], (210 ^ _30804) ^ [] : [geographicalsubregions(c_georegion_l3_x11_y2, c_georegion_l4_x35_y7)], (2 ^ _30804) ^ [] : [mtvisible(c_tptpgeo_member1_mt), -(geographicalsubregions(c_georegion_l3_x11_y2, c_georegion_l4_x35_y7))], (8 ^ _30804) ^ [_31050, _31052, _31054] : [isa(_31054, _31052), isa(_31054, _31050), disjointwith(_31052, _31050)], (18 ^ _30804) ^ [_31372, _31374, _31376] : [-(genlpreds(_31376, _31372)), genlinverse(_31376, _31374), genlinverse(_31374, _31372)], (28 ^ _30804) ^ [_31681, _31683] : [genlpreds(_31683, _31681), -(predicate(_31681))], (34 ^ _30804) ^ [_31889, _31891] : [genlpreds(_31891, _31889), -(predicate(_31889))], (40 ^ _30804) ^ [_32097, _32099] : [genlpreds(_32099, _32097), -(predicate(_32099))], (46 ^ _30804) ^ [_32305, _32307] : [genlpreds(_32307, _32305), -(predicate(_32307))], (52 ^ _30804) ^ [_32527, _32529, _32531] : [-(genlpreds(_32531, _32527)), genlpreds(_32531, _32529), genlpreds(_32529, _32527)], (62 ^ _30804) ^ [_32822] : [predicate(_32822), -(genlpreds(_32822, _32822))], (68 ^ _30804) ^ [_33010] : [predicate(_33010), -(genlpreds(_33010, _33010))], (74 ^ _30804) ^ [_33212, _33214] : [genlinverse(_33214, _33212), -(binarypredicate(_33212))], (80 ^ _30804) ^ [_33420, _33422] : [genlinverse(_33422, _33420), -(binarypredicate(_33422))], (86 ^ _30804) ^ [_33642, _33644, _33646] : [-(genlinverse(_33642, _33644)), genlinverse(_33646, _33644), genlpreds(_33642, _33646)], (96 ^ _30804) ^ [_33965, _33967, _33969] : [-(genlinverse(_33969, _33965)), genlinverse(_33969, _33967), genlpreds(_33967, _33965)], (106 ^ _30804) ^ [_34274, _34276] : [disjointwith(_34276, _34274), -(collection(_34274))], (112 ^ _30804) ^ [_34482, _34484] : [disjointwith(_34484, _34482), -(collection(_34484))], (118 ^ _30804) ^ [_34690, _34692] : [disjointwith(_34692, _34690), -(disjointwith(_34690, _34692))], (124 ^ _30804) ^ [_34914, _34916, _34918] : [-(disjointwith(_34918, _34914)), disjointwith(_34918, _34916), genls(_34914, _34916)], (134 ^ _30804) ^ [_35237, _35239, _35241] : [-(disjointwith(_35237, _35239)), disjointwith(_35241, _35239), genls(_35237, _35241)], (144 ^ _30804) ^ [_35546, _35548] : [isa(_35548, _35546), -(collection(_35546))], (150 ^ _30804) ^ [_35754, _35756] : [isa(_35756, _35754), -(collection(_35754))], (156 ^ _30804) ^ [_35962, _35964] : [isa(_35964, _35962), -(thing(_35964))], (162 ^ _30804) ^ [_36170, _36172] : [isa(_36172, _36170), -(thing(_36172))], (168 ^ _30804) ^ [_36392, _36394, _36396] : [-(isa(_36396, _36392)), isa(_36396, _36394), genls(_36394, _36392)], (178 ^ _30804) ^ [] : [-(mtvisible(c_basekb))], (180 ^ _30804) ^ [_36754, _36756] : [geographicalsubregions(_36756, _36754), -(geographicalregion(_36754))], (186 ^ _30804) ^ [_36962, _36964] : [geographicalsubregions(_36964, _36962), -(geographicalregion(_36964))], (202 ^ _30804) ^ [_37459] : [geographicalregion(_37459), -(geographicalsubregions(_37459, _37459))], (192 ^ _30804) ^ [_37184, _37186, _37188] : [-(geographicalsubregions(_37188, _37184)), geographicalsubregions(_37188, _37186), geographicalsubregions(_37186, _37184)]], input).
% 0.28/1.38 ncf('1',plain,[geographicalsubregions(c_georegion_l3_x11_y2, c_georegion_l4_x35_y7)],start(210 ^ 0)).
% 0.28/1.38 ncf('1.1',plain,[-(geographicalsubregions(c_georegion_l3_x11_y2, c_georegion_l4_x35_y7)), mtvisible(c_tptpgeo_member1_mt)],extension(2 ^ 1)).
% 0.28/1.38 ncf('1.1.1',plain,[-(mtvisible(c_tptpgeo_member1_mt))],extension(208 ^ 2)).
% 0.28/1.38 %-----------------------------------------------------
% 0.28/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------