%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CSR069+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:59:36 EDT 2023
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR069+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n016.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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:44:57 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(200 ^ _30097) ^ [] : [-(mtvisible(c_tptpgeo_member1_mt))], (202 ^ _30097) ^ [] : [borderson(c_georegion_l4_x38_y24, c_georegion_l4_x39_y24)], (2 ^ _30097) ^ [] : [mtvisible(c_tptpgeo_member1_mt), -(borderson(c_georegion_l4_x38_y24, c_georegion_l4_x39_y24))], (8 ^ _30097) ^ [_30343, _30345, _30347] : [isa(_30347, _30345), isa(_30347, _30343), disjointwith(_30345, _30343)], (18 ^ _30097) ^ [_30665, _30667, _30669] : [-(genlpreds(_30669, _30665)), genlinverse(_30669, _30667), genlinverse(_30667, _30665)], (28 ^ _30097) ^ [_30974, _30976] : [genlpreds(_30976, _30974), -(predicate(_30974))], (34 ^ _30097) ^ [_31182, _31184] : [genlpreds(_31184, _31182), -(predicate(_31182))], (40 ^ _30097) ^ [_31390, _31392] : [genlpreds(_31392, _31390), -(predicate(_31392))], (46 ^ _30097) ^ [_31598, _31600] : [genlpreds(_31600, _31598), -(predicate(_31600))], (52 ^ _30097) ^ [_31820, _31822, _31824] : [-(genlpreds(_31824, _31820)), genlpreds(_31824, _31822), genlpreds(_31822, _31820)], (62 ^ _30097) ^ [_32115] : [predicate(_32115), -(genlpreds(_32115, _32115))], (68 ^ _30097) ^ [_32303] : [predicate(_32303), -(genlpreds(_32303, _32303))], (74 ^ _30097) ^ [_32505, _32507] : [genlinverse(_32507, _32505), -(binarypredicate(_32505))], (80 ^ _30097) ^ [_32713, _32715] : [genlinverse(_32715, _32713), -(binarypredicate(_32715))], (86 ^ _30097) ^ [_32935, _32937, _32939] : [-(genlinverse(_32935, _32937)), genlinverse(_32939, _32937), genlpreds(_32935, _32939)], (96 ^ _30097) ^ [_33258, _33260, _33262] : [-(genlinverse(_33262, _33258)), genlinverse(_33262, _33260), genlpreds(_33260, _33258)], (106 ^ _30097) ^ [_33567, _33569] : [disjointwith(_33569, _33567), -(collection(_33567))], (112 ^ _30097) ^ [_33775, _33777] : [disjointwith(_33777, _33775), -(collection(_33777))], (118 ^ _30097) ^ [_33983, _33985] : [disjointwith(_33985, _33983), -(disjointwith(_33983, _33985))], (124 ^ _30097) ^ [_34207, _34209, _34211] : [-(disjointwith(_34211, _34207)), disjointwith(_34211, _34209), genls(_34207, _34209)], (134 ^ _30097) ^ [_34530, _34532, _34534] : [-(disjointwith(_34530, _34532)), disjointwith(_34534, _34532), genls(_34530, _34534)], (144 ^ _30097) ^ [_34839, _34841] : [isa(_34841, _34839), -(collection(_34839))], (150 ^ _30097) ^ [_35047, _35049] : [isa(_35049, _35047), -(collection(_35047))], (156 ^ _30097) ^ [_35255, _35257] : [isa(_35257, _35255), -(thing(_35257))], (162 ^ _30097) ^ [_35463, _35465] : [isa(_35465, _35463), -(thing(_35465))], (168 ^ _30097) ^ [_35685, _35687, _35689] : [-(isa(_35689, _35685)), isa(_35689, _35687), genls(_35687, _35685)], (178 ^ _30097) ^ [] : [-(mtvisible(c_basekb))], (180 ^ _30097) ^ [_36047, _36049] : [borderson(_36049, _36047), -(geographicalregion(_36047))], (186 ^ _30097) ^ [_36255, _36257] : [borderson(_36257, _36255), -(geographicalregion(_36257))], (198 ^ _30097) ^ [_36623] : [borderson(_36623, _36623)], (192 ^ _30097) ^ [_36463, _36465] : [borderson(_36465, _36463), -(borderson(_36463, _36465))]], input).
% 0.32/1.38 ncf('1',plain,[borderson(c_georegion_l4_x38_y24, c_georegion_l4_x39_y24)],start(202 ^ 0)).
% 0.32/1.38 ncf('1.1',plain,[-(borderson(c_georegion_l4_x38_y24, c_georegion_l4_x39_y24)), mtvisible(c_tptpgeo_member1_mt)],extension(2 ^ 1)).
% 0.32/1.38 ncf('1.1.1',plain,[-(mtvisible(c_tptpgeo_member1_mt))],extension(200 ^ 2)).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------