%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU356+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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 12:03:15 EDT 2023
% Result : Theorem 43.64s 42.87s
% Output : Proof 43.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU356+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n003.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 : Thu May 18 12:39:00 EDT 2023
% 0.12/0.34 % CPUTime :
% 43.64/42.87
% 43.64/42.87 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 43.64/42.87 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.64/42.87 %-----------------------------------------------------
% 43.64/42.87 ncf(matrix, plain, [(265 ^ _62646) ^ [] : [266 ^ _62646 : [(269 ^ _62646) ^ [_62985] : [element(_62985, the_carrier(258 ^ [])), relstr_set_smaller(258 ^ [], 263 ^ [], _62985), 277 ^ _62646 : [(282 ^ _62646) ^ [] : [related(258 ^ [], _62985, 276 ^ [_62985])], (280 ^ _62646) ^ [] : [-(relstr_set_smaller(258 ^ [], 263 ^ [], 276 ^ [_62985]))], (278 ^ _62646) ^ [] : [-(element(276 ^ [_62985], the_carrier(258 ^ [])))]]], (267 ^ _62646) ^ [] : [-(ex_sup_of_relstr_set(258 ^ [], 263 ^ []))]], 284 ^ _62646 : [(285 ^ _62646) ^ [] : [-(element(283 ^ [], the_carrier(258 ^ [])))], (287 ^ _62646) ^ [] : [-(relstr_set_smaller(258 ^ [], 263 ^ [], 283 ^ []))], (289 ^ _62646) ^ [_63662] : [element(_63662, the_carrier(258 ^ [])), relstr_set_smaller(258 ^ [], 263 ^ [], _63662), -(related(258 ^ [], 283 ^ [], _63662))], (299 ^ _62646) ^ [] : [ex_sup_of_relstr_set(258 ^ [], 263 ^ [])]]], (262 ^ _62646) ^ [] : [-(rel_str(258 ^ []))], (260 ^ _62646) ^ [] : [-(antisymmetric_relstr(258 ^ []))], !, (64 ^ _53767) ^ [_55872, _55874, _55876, _55878] : [-(element(_55876, _55872)), element(_55878, _55874), _55878 = _55876, _55874 = _55872], (212 ^ _53767) ^ [] : [true___, -(true___)], (231 ^ _53767) ^ [_61700] : [-(element(229 ^ [_61700], _61700))], (96 ^ _53767) ^ [_56933, _56935, _56937, _56939, _56941, _56943] : [-(related(_56941, _56937, _56933)), related(_56943, _56939, _56935), _56943 = _56941, _56939 = _56937, _56935 = _56933], (20 ^ _53767) ^ [_54515, _54517] : [-(one_sorted_str(_54515)), _54517 = _54515, one_sorted_str(_54517)], (50 ^ _53767) ^ [_55428, _55430, _55432, _55434] : [-(ex_sup_of_relstr_set(_55432, _55428)), ex_sup_of_relstr_set(_55434, _55430), _55434 = _55432, _55430 = _55428], (2 ^ _53767) ^ [_53891] : [-(_53891 = _53891)], (228 ^ _53767) ^ [] : [-(one_sorted_str(226 ^ []))], (218 ^ _53767) ^ [] : [true___, -(true___)], (114 ^ _53767) ^ [_57484, _57486] : [_57486 = _57484, -(the_carrier(_57486) = the_carrier(_57484))], (200 ^ _53767) ^ [_60955] : [rel_str(_60955), -(one_sorted_str(_60955))], (40 ^ _53767) ^ [_55105, _55107] : [-(rel_str(_55105)), _55107 = _55105, rel_str(_55107)], (10 ^ _53767) ^ [_54202, _54204, _54206] : [-(_54206 = _54202), _54206 = _54204, _54204 = _54202], (225 ^ _53767) ^ [] : [-(rel_str(223 ^ []))], (78 ^ _53767) ^ [_56344, _56346, _56348, _56350, _56352, _56354] : [-(relstr_set_smaller(_56352, _56348, _56344)), relstr_set_smaller(_56354, _56350, _56346), _56354 = _56352, _56350 = _56348, _56346 = _56344], (120 ^ _53767) ^ [_57690] : [rel_str(_57690), 123 ^ _53767 : [(124 ^ _53767) ^ [_57944] : [ex_sup_of_relstr_set(_57690, _57944), 128 ^ _53767 : [(131 ^ _53767) ^ [] : [-(relstr_set_smaller(_57690, _57944, 127 ^ [_57690, _57944]))], (133 ^ _53767) ^ [_58469] : [element(_58469, the_carrier(_57690)), relstr_set_smaller(_57690, _57944, _58469), -(related(_57690, 127 ^ [_57690, _57944], _58469))], (143 ^ _53767) ^ [_58770] : [element(_58770, the_carrier(_57690)), -(_58770 = 127 ^ [_57690, _57944]), relstr_set_smaller(_57690, _57944, _58770), 153 ^ _53767 : [(158 ^ _53767) ^ [] : [related(_57690, _58770, 152 ^ [_57690, _57944, _58770])], (156 ^ _53767) ^ [] : [-(relstr_set_smaller(_57690, _57944, 152 ^ [_57690, _57944, _58770]))], (154 ^ _53767) ^ [] : [-(element(152 ^ [_57690, _57944, _58770], the_carrier(_57690)))]]], (129 ^ _53767) ^ [] : [-(element(127 ^ [_57690, _57944], the_carrier(_57690)))]]], (162 ^ _53767) ^ [_59417] : [-(ex_sup_of_relstr_set(_57690, _59417)), 163 ^ _53767 : [(164 ^ _53767) ^ [_59594] : [element(_59594, the_carrier(_57690)), relstr_set_smaller(_57690, _59417, _59594), 174 ^ _53767 : [(179 ^ _53767) ^ [] : [related(_57690, _59594, 173 ^ [_57690, _59417, _59594])], (177 ^ _53767) ^ [] : [-(relstr_set_smaller(_57690, _59417, 173 ^ [_57690, _59417, _59594]))], (175 ^ _53767) ^ [] : [-(element(173 ^ [_57690, _59417, _59594], the_carrier(_57690)))]], 181 ^ _53767 : [(196 ^ _53767) ^ [] : [180 ^ [_57690, _59417, _59594] = _59594], (184 ^ _53767) ^ [] : [-(relstr_set_smaller(_57690, _59417, 180 ^ [_57690, _59417, _59594]))], (186 ^ _53767) ^ [_60484] : [element(_60484, the_carrier(_57690)), relstr_set_smaller(_57690, _59417, _60484), -(related(_57690, 180 ^ [_57690, _59417, _59594], _60484))], (182 ^ _53767) ^ [] : [-(element(180 ^ [_57690, _59417, _59594], the_carrier(_57690)))]]]]]]], (233 ^ _53767) ^ [_61778] : [antisymmetric_relstr(_61778), rel_str(_61778), 240 ^ _53767 : [(241 ^ _53767) ^ [_62021] : [element(_62021, the_carrier(_61778)), 244 ^ _53767 : [(245 ^ _53767) ^ [_62180] : [element(_62180, the_carrier(_61778)), -(_62021 = _62180), related(_61778, _62021, _62180), related(_61778, _62180, _62021)]]]]], (206 ^ _53767) ^ [] : [true___, -(true___)], (30 ^ _53767) ^ [_54810, _54812] : [-(antisymmetric_relstr(_54810)), _54812 = _54810, antisymmetric_relstr(_54812)], (4 ^ _53767) ^ [_53998, _54000] : [_54000 = _53998, -(_53998 = _54000)]], input).
% 43.64/42.87 ncf('1',plain,[267 : -(ex_sup_of_relstr_set(258 ^ [], 263 ^ [])), 285 : -(element(283 ^ [], the_carrier(258 ^ [])))],start(265 ^ 0)).
% 43.64/42.87 ncf('1.1',plain,[ex_sup_of_relstr_set(258 ^ [], 263 ^ []), 131 : -(relstr_set_smaller(258 ^ [], 263 ^ [], 127 ^ [258 ^ [], 263 ^ []])), 124 : rel_str(258 ^ [])],extension(120 ^ 3,bind([[_57690, _57944], [258 ^ [], 263 ^ []]]))).
% 43.64/42.87 ncf('1.1.1',plain,[relstr_set_smaller(258 ^ [], 263 ^ [], 127 ^ [258 ^ [], 263 ^ []]), element(127 ^ [258 ^ [], 263 ^ []], the_carrier(258 ^ [])), 282 : related(258 ^ [], 127 ^ [258 ^ [], 263 ^ []], 276 ^ [127 ^ [258 ^ [], 263 ^ []]])],extension(269 ^ 8,bind([[_62985], [127 ^ [258 ^ [], 263 ^ []]]]))).
% 43.64/42.87 ncf('1.1.1.1',plain,[-(element(127 ^ [258 ^ [], 263 ^ []], the_carrier(258 ^ [])))],extension(129 ^ 9)).
% 43.64/42.87 ncf('1.1.1.2',plain,[-(related(258 ^ [], 127 ^ [258 ^ [], 263 ^ []], 276 ^ [127 ^ [258 ^ [], 263 ^ []]])), element(276 ^ [127 ^ [258 ^ [], 263 ^ []]], the_carrier(258 ^ [])), relstr_set_smaller(258 ^ [], 263 ^ [], 276 ^ [127 ^ [258 ^ [], 263 ^ []]])],extension(133 ^ 11,bind([[_58469], [276 ^ [127 ^ [258 ^ [], 263 ^ []]]]]))).
% 43.64/42.87 ncf('1.1.1.2.1',plain,[-(element(276 ^ [127 ^ [258 ^ [], 263 ^ []]], the_carrier(258 ^ [])))],extension(278 ^ 12)).
% 43.64/42.87 ncf('1.1.1.2.2',plain,[-(relstr_set_smaller(258 ^ [], 263 ^ [], 276 ^ [127 ^ [258 ^ [], 263 ^ []]]))],extension(280 ^ 12)).
% 43.64/42.87 ncf('1.1.2',plain,[-(rel_str(258 ^ []))],extension(262 ^ 4)).
% 43.64/42.87 ncf('1.2',plain,[element(283 ^ [], the_carrier(258 ^ [])), 164 : relstr_set_smaller(258 ^ [], 263 ^ [], 283 ^ []), 179 : related(258 ^ [], 283 ^ [], 173 ^ [258 ^ [], 263 ^ [], 283 ^ []]), 196 : 180 ^ [258 ^ [], 263 ^ [], 283 ^ []] = 283 ^ [], 164 : -(ex_sup_of_relstr_set(258 ^ [], 263 ^ [])), 162 : rel_str(258 ^ [])],extension(120 ^ 3,bind([[_57690, _59417, _59594], [258 ^ [], 263 ^ [], 283 ^ []]]))).
% 43.64/42.87 ncf('1.2.1',plain,[-(relstr_set_smaller(258 ^ [], 263 ^ [], 283 ^ []))],extension(287 ^ 8)).
% 43.64/42.87 ncf('1.2.2',plain,[-(related(258 ^ [], 283 ^ [], 173 ^ [258 ^ [], 263 ^ [], 283 ^ []])), element(173 ^ [258 ^ [], 263 ^ [], 283 ^ []], the_carrier(258 ^ [])), relstr_set_smaller(258 ^ [], 263 ^ [], 173 ^ [258 ^ [], 263 ^ [], 283 ^ []])],extension(289 ^ 10,bind([[_63662], [173 ^ [258 ^ [], 263 ^ [], 283 ^ []]]]))).
% 43.64/42.87 ncf('1.2.2.1',plain,[-(element(173 ^ [258 ^ [], 263 ^ [], 283 ^ []], the_carrier(258 ^ [])))],extension(175 ^ 11)).
% 43.64/42.87 ncf('1.2.2.2',plain,[-(relstr_set_smaller(258 ^ [], 263 ^ [], 173 ^ [258 ^ [], 263 ^ [], 283 ^ []]))],extension(177 ^ 11)).
% 43.64/42.87 ncf('1.2.3',plain,[-(180 ^ [258 ^ [], 263 ^ [], 283 ^ []] = 283 ^ []), 245 : element(283 ^ [], the_carrier(258 ^ [])), 245 : related(258 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []], 283 ^ []), 245 : related(258 ^ [], 283 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []]), 245 : element(180 ^ [258 ^ [], 263 ^ [], 283 ^ []], the_carrier(258 ^ [])), 241 : antisymmetric_relstr(258 ^ []), 241 : rel_str(258 ^ [])],extension(233 ^ 10,bind([[_61778, _62021, _62180], [258 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []], 283 ^ []]]))).
% 43.64/42.87 ncf('1.2.3.1',plain,[-(element(283 ^ [], the_carrier(258 ^ [])))],reduction('1')).
% 43.64/42.87 ncf('1.2.3.2',plain,[-(related(258 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []], 283 ^ [])), element(283 ^ [], the_carrier(258 ^ [])), relstr_set_smaller(258 ^ [], 263 ^ [], 283 ^ [])],extension(186 ^ 15,bind([[_60484], [283 ^ []]]))).
% 43.64/42.87 ncf('1.2.3.2.1',plain,[-(element(283 ^ [], the_carrier(258 ^ [])))],lemmata('[2, 1].x')).
% 43.64/42.87 ncf('1.2.3.2.2',plain,[-(relstr_set_smaller(258 ^ [], 263 ^ [], 283 ^ []))],lemmata('[1].x')).
% 43.64/42.87 ncf('1.2.3.3',plain,[-(related(258 ^ [], 283 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []])), element(180 ^ [258 ^ [], 263 ^ [], 283 ^ []], the_carrier(258 ^ [])), relstr_set_smaller(258 ^ [], 263 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []])],extension(289 ^ 15,bind([[_63662], [180 ^ [258 ^ [], 263 ^ [], 283 ^ []]]]))).
% 43.64/42.87 ncf('1.2.3.3.1',plain,[-(element(180 ^ [258 ^ [], 263 ^ [], 283 ^ []], the_carrier(258 ^ [])))],extension(182 ^ 16)).
% 43.64/42.87 ncf('1.2.3.3.2',plain,[-(relstr_set_smaller(258 ^ [], 263 ^ [], 180 ^ [258 ^ [], 263 ^ [], 283 ^ []]))],extension(184 ^ 16)).
% 43.64/42.87 ncf('1.2.3.4',plain,[-(element(180 ^ [258 ^ [], 263 ^ [], 283 ^ []], the_carrier(258 ^ [])))],extension(182 ^ 13)).
% 43.64/42.87 ncf('1.2.3.5',plain,[-(antisymmetric_relstr(258 ^ []))],extension(260 ^ 11)).
% 43.64/42.87 ncf('1.2.3.6',plain,[-(rel_str(258 ^ []))],extension(262 ^ 11)).
% 43.64/42.87 ncf('1.2.4',plain,[ex_sup_of_relstr_set(258 ^ [], 263 ^ [])],extension(299 ^ 6)).
% 43.64/42.87 ncf('1.2.5',plain,[-(rel_str(258 ^ []))],extension(262 ^ 4)).
% 43.64/42.87 %-----------------------------------------------------
% 43.64/42.87 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------