%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM387+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:44:31 EDT 2023
% Result : Theorem 0.33s 1.40s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NUM387+1 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n001.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.35 % DateTime : Thu May 18 17:14:20 EDT 2023
% 0.12/0.35 % CPUTime :
% 0.33/1.40
% 0.33/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.40 %-----------------------------------------------------
% 0.33/1.40 ncf(matrix, plain, [(308 ^ _45137) ^ [] : [-(306 ^ [] = succ(306 ^ []))], (130 ^ _45137) ^ [_49348, _49350] : [in(_49350, _49348), in(_49348, _49350)], (136 ^ _45137) ^ [_49545] : [empty(_49545), -(function(_49545))], (142 ^ _45137) ^ [_49731] : [empty(_49731), -(relation(_49731))], (148 ^ _45137) ^ [_49917] : [159 ^ _45137 : [(160 ^ _45137) ^ [] : [-(relation(_49917))], (162 ^ _45137) ^ [] : [-(function(_49917))], (164 ^ _45137) ^ [] : [-(one_to_one(_49917))]], relation(_49917), empty(_49917), function(_49917)], (166 ^ _45137) ^ [_50409, _50411] : [-(set_union2(_50411, _50409) = set_union2(_50409, _50411))], (168 ^ _45137) ^ [_50495] : [-(succ(_50495) = set_union2(_50495, singleton(_50495)))], (171 ^ _45137) ^ [_50619] : [-(element(169 ^ [_50619], _50619))], (173 ^ _45137) ^ [] : [-(empty(empty_set))], (175 ^ _45137) ^ [] : [-(relation(empty_set))], (177 ^ _45137) ^ [] : [-(relation_empty_yielding(empty_set))], (179 ^ _45137) ^ [_50864] : [empty(succ(_50864))], (181 ^ _45137) ^ [] : [-(empty(empty_set))], (183 ^ _45137) ^ [_51025, _51027] : [-(relation(set_union2(_51027, _51025))), relation(_51027), relation(_51025)], (193 ^ _45137) ^ [_51324, _51326] : [-(empty(_51326)), empty(set_union2(_51326, _51324))], (199 ^ _45137) ^ [_51540, _51542] : [-(empty(_51542)), empty(set_union2(_51540, _51542))], (205 ^ _45137) ^ [] : [-(empty(empty_set))], (207 ^ _45137) ^ [] : [-(relation(empty_set))], (209 ^ _45137) ^ [_51849, _51851] : [-(set_union2(_51851, _51851) = _51851)], (212 ^ _45137) ^ [] : [-(relation(210 ^ []))], (214 ^ _45137) ^ [] : [-(function(210 ^ []))], (217 ^ _45137) ^ [] : [-(empty(215 ^ []))], (219 ^ _45137) ^ [] : [-(relation(215 ^ []))], (222 ^ _45137) ^ [] : [-(empty(220 ^ []))], (225 ^ _45137) ^ [] : [-(relation(223 ^ []))], (227 ^ _45137) ^ [] : [-(empty(223 ^ []))], (229 ^ _45137) ^ [] : [-(function(223 ^ []))], (232 ^ _45137) ^ [] : [empty(230 ^ [])], (234 ^ _45137) ^ [] : [-(relation(230 ^ []))], (237 ^ _45137) ^ [] : [empty(235 ^ [])], (240 ^ _45137) ^ [] : [-(relation(238 ^ []))], (242 ^ _45137) ^ [] : [-(function(238 ^ []))], (244 ^ _45137) ^ [] : [-(one_to_one(238 ^ []))], (247 ^ _45137) ^ [] : [-(relation(245 ^ []))], (249 ^ _45137) ^ [] : [-(relation_empty_yielding(245 ^ []))], (252 ^ _45137) ^ [] : [-(relation(250 ^ []))], (254 ^ _45137) ^ [] : [-(relation_empty_yielding(250 ^ []))], (256 ^ _45137) ^ [] : [-(function(250 ^ []))], (259 ^ _45137) ^ [] : [-(relation(257 ^ []))], (261 ^ _45137) ^ [] : [-(relation_non_empty(257 ^ []))], (263 ^ _45137) ^ [] : [-(function(257 ^ []))], (265 ^ _45137) ^ [_53544] : [-(in(_53544, succ(_53544)))], (267 ^ _45137) ^ [_53624] : [-(set_union2(_53624, empty_set) = _53624)], (269 ^ _45137) ^ [_53734, _53736] : [in(_53736, _53734), -(element(_53736, _53734))], (275 ^ _45137) ^ [_53944, _53946] : [element(_53946, _53944), -(empty(_53944)), -(in(_53946, _53944))], (285 ^ _45137) ^ [_54228] : [empty(_54228), -(_54228 = empty_set)], (291 ^ _45137) ^ [_54430, _54432] : [in(_54432, _54430), empty(_54430)], (297 ^ _45137) ^ [_54617, _54619] : [empty(_54619), -(_54619 = _54617), empty(_54617)], (108 ^ _45137) ^ [_48563, _48565] : [_48565 = _48563, -(singleton(_48565) = singleton(_48563))], (124 ^ _45137) ^ [_49120, _49122] : [_49122 = _49120, -(succ(_49122) = succ(_49120))], (114 ^ _45137) ^ [_48809, _48811, _48813, _48815] : [-(set_union2(_48815, _48811) = set_union2(_48813, _48809)), _48815 = _48813, _48811 = _48809], (2 ^ _45137) ^ [_45281] : [-(_45281 = _45281)], (4 ^ _45137) ^ [_45388, _45390] : [_45390 = _45388, -(_45388 = _45390)], (10 ^ _45137) ^ [_45592, _45594, _45596] : [-(_45596 = _45592), _45596 = _45594, _45594 = _45592], (20 ^ _45137) ^ [_45905, _45907] : [-(one_to_one(_45905)), _45907 = _45905, one_to_one(_45907)], (30 ^ _45137) ^ [_46200, _46202] : [-(relation_empty_yielding(_46200)), _46202 = _46200, relation_empty_yielding(_46202)], (40 ^ _45137) ^ [_46495, _46497] : [-(relation(_46495)), _46497 = _46495, relation(_46497)], (50 ^ _45137) ^ [_46790, _46792] : [-(relation_non_empty(_46790)), _46792 = _46790, relation_non_empty(_46792)], (60 ^ _45137) ^ [_47085, _47087] : [-(function(_47085)), _47087 = _47085, function(_47087)], (70 ^ _45137) ^ [_47408, _47410, _47412, _47414] : [-(element(_47412, _47408)), element(_47414, _47410), _47414 = _47412, _47410 = _47408], (98 ^ _45137) ^ [_48248, _48250] : [-(empty(_48248)), _48250 = _48248, empty(_48250)], (84 ^ _45137) ^ [_47852, _47854, _47856, _47858] : [-(in(_47856, _47852)), in(_47858, _47854), _47858 = _47856, _47854 = _47852]], input).
% 0.33/1.40 ncf('1',plain,[in(306 ^ [], succ(306 ^ [])), in(succ(306 ^ []), 306 ^ [])],start(130 ^ 0,bind([[_49348, _49350], [succ(306 ^ []), 306 ^ []]]))).
% 0.33/1.40 ncf('1.1',plain,[-(in(306 ^ [], succ(306 ^ [])))],extension(265 ^ 1,bind([[_53544], [306 ^ []]]))).
% 0.33/1.40 ncf('1.2',plain,[-(in(succ(306 ^ []), 306 ^ [])), in(306 ^ [], succ(306 ^ [])), 306 ^ [] = succ(306 ^ []), succ(306 ^ []) = 306 ^ []],extension(84 ^ 1,bind([[_47852, _47854, _47856, _47858], [306 ^ [], succ(306 ^ []), succ(306 ^ []), 306 ^ []]]))).
% 0.33/1.40 ncf('1.2.1',plain,[-(in(306 ^ [], succ(306 ^ [])))],extension(265 ^ 2,bind([[_53544], [306 ^ []]]))).
% 0.33/1.40 ncf('1.2.2',plain,[-(306 ^ [] = succ(306 ^ []))],extension(308 ^ 2)).
% 0.33/1.40 ncf('1.2.3',plain,[-(succ(306 ^ []) = 306 ^ []), 306 ^ [] = succ(306 ^ [])],extension(4 ^ 2,bind([[_45388, _45390], [succ(306 ^ []), 306 ^ []]]))).
% 0.33/1.40 ncf('1.2.3.1',plain,[-(306 ^ [] = succ(306 ^ []))],lemmata('[1].x')).
% 0.33/1.40 %-----------------------------------------------------
% 0.33/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------